For a fixed supplied family and its once-chosen links, put
The selected vector states give a cyclic-sum isometry
The nonunital version first proves unit preservation for the same nonzero irreducible representation. Simplicity and compact-operator exclusion are subsequent consequences. The existential unitary in a separately applied theorem need not equal a witness selected in another application.
Exact Card references
- The CAR source map into the fixed shell-family target — MathlibAnnex.CStarAlgebra.CAR.shellFamilySourceHom
- The ambient inclusion of the fixed shell-family target — MathlibAnnex.CStarAlgebra.CAR.shellFamilyInclusion
- Assembling selected GNS cyclic subspaces into an isometric source representation — MathlibAnnex.CStarAlgebra.CAR.exists_selectedAtomicCyclicIsometry
- The cyclic sum fills every irreducible target representation — MathlibAnnex.CStarAlgebra.CAR.exists_surjective_selectedAtomicCyclicIsometry
- Every irreducible target representation is the displayed operator model — MathlibAnnex.CStarAlgebra.CAR.ambientInclusion_unitaryEquivalent
- Irreducible representations are captured without assuming unitality — MathlibAnnex.CStarAlgebra.CAR.shellFamilyInclusion_unitaryEquivalent_nonUnital
- Closed-ideal simplicity of the shell-generated algebra — MathlibAnnex.CStarAlgebra.CAR.isSimpleCStarAlgebra_shellFamilyTarget
- The shell-generated algebra is not an algebra of all compact operators — MathlibAnnex.CStarAlgebra.CAR.not_isCompactOperatorModel_shellFamilyTarget
- One fixed shell-generated algebra and its representation-theoretic endpoint — MathlibAnnex.CStarAlgebra.CAR.shellFamilyEndpoint
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 CAR source map into the fixed shell-family target
MathlibAnnex.CStarAlgebra.CAR.shellFamilySourceHom
Restricting the codomain of the selected atomic representation gives the source map into one fixed generated target.
Immediate prerequisites in this Project
None in this scope
Used by in this Project
The shell-generated algebra is not an algebra of all compact operators, Closed-ideal simplicity of the shell-generated algebra
The ambient inclusion of the fixed shell-family target
MathlibAnnex.CStarAlgebra.CAR.shellFamilyInclusion
The same concrete target has a literal representation on the selected atomic Hilbert space.
Immediate prerequisites in this Project
None in this scope
Used by in this Project
Closed-ideal simplicity of the shell-generated algebra, Unitary equivalence without an initial unitality assumption
Assembling selected GNS cyclic subspaces into an isometric source representation
MathlibAnnex.CStarAlgebra.CAR.exists_selectedAtomicCyclicIsometry
Joins mutually orthogonal pure-state cyclic copies and controls the limiting flag projections on their sum.
Immediate prerequisites in this Project
None in this scope
Used by in this Project
The cyclic sum fills every irreducible target representation
Level 1
The cyclic sum fills every irreducible target representation
MathlibAnnex.CStarAlgebra.CAR.exists_surjective_selectedAtomicCyclicIsometry
Uses shell reconstruction and residual lines to turn an isometric CAR intertwiner into a unitary equivalence on the source.
Immediate prerequisites in this Project
Assembling selected GNS cyclic subspaces into an isometric source representation
Used by in this Project
Every irreducible representation is unitarily equivalent to the inclusion
The shell-generated algebra is not an algebra of all compact operators
MathlibAnnex.CStarAlgebra.CAR.not_isCompactOperatorModel_shellFamilyTarget
Excludes an injective representation of the infinite-dimensional unital algebra onto all compact operators.
Immediate prerequisites in this Project
The CAR source map into the fixed shell-family target
Used by in this Project
Structural properties of one shell-generated C*-algebra
Level 2
Every irreducible representation is unitarily equivalent to the inclusion
MathlibAnnex.CStarAlgebra.CAR.ambientInclusion_unitaryEquivalent
Extends the unitary equivalence from the CAR source to all additional generators and the norm-closed target.
Immediate prerequisites in this Project
The cyclic sum fills every irreducible target representation
Used by in this Project
Closed-ideal simplicity of the shell-generated algebra, Unitary equivalence without an initial unitality assumption
Level 3
Unitary equivalence without an initial unitality assumption
MathlibAnnex.CStarAlgebra.CAR.shellFamilyInclusion_unitaryEquivalent_nonUnital
Shows why allowing nonunital input representations does not enlarge the irreducible representation class of the shell-generated algebra.
Immediate prerequisites in this Project
The ambient inclusion of the fixed shell-family target, Every irreducible representation is unitarily equivalent to the inclusion
Used by in this Project
Structural properties of one shell-generated C*-algebra
Closed-ideal simplicity of the shell-generated algebra
MathlibAnnex.CStarAlgebra.CAR.isSimpleCStarAlgebra_shellFamilyTarget
Uses a faithful irreducible representation in the unique unitary-equivalence class to rule out proper nonzero closed two-sided ideals.
Immediate prerequisites in this Project
The ambient inclusion of the fixed shell-family target, Every irreducible representation is unitarily equivalent to the inclusion, The CAR source map into the fixed shell-family target
Used by in this Project
Structural properties of one shell-generated C*-algebra
Level 4
Structural properties of one shell-generated C*-algebra
MathlibAnnex.CStarAlgebra.CAR.shellFamilyEndpoint
Collects the proved properties of a single generated algebra, keeping the shell-family input separate from its consequences.
Immediate prerequisites in this Project
The shell-generated algebra is not an algebra of all compact operators, Closed-ideal simplicity of the shell-generated algebra, Unitary equivalence without an initial unitality assumption
Used by in this Project
None in this scope