MathlibAnnex.CStarAlgebra.CAR.shellFamilyEndpoint
Collects the proved properties of a single generated algebra, keeping the shell-family input separate from its consequences.
Statement
For every fixed shell family, form
Assumptions
Let
Index chosen pure-state Gelfand-Naimark-Segal (GNS) representations by their unitary-equivalence classes
A fixed shell family consists of complex-linear unital star automorphisms
At the root,
Let
Choose once a family of unitary operators
Put
The comparison Hilbert space
Conclusion
All conclusions concern this same concrete
Proof route
The construction of the shell unitaries gives a faithful source map and irreducible inclusion. The unital copy of the infinite-dimensional CAR algebra makes
Proof steps
Choose the links once, restrict
to the generated algebra, and use its faithful root summand. Norm closure is part of the construction of . If
were finite-dimensional, its injective complex-linear source map would make finite-dimensional, contradicting the growing matrix stages. Apply the unitary-equivalence theorem, the nonunital-to-unital argument, and the closed-ideal consequence. Exclude an isomorphism of this same infinite-dimensional algebra onto all compact operators. These are separate proved results supplying the listed fields.
Main citations
- Exact declaration and proof · Exact source
- MathlibAnnex.CStarAlgebra.CAR.ShellFamilyEndpoint · Exact source
- MathlibAnnex.CStarAlgebra.CAR.RepresentativeShellFamily · Exact source
- MathlibAnnex.CStarAlgebra.CAR.exists_completedAtomicShellModel · Exact source
- MathlibAnnex.CStarAlgebra.CAR.shellFamilyLinks · Exact source
- MathlibAnnex.CStarAlgebra.CAR.ShellFamilyTarget · Exact source
- MathlibAnnex.CStarAlgebra.CAR.shellFamilySourceHom · Exact source
- MathlibAnnex.CStarAlgebra.CAR.shellFamilyInclusion · Exact source
- MathlibAnnex.CStarAlgebra.CAR.not_finiteDimensional_shellFamilyTarget · Exact source
- MathlibAnnex.CStarAlgebra.CAR.isUniqueIrreducibleModel_shellFamilyInclusion · Exact source
- MathlibAnnex.CStarAlgebra.CAR.shellFamilyInclusion_unitaryEquivalent_nonUnital · Exact source
- MathlibAnnex.CStarAlgebra.CAR.isSimpleCStarAlgebra_shellFamilyTarget · Exact source
- MathlibAnnex.CStarAlgebra.CAR.not_isCompactOperatorModel_shellFamilyTarget · Exact source
Lean source signature (exact)
theorem shellFamilyEndpoint (family : RepresentativeShellFamily) :
ShellFamilyEndpoint.{v} familyHere ShellFamilyTarget family is shellFamilySourceHom family is shellFamilyInclusion family is ShellFamilyEndpoint is the proposition listing the properties in the Statement; the theorem shellFamilyEndpoint proves it. Its exact structure declaration is linked as “Properties of the fixed target” above. The family, and hence
Read exact source with highlighted declaration · Raw UTF-8 source · Card PDF
Lean realization notes
The separately linked Lean structure lists these properties; defining that proposition does not prove it. This theorem proves that proposition for every supplied family. The family hypothesis remains explicit. The structural theorem for the homogeneity-based algebra and its faithful representation on a separable Hilbert space specialize this fixed-family result.
Exact Card identity
Language: en
CARD_CONTENT_COMPLETE
Card UID: lfh:lfh-declaration-card:sha256:c2533b47d2800cf40bedcc7a2969c4296ab1b60fe6986fe527e1247ef3862788
Card revision: 1 · SHA-256: 963ba28055994c54f1f2a45c157c1d4c74f37952b595c5894c0c051169f78338
Exposition revision: 1 · SHA-256: de7fb04f639023fa54e46122ba7aed2b46a74ac72668314c3322290d884fae3f
Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73
Header SHA-256: 26f34455f56899e7460e8f2200e418326a3bf2d65dc459b8a8e0c90328f1d41c