Let
The generic atomic-shell theorem takes the rank-one limiting defects as hypotheses. The pure-GNS specialization discharges irreducibility, inequivalence and normalization, while retaining the shell hypotheses. The separate CAR realization proves the required residual-line identities. It chooses unitary links once. The generic generated algebra permits arbitrary bounded extra operators and does not itself assert the CAR consequences.
Exact Card references
- The selected GNS representation of a pure-state class — MathlibAnnex.CStarAlgebra.PureState.selectedRepresentation
- Distinct GNS classes have no unitary intertwiner — MathlibAnnex.CStarAlgebra.PureState.no_unitaryIntertwiner_selectedRepresentation
- The atomic direct sum of the selected CAR representations — MathlibAnnex.CStarAlgebra.CAR.selectedAtomicRepresentation
- An irreducible atomic model from projection shells — MathlibAnnex.CStarAlgebra.AtomicConstruction.exists_irreducible_atomicShellModel
- The atomic-shell construction on selected pure-GNS fibers — MathlibAnnex.CStarAlgebra.AtomicConstruction.exists_irreducible_pureAtomicShellModel
- The closed operator algebra generated by a representation and extra operators — MathlibAnnex.CStarAlgebra.AtomicConstruction.concreteTarget
- Realizing a shell family by a faithful irreducible operator algebra — MathlibAnnex.CStarAlgebra.CAR.exists_completedAtomicShellModel
Boundary Inputs
The displayed edges preserve dependency paths through omitted helpers. Levels count selected predecessors within this scope. Mathematical citations remain distinct from formal dependencies.
Exact source and provider boundary · Earlier 466-declaration Project view and PDF
Dependency-first reading route
Levels belong to this reading scope. Follow prerequisites or uses to focus the route.
Level 0
The selected GNS representation of a pure-state class
MathlibAnnex.CStarAlgebra.PureState.selectedRepresentation
A choice of representative pure states, fixed literally at a root, gives one concrete GNS representation per equivalence class.
Immediate prerequisites in this Project
None in this scope
Used by in this Project
Distinct GNS classes have no unitary intertwiner, The atomic direct sum of the selected CAR representations
The closed operator algebra generated by a representation and extra operators
MathlibAnnex.CStarAlgebra.AtomicConstruction.concreteTarget
Places a represented algebra and a chosen family of bounded operators in one concrete closed algebra.
Immediate prerequisites in this Project
None in this scope
Used by in this Project
An irreducible operator algebra constructed from projection shells
Level 1
Distinct GNS classes have no unitary intertwiner
MathlibAnnex.CStarAlgebra.PureState.no_unitaryIntertwiner_selectedRepresentation
The class index makes the selected pure-GNS family pairwise unitarily inequivalent.
Immediate prerequisites in this Project
The selected GNS representation of a pure-state class
Used by in this Project
The atomic-shell construction on selected pure-GNS fibers
The atomic direct sum of the selected CAR representations
MathlibAnnex.CStarAlgebra.CAR.selectedAtomicRepresentation
All selected pure-GNS fibers of the completed CAR algebra act together on one Hilbert direct sum.
Immediate prerequisites in this Project
The selected GNS representation of a pure-state class
Used by in this Project
Realizing a shell family by a faithful irreducible operator algebra
An irreducible operator algebra constructed from projection shells
MathlibAnnex.CStarAlgebra.AtomicConstruction.exists_irreducible_atomicShellModel
Shell partial isometries with rank-one limiting defects can be completed to unitary links that join inequivalent irreducible fibers.
Immediate prerequisites in this Project
The closed operator algebra generated by a representation and extra operators
Used by in this Project
The atomic-shell construction on selected pure-GNS fibers
Level 2
The atomic-shell construction on selected pure-GNS fibers
MathlibAnnex.CStarAlgebra.AtomicConstruction.exists_irreducible_pureAtomicShellModel
Pure-state GNS data supplies the irreducible and inequivalent fibers required by the generic shell construction.
Immediate prerequisites in this Project
Distinct GNS classes have no unitary intertwiner, An irreducible operator algebra constructed from projection shells
Used by in this Project
Realizing a shell family by a faithful irreducible operator algebra
Level 3
Realizing a shell family by a faithful irreducible operator algebra
MathlibAnnex.CStarAlgebra.CAR.exists_completedAtomicShellModel
Constructs unitary links between pure-state summands and an irreducible algebra containing a faithful copy of CAR.
Immediate prerequisites in this Project
The atomic direct sum of the selected CAR representations, The atomic-shell construction on selected pure-GNS fibers
Used by in this Project
None in this scope