Back to Project mathematical routes
Two-sided inner sequences establish pure-state homogeneity, which supplies one fixed shell family. Each non-root component uses the same approximately inner automorphism for all its shells; the generic matching theorem retains its stated hypotheses.
8 direct Cards + 15 reused prerequisites = 23 unique Cards. This count is a selected Card closure, not a source-declaration count.
Route reading PDF · Preserved source exploration
Read this route with prerequisites
Direct references: 19 — Approximately inner homogeneity of pure CAR states · 20 — A two-sided inner intertwining sequence for two states · 24 — Exact projection links for one approximately inner automorphism · 25 — A fixed representative family of CAR shell data · 21 — Two-sided inner sequences imply pure-state homogeneity · 22 — Pure CAR states admit two-sided inner intertwining sequences · 23 — Pure-state homogeneity of the completed CAR algebra · 26 — Choosing the CAR shell family from proved homogeneity
Reused prerequisites: 14 — Purifying a vector state on a finite CAR stage · 3 — The product-vector state on the completed CAR algebra · 10 — Root compression becomes scalar in norm · 15 — Lifting a corner involution to an ambient CAR unitary · 16 — Exact vector transport along an almost central unitary path · 18 — Approximating another vector state along a unitary path · 6 — A finite-row average centralizes its matrix stage · 17 — Cross-representation state approximation with a protected finite set · 9 — The decreasing root projections in the CAR completion · 4 — Purity of the completed root state · 2 — The CAR algebra as a completion of finite matrix stages · 13 — Realizing a finite Gram matrix in a represented CAR corner · 12 — An irreducible CAR representation has no nonzero compact image · 11 — Simplicity of the completed CAR algebra · 5 — The completed CAR algebra is infinite-dimensional
For pure states on CAR, the sequence construction controls both and the actual inverses . The limiting automorphism satisfies . The detailed alternating correction inequalities, the protected inverse images, and the substitution are retained in the key proof Card; this route does not duplicate that proof.
For one fixed approximately inner automorphism, shell matching gives and , where . At the root class , the chosen family uses and . Each other component uses one automorphism for all of its shells. The generic projection-matching theorem is not a new proof of the general KOS proposition. The same chosen homogeneity family is used in the construction of the algebra and in the classification of its irreducible representations.
Read selected Card prerequisites before their uses. Levels are recomputed from the selected reachability-preserving projection; omitted source helpers remain traceable in the source exploration.
No Cards match this search. Clear search to recover this reading scope.
A point-norm approximation followed by close-projection conjugacy gives exact support identities for an arbitrary projection family.
MathlibAnnex.CStarAlgebra.exists_shell_family_of_approximately_inner
Immediate Card prerequisites: None in this selected scope
Used by in this scope: Choosing the CAR shell family from proved homogeneity
One family records a transporting automorphism and exact shell links for each selected pure-state class, with an explicitly fixed root component.
MathlibAnnex.CStarAlgebra.CAR.RepresentativeShellFamily
Immediate Card prerequisites: None in this selected scope
Used by in this scope: Choosing the CAR shell family from proved homogeneity
Names the completed CAR algebra in which finite matrix calculations can be extended by norm approximation.
MathlibAnnex.CStarAlgebra.CAR.Limit
Immediate Card prerequisites: None in this selected scope
Used by in this scope: The product-vector state on the completed CAR algebra · Approximately inner homogeneity of pure CAR states · A finite-row average centralizes its matrix stage · The decreasing root projections in the CAR completion · The completed CAR algebra is infinite-dimensional · A two-sided inner intertwining sequence for two states
An inner sequence records both forward and actual inverse convergence data before any limiting automorphism is constructed.
MathlibAnnex.CStarAlgebra.CAR.HasInnerIntertwiningSequence
Immediate Card prerequisites: The CAR algebra as a completion of finite matrix stages
Used by in this scope: Two-sided inner sequences imply pure-state homogeneity · Pure CAR states admit two-sided inner intertwining sequences
The homogeneity property asks for exact state transport by an automorphism that is locally approximable by inner automorphisms.
MathlibAnnex.CStarAlgebra.CAR.PureStateHomogeneity
Immediate Card prerequisites: The CAR algebra as a completion of finite matrix stages
Used by in this scope: Two-sided inner sequences imply pure-state homogeneity
Compatible evaluation at the distinguished matrix coordinate extends continuously to the CAR completion.
MathlibAnnex.CStarAlgebra.CAR.rootState
Immediate Card prerequisites: The CAR algebra as a completion of finite matrix stages
Used by in this scope: Root compression becomes scalar in norm · Purity of the completed root state
Rules out finite dimension by retaining matrix subalgebras of unbounded dimension.
MathlibAnnex.CStarAlgebra.CAR.not_finiteDimensional
Immediate Card prerequisites: The CAR algebra as a completion of finite matrix stages
Used by in this scope: An irreducible CAR representation has no nonzero compact image
The distinguished stage corners give a nested sequence of projections supporting the root state.
MathlibAnnex.CStarAlgebra.CAR.rootFlag
Immediate Card prerequisites: The CAR algebra as a completion of finite matrix stages
Used by in this scope: Root compression becomes scalar in norm
Turns an arbitrary element of the completed CAR algebra into one commuting with a prescribed finite matrix stage.
MathlibAnnex.CStarAlgebra.CAR.ofStage_commute_rowAverage
Immediate Card prerequisites: The CAR algebra as a completion of finite matrix stages
Used by in this scope: Exact vector transport along an almost central unitary path · Approximating another vector state along a unitary path
The forward and inverse limits close the homogeneity argument once an intertwining sequence is supplied for every pure-state pair.
MathlibAnnex.CStarAlgebra.CAR.homogeneity_of_innerIntertwiningSequences
Immediate Card prerequisites: Approximately inner homogeneity of pure CAR states · A two-sided inner intertwining sequence for two states
Used by in this scope: Pure-state homogeneity of the completed CAR algebra
Extends an exact rank-one compression identity on finite stages to a pointwise norm limit on the completed algebra.
MathlibAnnex.CStarAlgebra.CAR.tendsto_norm_compressionError
Immediate Card prerequisites: The product-vector state on the completed CAR algebra · The decreasing root projections in the CAR completion
Used by in this scope: Simplicity of the completed CAR algebra
Passes extremality of the root vector states from every finite matrix stage to the completed CAR algebra.
MathlibAnnex.CStarAlgebra.CAR.isPureState_rootState
Immediate Card prerequisites: The product-vector state on the completed CAR algebra
Used by in this scope: Choosing the CAR shell family from proved homogeneity
Every nonzero closed two-sided ideal of the CAR algebra contains the identity.
MathlibAnnex.CStarAlgebra.CAR.isSimpleCStarAlgebra_limit
Immediate Card prerequisites: Root compression becomes scalar in norm
Used by in this scope: An irreducible CAR representation has no nonzero compact image
Simplicity and infinite dimensionality rule out compact operators coming from nonzero CAR elements.
MathlibAnnex.CStarAlgebra.CAR.eq_zero_of_isCompactOperator_image
Immediate Card prerequisites: Simplicity of the completed CAR algebra · The completed CAR algebra is infinite-dimensional
Used by in this scope: Lifting a corner involution to an ambient CAR unitary · Realizing a finite Gram matrix in a represented CAR corner
A prescribed unitary involution on a represented root corner can be realized on finitely many vectors by one lifted corner exponential.
MathlibAnnex.CStarAlgebra.CAR.exists_liftedCornerExponential_apply_eq_involution
Immediate Card prerequisites: An irreducible CAR representation has no nonzero compact image
Used by in this scope: Exact vector transport along an almost central unitary path · Approximating another vector state along a unitary path
The infinite-dimensional root corner contains an isometric copy of any finite family of vectors.
MathlibAnnex.CStarAlgebra.CAR.exists_rootCornerFamily_with_gram
Immediate Card prerequisites: An irreducible CAR representation has no nonzero compact image
Used by in this scope: Purifying a vector state on a finite CAR stage
Every finite-stage restriction of a unit vector state can be realized by a unit vector in any irreducible CAR representation.
MathlibAnnex.CStarAlgebra.CAR.exists_unitVector_vectorFunctional_eq_on_stage
Immediate Card prerequisites: Realizing a finite Gram matrix in a represented CAR corner
Used by in this scope: Approximating another vector state along a unitary path · Cross-representation state approximation with a protected finite set
Finite matrix-state tests ensure exact transport while protecting a prescribed finite set throughout the path.
MathlibAnnex.CStarAlgebra.CAR.exists_stageTests_exact_unitary_path_apply_eq_and_conjugate_sub_norm_lt
Immediate Card prerequisites: Lifting a corner involution to an ambient CAR unitary · A finite-row average centralizes its matrix stage
Used by in this scope: Cross-representation state approximation with a protected finite set
A fixed irreducible CAR representation can approximate any vector state on finitely many elements by moving a given unit vector.
MathlibAnnex.CStarAlgebra.CAR.exists_unitary_crossRepresentation_path_approx
Immediate Card prerequisites: Purifying a vector state on a finite CAR stage · Lifting a corner involution to an ambient CAR unitary · A finite-row average centralizes its matrix stage
Used by in this scope: Pure CAR states admit two-sided inner intertwining sequences
Finite entrywise tests allow new state approximation while an entire unitary path nearly fixes earlier data.
MathlibAnnex.CStarAlgebra.CAR.exists_stageTests_crossRepresentation_path_approx
Immediate Card prerequisites: Purifying a vector state on a finite CAR stage · Exact vector transport along an almost central unitary path
Used by in this scope: Pure CAR states admit two-sided inner intertwining sequences
Finite-set vector-state transport supplies explicit corrections; their summable conjugation bounds and state estimates yield the required two-sided sequence.
MathlibAnnex.CStarAlgebra.CAR.hasInnerIntertwiningSequence_of_pure
Immediate Card prerequisites: Approximating another vector state along a unitary path · Cross-representation state approximation with a protected finite set · A two-sided inner intertwining sequence for two states
Used by in this scope: Pure-state homogeneity of the completed CAR algebra
The constructed inner intertwining sequences discharge the supplier hypothesis and give an approximately inner transporting automorphism.
MathlibAnnex.CStarAlgebra.CAR.homogeneity
Immediate Card prerequisites: Two-sided inner sequences imply pure-state homogeneity · Pure CAR states admit two-sided inner intertwining sequences
Used by in this scope: Choosing the CAR shell family from proved homogeneity
CAR homogeneity and exact shell matching supply one family whose distinguished component is fixed by an explicit identity choice.
MathlibAnnex.CStarAlgebra.CAR.homogeneityShellFamily
Immediate Card prerequisites: Purity of the completed root state · Exact projection links for one approximately inner automorphism · A fixed representative family of CAR shell data · Pure-state homogeneity of the completed CAR algebra
Used by in this scope: None in this selected scope