MathlibAnnex.CStarAlgebra.CAR.AtomicCounterexampleAlgebra
abbrev
Defines the single algebra used in the irreducible and separable faithful representations.
Statement
Let be the completed CAR algebra and let be its distinguished pure state. Let be the set of unitary-equivalence classes of pure-state GNS representations. Choose a representative in each class, keeping the GNS representation of in its distinguished class, and put and . Fix the automorphisms and shell partial isometries supplied by CAR homogeneity, and choose the corresponding unitaries on by the cited shell construction. Define
Definition
is the norm-closed unital complex -subalgebra of generated by and the unitaries . The automorphisms, shell partial isometries and resulting unitaries are chosen once; the abbreviation does not choose another isomorphic copy of the algebra.
Assumptions
The CAR algebra, the pure state , the GNS representatives and the unitaries are those in the cited fixed construction. The index set is not assumed countable.
Conclusion
The notation refers to this particular generated C*-algebra. It does not denote a new isomorphic copy when different representations of are considered.
The abbreviation defines the algebra; separate theorems establish its simplicity, uniqueness of the nonzero irreducible representation up to unitary equivalence, and failure to be isomorphic to an algebra of compact operators. The fixed construction uses the proved CAR homogeneity theorem, without an additional KOS or CH hypothesis.
Main citations
- Definition
and its exact construction —
MathlibAnnex.CStarAlgebra.CAR.AtomicCounterexampleAlgebra - The
once-chosen representative shell family —
MathlibAnnex.CStarAlgebra.CAR.homogeneityShellFamily - The
generated algebra for a fixed shell family —
MathlibAnnex.CStarAlgebra.CAR.ShellFamilyTarget - The
fixed ambient link operators —
MathlibAnnex.CStarAlgebra.CAR.shellFamilyLinks
Lean source signature (exact)
abbrev AtomicCounterexampleAlgebra := ShellFamilyTarget homogeneityShellFamily
| In the source | Mathematical meaning |
|---|---|
AtomicCounterexampleAlgebra |
The abbreviation denotes the one particular concrete algebra in the statement, rather than an arbitrary algebra chosen anew for each representation. |
homogeneityShellFamily |
The fixed CAR shell family of automorphisms and partial isometries supplied by the proved homogeneity construction, based at the root state . It carries no additional KOS or CH hypothesis. |
ShellFamilyTarget homogeneityShellFamily |
The full RHS is , with , , and the links chosen once for that family. The index set need not be countable. Simplicity and capture are separately proved properties, not clauses of this abbreviation. |
Further source notes: The separately cited
| |
Read exact source with highlighted declaration · Raw UTF-8 source · Card PDF · Back to Project
Exact content identity
Declaration: MathlibAnnex.CStarAlgebra.CAR.AtomicCounterexampleAlgebra
Accepted content SHA-256: ec65232332e17449f6b4ed3d6223d1aa78a8a37182f90ebece96a750fb77b460
Accepted source guide SHA-256: 57e9aaf7410ee102b77ecc712a6140794c7ad914a2bc8e5cfa3cc9407cdbd01e
Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73