Back to Project mathematical routes
The chosen homogeneity family defines one fixed unital simple infinite-dimensional algebra with a unique nonzero irreducible representation class. It also has a faithful representation on a separable trace space but no nonzero separable irreducible representation.
7 direct Cards + 54 reused prerequisites = 61 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: 60 — The C*-algebra generated by the CAR representation and the shell unitaries · 62 — A simple C*-algebra with a unique irreducible representation class · 61 — The ambient representation of the fixed algebra · 63 — The fixed algebra on the CAR trace Hilbert space · 64 — Faithfulness of the representation on the CAR trace Hilbert space · 65 — No nonzero irreducible representation on a separable Hilbert space · 66 — A separably represented C*-algebra with no separable irreducible representation
Reused prerequisites: 38 — The atomic common range is one embedded GNS line · 14 — Purifying a vector state on a finite CAR stage · 43 — The ambient inclusion of the fixed shell-family target · 3 — The product-vector state on the completed CAR algebra · 26 — Choosing the CAR shell family from proved homogeneity · 19 — Approximately inner homogeneity of pure CAR states · 57 — The target represented on the CAR trace GNS space · 55 — The GNS representation of the target trace extension · 10 — Root compression becomes scalar in norm · 27 — The selected GNS representation of a pure-state class · 36 — The matching GNS fiber retains exactly its cyclic line · 28 — Distinct GNS classes have no unitary intertwiner · 49 — The shell-generated algebra is not an algebra of all compact operators · 50 — Structural properties of one shell-generated C*-algebra · 56 — Faithfulness of the target-state GNS representation · 29 — The atomic direct sum of the selected CAR representations · 15 — Lifting a corner involution to an ambient CAR unitary · 16 — Exact vector transport along an almost central unitary path · 46 — Every irreducible representation is unitarily equivalent to the inclusion · 33 — Realizing a shell family by a faithful irreducible operator algebra · 42 — The CAR source map into the fixed shell-family target · 34 — Shell matching fixes the trace of transported flags · 1 — The normalized trace on a finite CAR stage · 35 — Transported flags vanish on vectors generated by a trace vector · 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 · 48 — Closed-ideal simplicity of the shell-generated algebra · 4 — Purity of the completed root state · 30 — An irreducible operator algebra constructed from projection shells · 51 — Extending the CAR trace to the fixed shell target · 7 — Constructing the normalized trace on the completed CAR algebra · 2 — The CAR algebra as a completion of finite matrix stages · 37 — An inequivalent GNS fiber has no residual common range · 21 — Two-sided inner sequences imply pure-state homogeneity · 40 — An irreducible target representation has a surviving fixed space · 39 — Reconstructing a represented unitary from its shells and residual corner · 24 — Exact projection links for one approximately inner automorphism · 25 — A fixed representative family of CAR shell data · 58 — Faithfulness of the representation on the CAR trace Hilbert space · 47 — Unitary equivalence without an initial unitality assumption · 22 — Pure CAR states admit two-sided inner intertwining sequences · 13 — Realizing a finite Gram matrix in a represented CAR corner · 31 — The atomic-shell construction on selected pure-GNS fibers · 32 — The closed operator algebra generated by a representation and extra operators · 12 — An irreducible CAR representation has no nonzero compact image · 45 — The cyclic sum fills every irreducible target representation · 11 — Simplicity of the completed CAR algebra · 23 — Pure-state homogeneity of the completed CAR algebra · 5 — The completed CAR algebra is infinite-dimensional · 20 — A two-sided inner intertwining sequence for two states · 41 — A common root vector realizes every selected state through the generators · 44 — Assembling selected GNS cyclic subspaces into an isometric source representation
Specialize the supplied family to the once-chosen homogeneity family. The algebra remains , with inclusion . The structural theorem gives its faithful irreducible inclusion and the unique nonzero irreducible representation class, including possibly nonunital inputs.
The same acts faithfully on the separable CAR trace space by . It has no nonzero irreducible representation on a separable Hilbert space. The proof first establishes unit preservation and composes the two classification unitaries in the direction before applying the finite-dimensionality theorem. This does not rule out its irreducible inclusion on the nonseparable atomic space.
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 choice of representative pure states, fixed literally at a root, gives one concrete GNS representation per equivalence class.
MathlibAnnex.CStarAlgebra.PureState.selectedRepresentation
Immediate Card prerequisites: None in this selected scope
Used by in this scope: The matching GNS fiber retains exactly its cyclic line · Distinct GNS classes have no unitary intertwiner · The atomic direct sum of the selected CAR representations
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
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 · Constructing the normalized trace on the completed CAR algebra · The completed CAR algebra is infinite-dimensional · A two-sided inner intertwining sequence for two states
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 · The matching GNS fiber retains exactly its cyclic line · Shell matching fixes the trace of transported flags · An inequivalent GNS fiber has no residual common range · Reconstructing a represented unitary from its shells and residual corner · Assembling selected GNS cyclic subspaces into an isometric source representation
Places a represented algebra and a chosen family of bounded operators in one concrete closed algebra.
MathlibAnnex.CStarAlgebra.AtomicConstruction.concreteTarget
Immediate Card prerequisites: None in this selected scope
Used by in this scope: An irreducible operator algebra constructed from projection shells · Reconstructing a represented unitary from its shells and residual corner
The normalized matrix trace provides a positive tracial functional compatible with the CAR inclusions.
MathlibAnnex.CStarAlgebra.CAR.stageTrace
Immediate Card prerequisites: None in this selected scope
Used by in this scope: Constructing the normalized trace on the completed CAR algebra
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
Carries compatible bounded matrix traces through the algebraic limit, normed union and completion.
MathlibAnnex.CStarAlgebra.CAR.trace
Immediate Card prerequisites: The normalized trace on a finite CAR stage · The CAR algebra as a completion of finite matrix stages
Used by in this scope: Shell matching fixes the trace of transported flags · Extending the CAR trace to the fixed shell target
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: The shell-generated algebra is not an algebra of all compact operators · An irreducible CAR representation has no nonzero compact image
Shell partial isometries with rank-one limiting defects can be completed to unitary links that join inequivalent irreducible fibers.
MathlibAnnex.CStarAlgebra.AtomicConstruction.exists_irreducible_atomicShellModel
Immediate Card prerequisites: The closed operator algebra generated by a representation and extra operators
Used by in this scope: The atomic-shell construction on selected pure-GNS fibers
The class index makes the selected pure-GNS family pairwise unitarily inequivalent.
MathlibAnnex.CStarAlgebra.PureState.no_unitaryIntertwiner_selectedRepresentation
Immediate Card prerequisites: The selected GNS representation of a pure-state class
Used by in this scope: An inequivalent GNS fiber has no residual common range · The atomic-shell construction on selected pure-GNS fibers · Assembling selected GNS cyclic subspaces into an isometric source representation
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 · Shell matching fixes the trace of transported flags · Reconstructing a represented unitary from its shells and residual corner
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
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
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: The matching GNS fiber retains exactly its cyclic line · An inequivalent GNS fiber has no residual common range · Simplicity of the completed CAR algebra · A common root vector realizes every selected state through the generators · Assembling selected GNS cyclic subspaces into an isometric source representation
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 · The matching GNS fiber retains exactly its cyclic line · The atomic direct sum of the selected CAR representations · An inequivalent GNS fiber has no residual common range
Pure-state GNS data supplies the irreducible and inequivalent fibers required by the generic shell construction.
MathlibAnnex.CStarAlgebra.AtomicConstruction.exists_irreducible_pureAtomicShellModel
Immediate Card prerequisites: Distinct GNS classes have no unitary intertwiner · An irreducible operator algebra constructed from projection shells
Used by in this scope: Realizing a shell family by a faithful irreducible operator algebra
Recovers exact trace values from the initial and final supports of shell links.
MathlibAnnex.CStarAlgebra.CAR.trace_transportedFlag
Immediate Card prerequisites: The decreasing root projections in the CAR completion · Constructing the normalized trace on the completed CAR algebra · A fixed representative family of CAR shell data
Used by in this scope: Transported flags vanish on vectors generated by a trace vector
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
All selected pure-GNS fibers of the completed CAR algebra act together on one Hilbert direct sum.
MathlibAnnex.CStarAlgebra.CAR.selectedAtomicRepresentation
Immediate Card prerequisites: The selected GNS representation of a pure-state class · Purity of the completed root state
Used by in this scope: Realizing a shell family by a faithful irreducible operator algebra · Reconstructing a represented unitary from its shells and residual corner · Assembling selected GNS cyclic subspaces into an isometric source representation
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
Identifies the residual projection of a transported CAR flag in its matching pure-state representation.
MathlibAnnex.CStarAlgebra.CAR.selected_commonFixedProjection_eq_rankOne
Immediate Card prerequisites: Root compression becomes scalar in norm · The selected GNS representation of a pure-state class · Purity of the completed root state · A fixed representative family of CAR shell data
Used by in this scope: The atomic common range is one embedded GNS line
Turns decay of projection traces into norm convergence on each source-orbit vector.
MathlibAnnex.CStarAlgebra.CAR.tendsto_transportedFlag_orbit_zero
Immediate Card prerequisites: Shell matching fixes the trace of transported flags
Used by in this scope: The target represented on the CAR trace GNS space
Uses compression and cyclic transport to exclude fixed vectors in every other chosen pure-state class.
MathlibAnnex.CStarAlgebra.CAR.selected_commonFixedProjection_eq_zero
Immediate Card prerequisites: Root compression becomes scalar in norm · Distinct GNS classes have no unitary intertwiner · Purity of the completed root state · A fixed representative family of CAR shell data
Used by in this scope: The atomic common range is one embedded GNS line
Assembles the matching and inequivalent fiber calculations in an arbitrary Hilbert direct sum.
MathlibAnnex.CStarAlgebra.CAR.iInf_range_atomic_transportedFlag_eq_span
Immediate Card prerequisites: The matching GNS fiber retains exactly its cyclic line · An inequivalent GNS fiber has no residual common range
Used by in this scope: Every irreducible representation is unitarily equivalent to the inclusion · Realizing a shell family by a faithful irreducible operator algebra
Joins mutually orthogonal pure-state cyclic copies and controls the limiting flag projections on their sum.
MathlibAnnex.CStarAlgebra.CAR.exists_selectedAtomicCyclicIsometry
Immediate Card prerequisites: Root compression becomes scalar in norm · Distinct GNS classes have no unitary intertwiner · The atomic direct sum of the selected CAR representations · A fixed representative family of CAR shell data
Used by in this scope: The cyclic sum fills every irreducible target representation
Separates a represented generator into a strong shell sum and the exact operator between its limiting fixed spaces.
MathlibAnnex.CStarAlgebra.CAR.exists_targetShellReconstruction
Immediate Card prerequisites: The atomic direct sum of the selected CAR representations · The decreasing root projections in the CAR completion · A fixed representative family of CAR shell data · The closed operator algebra generated by a representation and extra operators
Used by in this scope: The target represented on the CAR trace GNS space · An irreducible target representation has a surviving fixed space
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
Constructs unitary links between pure-state summands and an irreducible algebra containing a faithful copy of CAR.
MathlibAnnex.CStarAlgebra.CAR.exists_completedAtomicShellModel
Immediate Card prerequisites: The atomic common range is one embedded GNS line · The atomic direct sum of the selected CAR representations · The atomic-shell construction on selected pure-GNS fibers
Used by in this scope: The ambient inclusion of the fixed shell-family target · The CAR source map into the fixed shell-family target · The C*-algebra generated by the CAR representation and the shell unitaries
Rules out simultaneous disappearance of all limiting CAR flags by passing reduction through the reconstructed generators.
MathlibAnnex.CStarAlgebra.CAR.exists_nonzero_targetFixedSpace
Immediate Card prerequisites: Reconstructing a represented unitary from its shells and residual corner
Used by in this scope: A common root vector realizes every selected state through the generators
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
Builds a compatible family of unit vectors from a surviving residual space and identifies their CAR vector states.
MathlibAnnex.CStarAlgebra.CAR.exists_targetDefectVectorFamily
Immediate Card prerequisites: Root compression becomes scalar in norm · An irreducible target representation has a surviving fixed space
Used by in this scope: The cyclic sum fills every irreducible target representation
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
Restricting the codomain of the selected atomic representation gives the source map into one fixed generated target.
MathlibAnnex.CStarAlgebra.CAR.shellFamilySourceHom
The same concrete target has a literal representation on the selected atomic Hilbert space.
MathlibAnnex.CStarAlgebra.CAR.shellFamilyInclusion
Immediate Card prerequisites: Realizing a shell family by a faithful irreducible operator algebra
Used by in this scope: The ambient representation of the fixed algebra · Closed-ideal simplicity of the shell-generated algebra · Unitary equivalence without an initial unitality assumption
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
Excludes an injective representation of the infinite-dimensional unital algebra onto all compact operators.
MathlibAnnex.CStarAlgebra.CAR.not_isCompactOperatorModel_shellFamilyTarget
Immediate Card prerequisites: The CAR source map into the fixed shell-family target · The completed CAR algebra is infinite-dimensional
Used by in this scope: Structural properties of one shell-generated C*-algebra
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
The source trace first becomes a state on the existing target algebra.
MathlibAnnex.CStarAlgebra.CAR.exists_state_extension_trace
Immediate Card prerequisites: The CAR source map into the fixed shell-family target · Constructing the normalized trace on the completed CAR algebra
Used by in this scope: The GNS representation of the target trace extension
Uses shell reconstruction and residual lines to turn an isometric CAR intertwiner into a unitary equivalence on the source.
MathlibAnnex.CStarAlgebra.CAR.exists_surjective_selectedAtomicCyclicIsometry
Extends the unitary equivalence from the CAR source to all additional generators and the norm-closed target.
MathlibAnnex.CStarAlgebra.CAR.ambientInclusion_unitaryEquivalent
Immediate Card prerequisites: The atomic common range is one embedded GNS line · The cyclic sum fills every irreducible target representation
Used by in this scope: Closed-ideal simplicity of the shell-generated algebra · Unitary equivalence without an initial unitality assumption
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 chosen state on the existing target supplies its cyclic GNS representation.
MathlibAnnex.CStarAlgebra.CAR.tracialRepresentation
Immediate Card prerequisites: Extending the CAR trace to the fixed shell target
Used by in this scope: The target represented on the CAR trace GNS space · Faithfulness of the target-state GNS representation
A fixed pointed unitary transports the target action onto the Hilbert space constructed from CAR alone.
MathlibAnnex.CStarAlgebra.CAR.traceModelRepresentation
Immediate Card prerequisites: The GNS representation of the target trace extension · Transported flags vanish on vectors generated by a trace vector · Reconstructing a represented unitary from its shells and residual corner
Used by in this scope: The fixed algebra on the CAR trace Hilbert space · Faithfulness of the representation on the CAR trace Hilbert space
Shows why allowing nonunital input representations does not enlarge the irreducible representation class of the shell-generated algebra.
MathlibAnnex.CStarAlgebra.CAR.shellFamilyInclusion_unitaryEquivalent_nonUnital
Immediate Card prerequisites: The ambient inclusion of the fixed shell-family target · Every irreducible representation is unitarily equivalent to the inclusion
Used by in this scope: Structural properties of one shell-generated C*-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
Uses a faithful irreducible representation in the unique unitary-equivalence class to rule out proper nonzero closed two-sided ideals.
MathlibAnnex.CStarAlgebra.CAR.isSimpleCStarAlgebra_shellFamilyTarget
Immediate Card prerequisites: 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 scope: Structural properties of one shell-generated C*-algebra · Faithfulness of the target-state GNS representation
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: A simple C*-algebra with a unique irreducible representation class · The C*-algebra generated by the CAR representation and the shell unitaries
Collects the proved properties of a single generated algebra, keeping the shell-family input separate from its consequences.
MathlibAnnex.CStarAlgebra.CAR.shellFamilyEndpoint
Immediate Card prerequisites: 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 scope: A simple C*-algebra with a unique irreducible representation class
The ideal dichotomy of the same target forces the constructed nonzero representation to be injective.
MathlibAnnex.CStarAlgebra.CAR.tracialRepresentation_injective
Immediate Card prerequisites: The GNS representation of the target trace extension · Closed-ideal simplicity of the shell-generated algebra
Used by in this scope: Faithfulness of the representation on the CAR trace Hilbert space
Defines the single algebra used in the irreducible and separable faithful representations.
MathlibAnnex.CStarAlgebra.CAR.AtomicCounterexampleAlgebra
Immediate Card prerequisites: Choosing the CAR shell family from proved homogeneity · Realizing a shell family by a faithful irreducible operator algebra
Used by in this scope: The fixed algebra on the CAR trace Hilbert space · The ambient representation of the fixed algebra
Establishes the properties that make the fixed algebra a counterexample to Naimark’s problem.
MathlibAnnex.CStarAlgebra.CAR.atomicCounterexampleEndpoint
Immediate Card prerequisites: Choosing the CAR shell family from proved homogeneity · Structural properties of one shell-generated C*-algebra
Used by in this scope: No nonzero irreducible representation on a separable Hilbert space
Unitary conjugation preserves injectivity of the target-state representation.
MathlibAnnex.CStarAlgebra.CAR.traceModelRepresentation_injective
Immediate Card prerequisites: The target represented on the CAR trace GNS space · Faithfulness of the target-state GNS representation
Used by in this scope: Faithfulness of the representation on the CAR trace Hilbert space
Defines a representation of the same algebra on the GNS Hilbert space of the CAR trace.
MathlibAnnex.CStarAlgebra.CAR.separableCounterexampleRepresentation
Immediate Card prerequisites: The target represented on the CAR trace GNS space · The C*-algebra generated by the CAR representation and the shell unitaries
Used by in this scope: Faithfulness of the representation on the CAR trace Hilbert space
Defines the inclusion representation .
MathlibAnnex.CStarAlgebra.CAR.atomicCounterexampleRepresentation
Immediate Card prerequisites: The ambient inclusion of the fixed shell-family target · The C*-algebra generated by the CAR representation and the shell unitaries
Used by in this scope: No nonzero irreducible representation on a separable Hilbert space
Proves that the representation is injective.
MathlibAnnex.CStarAlgebra.CAR.separableCounterexampleRepresentation_injective
Immediate Card prerequisites: The fixed algebra on the CAR trace Hilbert space · Faithfulness of the representation on the CAR trace Hilbert space
Used by in this scope: A separably represented C*-algebra with no separable irreducible representation
Rules out irreducible representations of on separable Hilbert spaces by the finite-dimensionality theorem for a single irreducible representation class.
MathlibAnnex.CStarAlgebra.CAR.not_isIrreducible_of_separable
Immediate Card prerequisites: The ambient representation of the fixed algebra · A simple C*-algebra with a unique irreducible representation class
Used by in this scope: A separably represented C*-algebra with no separable irreducible representation
The same algebra has a faithful representation on a separable Hilbert space, but no nonzero irreducible representation on any separable Hilbert space.
MathlibAnnex.CStarAlgebra.CAR.atomicCounterexampleEndpoint_and_exists_separable_faithful_representation_and_no_separable_irreducible_representation
Immediate Card prerequisites: No nonzero irreducible representation on a separable Hilbert space · Faithfulness of the representation on the CAR trace Hilbert space
Used by in this scope: None in this selected scope