Preserved earlier 68-Card presentation and source/provider boundary. The earlier 466-declaration source view is linked below; the 68-node Card graph is not a full-native declaration count.Return to selected Card readingReturn to current selected Card reading
The mathematical goal
A single unital, simple, infinite-dimensional C*-algebra has one unitary-equivalence class of nonzero irreducible representations and a faithful tracial representation on a separable Hilbert space. The normalized trace of its CAR subalgebra extends uniquely among all states of the same generated algebra.
Exact source: MathlibAnnex v0.4.0 Project entry · Source manifest
Scope
The principal construction concerns complex C*-algebras and nonzero irreducible representations. Its fixed algebra and separable faithful tracial representation require no CH hypothesis. CH enters only in the statement equating the continuum with aleph one and the corresponding density-character existence result. The general reverse density obstruction also allows nonunital algebras.
68 selected Declaration Cards form this Companion, with 1,044 dependency relations, 122 displayed edges and levels 0–15. The CH consequence is a separate route reusing two density Cards.
Mathematical routes
CAR foundations and canonical states
12 Cards · levels 0–4
Finite-stage purification and local transport
6 Cards · levels 0–2
Pure-state homogeneity and shell matching
8 Cards · levels 0–3
Direct sums of GNS representations and shell unitaries
7 Cards · levels 0–3
Fixed subspaces and reconstruction of the generators
8 Cards · levels 0–2
Unitary equivalence of irreducible representations
9 Cards · levels 0–4
Trace extensions and faithful representations on a separable space
9 Cards · levels 0–3
One C*-algebra and its representation-theoretic properties
7 Cards · levels 0–3
Density and cardinality
2 Cards · levels 0–1
CH and the existence of a counterexample of norm density aleph one
3 Cards · levels 0–2
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 normalized trace on a finite CAR stage
MathlibAnnex.CStarAlgebra.CAR.stageTrace
The normalized matrix trace provides a positive tracial functional compatible with the CAR inclusions.
Immediate prerequisites in this Project
None in this scope
Used by in this Project
Constructing the normalized trace on the completed CAR algebra
The CAR algebra as a completion of finite matrix stages
MathlibAnnex.CStarAlgebra.CAR.Limit
Names the completed CAR algebra in which finite matrix calculations can be extended by norm approximation.
Immediate prerequisites in this Project
None in this scope
Used by in this Project
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
Exact projection links for one approximately inner automorphism
MathlibAnnex.CStarAlgebra.exists_shell_family_of_approximately_inner
A point-norm approximation followed by close-projection conjugacy gives exact support identities for an arbitrary projection family.
Immediate prerequisites in this Project
None in this scope
Used by in this Project
Choosing the CAR shell family from proved homogeneity
A fixed representative family of CAR shell data
MathlibAnnex.CStarAlgebra.CAR.RepresentativeShellFamily
One family records a transporting automorphism and exact shell links for each selected pure-state class, with an explicitly fixed root component.
Immediate prerequisites in this Project
None in this scope
Used by in this Project
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
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
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
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, Reconstructing a represented unitary from its shells and residual corner
Level 1
The product-vector state on the completed CAR algebra
MathlibAnnex.CStarAlgebra.CAR.rootState
Compatible evaluation at the distinguished matrix coordinate extends continuously to the CAR completion.
Immediate prerequisites in this Project
The CAR algebra as a completion of finite matrix stages
Used by in this Project
Root compression becomes scalar in norm, Purity of the completed root state
The completed CAR algebra is infinite-dimensional
MathlibAnnex.CStarAlgebra.CAR.not_finiteDimensional
Rules out finite dimension by retaining matrix subalgebras of unbounded dimension.
Immediate prerequisites in this Project
The CAR algebra as a completion of finite matrix stages
Used by in this Project
The shell-generated algebra is not an algebra of all compact operators, An irreducible CAR representation has no nonzero compact image
A finite-row average centralizes its matrix stage
MathlibAnnex.CStarAlgebra.CAR.ofStage_commute_rowAverage
Turns an arbitrary element of the completed CAR algebra into one commuting with a prescribed finite matrix stage.
Immediate prerequisites in this Project
The CAR algebra as a completion of finite matrix stages
Used by in this Project
Exact vector transport along an almost central unitary path, Approximating another vector state along a unitary path
Constructing the normalized trace on the completed CAR algebra
MathlibAnnex.CStarAlgebra.CAR.trace
Carries compatible bounded matrix traces through the algebraic limit, normed union and completion.
Immediate prerequisites in this Project
The normalized trace on a finite CAR stage, The CAR algebra as a completion of finite matrix stages
Used by in this Project
Shell matching fixes the trace of transported flags, Extending the CAR trace to the fixed shell target, Normalization and the trace identity determine the CAR trace
The decreasing root projections in the CAR completion
MathlibAnnex.CStarAlgebra.CAR.rootFlag
The distinguished stage corners give a nested sequence of projections supporting the root state.
Immediate prerequisites in this Project
The CAR algebra as a completion of finite matrix stages
Used by in this Project
Root compression becomes scalar in norm, Shell matching fixes the trace of transported flags, Reconstructing a represented unitary from its shells and residual corner
Approximately inner homogeneity of pure CAR states
MathlibAnnex.CStarAlgebra.CAR.PureStateHomogeneity
The homogeneity property asks for exact state transport by an automorphism that is locally approximable by inner automorphisms.
Immediate prerequisites in this Project
The CAR algebra as a completion of finite matrix stages
Used by in this Project
Two-sided inner sequences imply pure-state homogeneity
A two-sided inner intertwining sequence for two states
MathlibAnnex.CStarAlgebra.CAR.HasInnerIntertwiningSequence
An inner sequence records both forward and actual inverse convergence data before any limiting automorphism is constructed.
Immediate prerequisites in this Project
The CAR algebra as a completion of finite matrix stages
Used by in this Project
Two-sided inner sequences imply pure-state homogeneity, Pure CAR states admit two-sided inner intertwining sequences
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
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
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
Purity of the completed root state
MathlibAnnex.CStarAlgebra.CAR.isPureState_rootState
Passes extremality of the root vector states from every finite matrix stage to the completed CAR algebra.
Immediate prerequisites in this Project
The product-vector state on the completed CAR algebra
Used by in this Project
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
Normalization and the trace identity determine the CAR trace
MathlibAnnex.CStarAlgebra.CAR.eq_trace_of_apply_one_of_mul_comm
Proves uniqueness without assuming positivity of the competing continuous functional.
Immediate prerequisites in this Project
Constructing the normalized trace on the completed CAR algebra
Used by in this Project
The fixed shell target has a unique tracial state
Root compression becomes scalar in norm
MathlibAnnex.CStarAlgebra.CAR.tendsto_norm_compressionError
Extends an exact rank-one compression identity on finite stages to a pointwise norm limit on the completed algebra.
Immediate prerequisites in this Project
The product-vector state on the completed CAR algebra, The decreasing root projections in the CAR completion
Used by in this Project
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
Two-sided inner sequences imply pure-state homogeneity
MathlibAnnex.CStarAlgebra.CAR.homogeneity_of_innerIntertwiningSequences
The forward and inverse limits close the homogeneity argument once an intertwining sequence is supplied for every pure-state pair.
Immediate prerequisites in this Project
Approximately inner homogeneity of pure CAR states, A two-sided inner intertwining sequence for two states
Used by in this Project
Pure-state homogeneity of the completed CAR algebra
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
Shell matching fixes the trace of transported flags
MathlibAnnex.CStarAlgebra.CAR.trace_transportedFlag
Recovers exact trace values from the initial and final supports of shell links.
Immediate prerequisites in this Project
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 Project
Transported flags vanish on vectors generated by a trace vector
Level 3
Simplicity of the completed CAR algebra
MathlibAnnex.CStarAlgebra.CAR.isSimpleCStarAlgebra_limit
Every nonzero closed two-sided ideal of the CAR algebra contains the identity.
Immediate prerequisites in this Project
Root compression becomes scalar in norm
Used by in this Project
An irreducible CAR representation has no nonzero compact image
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, Purity of the completed root state
Used by in this Project
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
Transported flags vanish on vectors generated by a trace vector
MathlibAnnex.CStarAlgebra.CAR.tendsto_transportedFlag_orbit_zero
Turns decay of projection traces into norm convergence on each source-orbit vector.
Immediate prerequisites in this Project
Shell matching fixes the trace of transported flags
Used by in this Project
The target represented on the CAR trace GNS space, Pointed unitary transport between trace-cyclic target representations
The matching GNS fiber retains exactly its cyclic line
MathlibAnnex.CStarAlgebra.CAR.selected_commonFixedProjection_eq_rankOne
Identifies the residual projection of a transported CAR flag in its matching pure-state representation.
Immediate prerequisites in this Project
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 Project
The atomic common range is one embedded GNS line
An inequivalent GNS fiber has no residual common range
MathlibAnnex.CStarAlgebra.CAR.selected_commonFixedProjection_eq_zero
Uses compression and cyclic transport to exclude fixed vectors in every other chosen pure-state class.
Immediate prerequisites in this Project
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 Project
The atomic common range is one embedded GNS line
Level 4
An irreducible CAR representation has no nonzero compact image
MathlibAnnex.CStarAlgebra.CAR.eq_zero_of_isCompactOperator_image
Simplicity and infinite dimensionality rule out compact operators coming from nonzero CAR elements.
Immediate prerequisites in this Project
Simplicity of the completed CAR algebra, The completed CAR algebra is infinite-dimensional
Used by in this Project
Lifting a corner involution to an ambient CAR unitary, Realizing a finite Gram matrix in a represented CAR corner
The atomic common range is one embedded GNS line
MathlibAnnex.CStarAlgebra.CAR.iInf_range_atomic_transportedFlag_eq_span
Assembles the matching and inequivalent fiber calculations in an arbitrary Hilbert direct sum.
Immediate prerequisites in this Project
The matching GNS fiber retains exactly its cyclic line, An inequivalent GNS fiber has no residual common range
Used by in this Project
Every irreducible representation is unitarily equivalent to the inclusion, Realizing a shell family by a faithful irreducible operator algebra
Reconstructing a represented unitary from its shells and residual corner
MathlibAnnex.CStarAlgebra.CAR.exists_targetShellReconstruction
Separates a represented generator into a strong shell sum and the exact operator between its limiting fixed spaces.
Immediate prerequisites in this Project
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 Project
The target represented on the CAR trace GNS space, Pointed unitary transport between trace-cyclic target representations, An irreducible target representation has a surviving fixed space
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
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 Project
The cyclic sum fills every irreducible target representation
Level 5
Realizing a finite Gram matrix in a represented CAR corner
MathlibAnnex.CStarAlgebra.CAR.exists_rootCornerFamily_with_gram
The infinite-dimensional root corner contains an isometric copy of any finite family of vectors.
Immediate prerequisites in this Project
An irreducible CAR representation has no nonzero compact image
Used by in this Project
Purifying a vector state on a finite CAR stage
Lifting a corner involution to an ambient CAR unitary
MathlibAnnex.CStarAlgebra.CAR.exists_liftedCornerExponential_apply_eq_involution
A prescribed unitary involution on a represented root corner can be realized on finitely many vectors by one lifted corner exponential.
Immediate prerequisites in this Project
An irreducible CAR representation has no nonzero compact image
Used by in this Project
Exact vector transport along an almost central unitary path, Approximating another vector state along a unitary path
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 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 Project
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
An irreducible target representation has a surviving fixed space
MathlibAnnex.CStarAlgebra.CAR.exists_nonzero_targetFixedSpace
Rules out simultaneous disappearance of all limiting CAR flags by passing reduction through the reconstructed generators.
Immediate prerequisites in this Project
Reconstructing a represented unitary from its shells and residual corner
Used by in this Project
A common root vector realizes every selected state through the generators
Level 6
Purifying a vector state on a finite CAR stage
MathlibAnnex.CStarAlgebra.CAR.exists_unitVector_vectorFunctional_eq_on_stage
Every finite-stage restriction of a unit vector state can be realized by a unit vector in any irreducible CAR representation.
Immediate prerequisites in this Project
Realizing a finite Gram matrix in a represented CAR corner
Used by in this Project
Approximating another vector state along a unitary path, Cross-representation state approximation with a protected finite set
Exact vector transport along an almost central unitary path
MathlibAnnex.CStarAlgebra.CAR.exists_stageTests_exact_unitary_path_apply_eq_and_conjugate_sub_norm_lt
Finite matrix-state tests ensure exact transport while protecting a prescribed finite set throughout the path.
Immediate prerequisites in this Project
Lifting a corner involution to an ambient CAR unitary, A finite-row average centralizes its matrix stage
Used by in this Project
Cross-representation state approximation with a protected finite set
A common root vector realizes every selected state through the generators
MathlibAnnex.CStarAlgebra.CAR.exists_targetDefectVectorFamily
Builds a compatible family of unit vectors from a surviving residual space and identifies their CAR vector states.
Immediate prerequisites in this Project
Root compression becomes scalar in norm, An irreducible target representation has a surviving fixed space
Used by in this Project
The cyclic sum fills every irreducible target representation
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
Realizing a shell family by a faithful irreducible operator algebra
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, Pointed unitary transport between trace-cyclic target representations, Extending the CAR trace to the fixed shell target
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
Realizing a shell family by a faithful irreducible operator algebra
Used by in this Project
The ambient representation of the fixed algebra, Closed-ideal simplicity of the shell-generated algebra, Unitary equivalence without an initial unitality assumption
Level 7
Cross-representation state approximation with a protected finite set
MathlibAnnex.CStarAlgebra.CAR.exists_stageTests_crossRepresentation_path_approx
Finite entrywise tests allow new state approximation while an entire unitary path nearly fixes earlier data.
Immediate prerequisites in this Project
Purifying a vector state on a finite CAR stage, Exact vector transport along an almost central unitary path
Used by in this Project
Pure CAR states admit two-sided inner intertwining sequences
Approximating another vector state along a unitary path
MathlibAnnex.CStarAlgebra.CAR.exists_unitary_crossRepresentation_path_approx
A fixed irreducible CAR representation can approximate any vector state on finitely many elements by moving a given unit vector.
Immediate prerequisites in this Project
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 Project
Pure CAR states admit two-sided inner intertwining sequences
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
A common root vector realizes every selected state through the generators, 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, The completed CAR algebra is infinite-dimensional
Used by in this Project
Structural properties of one shell-generated C*-algebra, A Naimark counterexample of continuum norm density
Extending the CAR trace to the fixed shell target
MathlibAnnex.CStarAlgebra.CAR.exists_state_extension_trace
The source trace first becomes a state on the existing target algebra.
Immediate prerequisites in this Project
The CAR source map into the fixed shell-family target, Constructing the normalized trace on the completed CAR algebra
Used by in this Project
The GNS representation of the target trace extension
Pointed unitary transport between trace-cyclic target representations
MathlibAnnex.CStarAlgebra.CAR.exists_pointed_unitary_of_trace_of_cyclic
Source cyclicity and strong shell sums extend the canonical CAR orbit isometry to the whole target.
Immediate prerequisites in this Project
The CAR source map into the fixed shell-family target, Transported flags vanish on vectors generated by a trace vector, Reconstructing a represented unitary from its shells and residual corner
Used by in this Project
The unique trace extension is tracial on the whole target, Uniqueness among all state extensions of the CAR trace
Level 8
Pure CAR states admit two-sided inner intertwining sequences
MathlibAnnex.CStarAlgebra.CAR.hasInnerIntertwiningSequence_of_pure
Finite-set vector-state transport supplies explicit corrections; their summable conjugation bounds and state estimates yield the required two-sided sequence.
Immediate prerequisites in this Project
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 Project
Pure-state homogeneity of the completed CAR algebra
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 atomic common range is one embedded GNS line, 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
The GNS representation of the target trace extension
MathlibAnnex.CStarAlgebra.CAR.tracialRepresentation
The chosen state on the existing target supplies its cyclic GNS representation.
Immediate prerequisites in this Project
Extending the CAR trace to the fixed shell target
Used by in this Project
The target represented on the CAR trace GNS space, Faithfulness of the target-state GNS representation, The unique trace extension is tracial on the whole target, Uniqueness among all state extensions of the CAR trace
Level 9
Pure-state homogeneity of the completed CAR algebra
MathlibAnnex.CStarAlgebra.CAR.homogeneity
The constructed inner intertwining sequences discharge the supplier hypothesis and give an approximately inner transporting automorphism.
Immediate prerequisites in this Project
Two-sided inner sequences imply pure-state homogeneity, Pure CAR states admit two-sided inner intertwining sequences
Used by in this Project
Choosing the CAR shell family from proved homogeneity
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, Faithfulness of the target-state GNS representation
Uniqueness among all state extensions of the CAR trace
MathlibAnnex.CStarAlgebra.CAR.existsUnique_state_extension_trace
Pointed transport identifies arbitrary state extensions before traciality is proved.
Immediate prerequisites in this Project
The GNS representation of the target trace extension, Pointed unitary transport between trace-cyclic target representations
Used by in this Project
None in this scope
The unique trace extension is tracial on the whole target
MathlibAnnex.CStarAlgebra.CAR.traceExtension_mul_comm
Unitary invariance, strong shell sums, and a closed centralizer extend the trace identity beyond the source.
Immediate prerequisites in this Project
The GNS representation of the target trace extension, Pointed unitary transport between trace-cyclic target representations
Used by in this Project
The fixed shell target has a unique tracial state
The target represented on the CAR trace GNS space
MathlibAnnex.CStarAlgebra.CAR.traceModelRepresentation
A fixed pointed unitary transports the target action onto the Hilbert space constructed from CAR alone.
Immediate prerequisites in this Project
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 Project
The fixed algebra on the CAR trace Hilbert space, Faithfulness of the representation on the CAR trace Hilbert space
Level 10
Choosing the CAR shell family from proved homogeneity
MathlibAnnex.CStarAlgebra.CAR.homogeneityShellFamily
CAR homogeneity and exact shell matching supply one family whose distinguished component is fixed by an explicit identity choice.
Immediate prerequisites in this Project
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 Project
A simple C*-algebra with a unique irreducible representation class, The C*-algebra generated by the CAR representation and the shell unitaries
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
A simple C*-algebra with a unique irreducible representation class
The fixed shell target has a unique tracial state
MathlibAnnex.CStarAlgebra.CAR.existsUnique_tracial_state
Every tracial state is forced back to the CAR trace and hence to its unique extension.
Immediate prerequisites in this Project
Normalization and the trace identity determine the CAR trace, The unique trace extension is tracial on the whole target
Used by in this Project
None in this scope
Faithfulness of the target-state GNS representation
MathlibAnnex.CStarAlgebra.CAR.tracialRepresentation_injective
The ideal dichotomy of the same target forces the constructed nonzero representation to be injective.
Immediate prerequisites in this Project
The GNS representation of the target trace extension, Closed-ideal simplicity of the shell-generated algebra
Used by in this Project
Faithfulness of the representation on the CAR trace Hilbert space
Level 11
Faithfulness of the representation on the CAR trace Hilbert space
MathlibAnnex.CStarAlgebra.CAR.traceModelRepresentation_injective
Unitary conjugation preserves injectivity of the target-state representation.
Immediate prerequisites in this Project
The target represented on the CAR trace GNS space, Faithfulness of the target-state GNS representation
Used by in this Project
Faithfulness of the representation on the CAR trace Hilbert space
The C*-algebra generated by the CAR representation and the shell unitaries
MathlibAnnex.CStarAlgebra.CAR.AtomicCounterexampleAlgebra
Defines the single algebra
Immediate prerequisites in this Project
Choosing the CAR shell family from proved homogeneity, Realizing a shell family by a faithful irreducible operator algebra
Used by in this Project
The fixed algebra on the CAR trace Hilbert space, The ambient representation of the fixed algebra
A simple C*-algebra with a unique irreducible representation class
MathlibAnnex.CStarAlgebra.CAR.atomicCounterexampleEndpoint
Establishes the properties that make the fixed algebra
Immediate prerequisites in this Project
Choosing the CAR shell family from proved homogeneity, Structural properties of one shell-generated C*-algebra
Used by in this Project
No nonzero irreducible representation on a separable Hilbert space
Level 12
The ambient representation of the fixed algebra
MathlibAnnex.CStarAlgebra.CAR.atomicCounterexampleRepresentation
Defines the inclusion representation
Immediate prerequisites in this Project
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 Project
No nonzero irreducible representation on a separable Hilbert space
The fixed algebra on the CAR trace Hilbert space
MathlibAnnex.CStarAlgebra.CAR.separableCounterexampleRepresentation
Defines a representation of the same algebra
Immediate prerequisites in this Project
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 Project
Faithfulness of the representation on the CAR trace Hilbert space
Level 13
Faithfulness of the representation on the CAR trace Hilbert space
MathlibAnnex.CStarAlgebra.CAR.separableCounterexampleRepresentation_injective
Proves that the representation
Immediate prerequisites in this Project
The fixed algebra on the CAR trace Hilbert space, Faithfulness of the representation on the CAR trace Hilbert space
Used by in this Project
Exact norm density of the fixed atomic algebra, A separably represented C*-algebra with no separable irreducible representation
No nonzero irreducible representation on a separable Hilbert space
MathlibAnnex.CStarAlgebra.CAR.not_isIrreducible_of_separable
Rules out irreducible representations of
Immediate prerequisites in this Project
The ambient representation of the fixed algebra, A simple C*-algebra with a unique irreducible representation class
Used by in this Project
A separably represented C*-algebra with no separable irreducible representation
Level 14
A separably represented C*-algebra with no separable irreducible representation
MathlibAnnex.CStarAlgebra.CAR.atomicCounterexampleEndpoint_and_exists_separable_faithful_representation_and_no_separable_irreducible_representation
The same algebra
Immediate prerequisites in this Project
No nonzero irreducible representation on a separable Hilbert space, Faithfulness of the representation on the CAR trace Hilbert space
Used by in this Project
None in this scope
Exact norm density of the fixed atomic algebra
MathlibAnnex.CStarAlgebra.CAR.hasDensityCharacter_atomicCounterexampleAlgebra
Combines a cardinality bound from a faithful representation on a separable Hilbert space with a lower bound for every norm-dense subset.
Immediate prerequisites in this Project
Faithfulness of the representation on the CAR trace Hilbert space
Used by in this Project
A Naimark counterexample of continuum norm density
Level 15
A Naimark counterexample of continuum norm density
MathlibAnnex.CStarAlgebra.CAR.existsNaimarkCounterexampleOfDensity_continuum
Gives a C*-algebra of norm density
Immediate prerequisites in this Project
Exact norm density of the fixed atomic algebra, The shell-generated algebra is not an algebra of all compact operators
Used by in this Project
None in this scope
Earlier declaration anchors and source traceability
- MathlibAnnex.CStarAlgebra.CAR.Stage — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.stepIndexEquiv — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.transportBudget — earlier Project view
- MathlibAnnex.CStarAlgebra.IsSimpleCStarAlgebra — earlier Project view
- MathlibAnnex.CStarAlgebra.exists_shell_of_approximately_inner — earlier Project view
- MathlibAnnex.CStarAlgebra.stateSpace — earlier Project view
- MathlibAnnex.CStarAlgebra.AtomicConstruction.ambientInclusion — earlier Project view
- MathlibAnnex.CStarAlgebra.AtomicConstruction.concreteTarget.instIsClosed — earlier Project view
- MathlibAnnex.CStarAlgebra.AtomicConstruction.generator — earlier Project view
- MathlibAnnex.CStarAlgebra.AtomicConstruction.sourceHom — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.ShellFamilyEndpoint — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.amplify — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.finrank_stage — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.matrixUnit — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.rootLinear — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.rootProjection — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.stageFiniteDimensional — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.stageIsSimpleRing — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.stageNontrivial — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.stageTraceLinear — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.summable_transportBudget — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.tendsto_transportBudget_zero — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.transportBudget_pos — earlier Project view
- MathlibAnnex.CStarAlgebra.IsPureState — earlier Project view
- MathlibAnnex.CStarAlgebra.positiveLinearMapOfMemStateSpace — earlier Project view
- MathlibAnnex.CStarAlgebra.AtomicConstruction.ambientInclusion_injective — earlier Project view
- MathlibAnnex.CStarAlgebra.AtomicConstruction.eq_top_of_source_mem_of_generator_mem — earlier Project view
- MathlibAnnex.CStarAlgebra.AtomicConstruction.generator_coe — earlier Project view
- MathlibAnnex.CStarAlgebra.AtomicConstruction.intertwines_concreteTarget_of_generators — earlier Project view
- MathlibAnnex.CStarAlgebra.AtomicConstruction.reduces_concreteTarget_of_generators — earlier Project view
- MathlibAnnex.CStarAlgebra.AtomicConstruction.sourceHom_coe — earlier Project view
- MathlibAnnex.CStarAlgebra.AtomicConstruction.sourceHom_injective — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.amplify_injective — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.matrixUnit_apply — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.matrixUnit_mul_of_ne — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.matrixUnit_mul_same — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.norm_stageTraceLinear_le — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.rootFunctional — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.rootLinear_nonneg — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.rootProjection_mul_mul — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.stageSeparableSpace — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.stage_eq_sum_smul_matrixUnit — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.star_matrixUnit — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.step — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.sum_matrixUnit_diag — earlier Project view
- MathlibAnnex.CStarAlgebra.PureState.SelectedGNS — earlier Project view
- MathlibAnnex.CStarAlgebra.positiveLinearMapOfMemStateSpace_one — earlier Project view
- MathlibAnnex.CStarAlgebra.AtomicConstruction.starAlgHom_ext — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.embed — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.isStarProjection_rootProjection — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.rootFunctional_apply — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.rootFunctional_step — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.rootPositiveFunctional — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.step_injective — earlier Project view
- MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert — earlier Project view
- MathlibAnnex.CStarAlgebra.PureState.selectedVector — earlier Project view
- MathlibAnnex.CStarAlgebra.AtomicConstruction.intertwines_of_source_of_generators — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.embed_refl — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.embed_succ — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.eq_rootFunctional_of_apply_rootProjection_eq_one — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.norm_stageTrace_le — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.norm_step — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.rootPositiveFunctional_one — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.stageTrace_apply — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.stageTrace_mul_comm — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.stageTrace_rootProjection — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.step_rootProjection_mul — earlier Project view
- MathlibAnnex.CStarAlgebra.PureState.norm_selectedVector — earlier Project view
- MathlibAnnex.CStarAlgebra.PureState.selectedEmbedding — earlier Project view
- MathlibAnnex.CStarAlgebra.PureState.selected_vectorFunctional — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.embed_apply — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.isometry_step — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.rootFunctional_embed — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.rootFunctional_mem_stateSpace — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.stageTrace_one — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.stageTrace_star_mul_self_nonneg — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.stageTrace_step — earlier Project view
- MathlibAnnex.CStarAlgebra.PureState.SelectedGNS.instNontrivial — earlier Project view
- MathlibAnnex.CStarAlgebra.PureState.isIrreducible_selectedRepresentation — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.embed_trans — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.isPureState_rootFunctional — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.isometry_stage — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.stageTrace_embed — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.PreCAR — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.embedDirectedSystem — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.AlgCAR — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.toPreCAR — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.algRootLinear — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.algStageHom — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.algTraceLinear — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.isometry_toPreCAR — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.preToAlg — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.toPreCAR_step — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.toPreCAR_embed — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.algToPre — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.algToPre_preToAlg — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.preToAlg_algToPre — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.preAlgEquiv — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.preRing — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.preAlgebra — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.preNorm — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.preStarRing — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.preStarAlgEquiv — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.preStarModule — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.stageHom — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.exists_common_stage — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.stageHom_apply — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.norm_stageHom — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.stageHom_injective — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.preNontrivial — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.preNormedAddCommGroup — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.preNormedRing — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.dense_stageUnion — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.preCStarRing — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.preNormedSpace — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.preSeparableSpace — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.limitNontrivial — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.limitNormedAlgebra — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.limitSeparableSpace — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.limitStar — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.preNormedAlgebra — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.preRootLinear — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.preTraceLinear — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.AlternatingState — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.continuous_limit_star — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.preRootLinear_stage — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.preTraceLinear_stageHom — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.star_coe — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.transportDense — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.AlternatingTransition — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.densePrefix — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.denseRange_transportDense — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.limitContinuousStar — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.limitStarModule — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.norm_preRootLinear_le — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.norm_preTraceLinear_le — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.toLimit — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.limitStarRing — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.mem_densePrefix — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.ofStage — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.preRootFunctional — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.preTrace — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.dense_stageRange — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.innerAt — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.limitCStarRing — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.limitMatrixUnit — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.ofStage_apply — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.ofStage_embed — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.ofStage_step — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.preRootFunctional_stage — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.preTrace_stageHom — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.IsRootCornerUnitary — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.compressionError — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.cornerExponential — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.cornerLift — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.isStarProjection_rootFlag — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.limitCStarAlgebra — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.limitMatrixUnit_mul — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.norm_ofStage — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.preRootFunctional_star_mul_self_nonneg — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.protectedPrefix — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.reconstructedStageVector — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.rootCornerSubspace — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.rootFlag_zero — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.rootShell — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.rootState_coe — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.rowAverageLinear — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.stageTests — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.star_limitMatrixUnit — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.sum_limitMatrixUnit_diag — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.trace_coe — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.compressionError_sub — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.cornerLift_eq_rowAverageLinear — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.exists_stage_approx — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.isRootCornerUnitary_cornerExponential — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.isStarProjection_limitMatrixUnit_zero_zero — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.limitPartialOrder — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.mem_protectedPrefix — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.mem_stageTests — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.mem_symm_protectedPrefix — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.norm_compressionError_le — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.norm_trace_le — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.ofStage_injective — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.representation_cornerLift_apply — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.representation_matrixUnit_reconstructedStageVector — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.restrictState — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.rootState_stage — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.rootState_star_mul_self_nonneg — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.rowAverageLinear_apply — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.rowAverageLinear_one — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.row_isometry_sum — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.star_cornerLift — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.trace_mul_comm — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.trace_ofStage — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.trace_star_mul_self_nonneg — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.cornerLift_mem_unitary — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.eq_rootState_of_restrict — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.exists_common_stage_approx — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.exists_rootCornerSupported_selfAdjoint_norm_le_two_mul_and_eq_on — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.limitMatrixUnit_commute_rowAverage — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.limitStarOrderedRing — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.restrictState_apply — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.rootState_one — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.rootState_rootFlag — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.trace_one — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.trace_rootFlag — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.RepresentativeShellData — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.apply_limitMatrixUnit_eq_trace_of_apply_one_of_mul_comm — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.exists_rootCornerSupported_exponential_eq_on — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.liftedCornerExponential — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.ofStage_eq_sum_smul_limitMatrixUnit — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.restrictState_mem_stateSpace — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.rootFlag_mul_ofStage_mul — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.rootFlag_succ_le — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.rootState_nonneg — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.rowAverageLinear_nonneg — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.sum_norm_sq_map_limitMatrixUnit_star — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.trace_nonneg — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.vectorFunctional_reconstructedStageVector_matrixUnit — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.antitone_rootFlag — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.apply_ofStage_eq_trace_of_apply_one_of_mul_comm — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.compressionError_ofStage — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.continuousLinearMap_eq_on_ofStage_of_eq_matrixUnit — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.isStarProjection_rootShell — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.representation_liftedCornerExponential_apply_of_root — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.representativeShellData — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.rootPositiveState — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.rootState_mem_stateSpace — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.rowAveragePositive — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.tracePositive — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.TraceHilbertSpace — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.norm_leftMulMapPreGNS_apply_le — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.norm_rowAverageLinear_le — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.ofStage_commute_cornerLift — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.reconstructedStageVector_vectorFunctional_eq_on_stage — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.representativeLink_final — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.rootFlag_mul_of_le — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.rootPositiveState_one — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.rootShell_mul_star_rootShell — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.star_rootShell_mul_rootShell — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.tendsto_rootFlag_orbit_zero — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.tracePositive_one — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.transportedFlag — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.SeparableCounterexampleHilbertSpace — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.completedRootPureState — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.isStarProjection_transportedFlag — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.liftedCornerExponential_commute_stage — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.norm_reconstructedStageVector_eq_one — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.norm_rootRepresentation_le — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.representativeLink_initial — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.rootGNSNontrivial — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.rowAverage — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.tendsto_norm_transported_compressionError — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.traceRepresentation — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.traceVector — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.transportedFlag_mul_of_le — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.transportedFlag_zero — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.denseRange_traceRepresentation_orbit — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.exists_selectedCyclicUnitary — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.inner_traceVector_traceRepresentation — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.liftedCornerExponentialPath — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.norm_traceVector — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.representativeShellData_root_alpha — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.representativeShellData_root_link — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.rootRepresentationCLM — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.rootRepresentation_stage_injective — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.rootShell_identity_family — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.selectedVector_fixed_transportedFlag — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.tendsto_transported_compressionError — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.trace_transportedFlag_eq_trace_rootFlag — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.AtomicTarget — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.isOrtho_cyclicSubspace_of_selectedStates — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.liftedCornerExponentialPairPath — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.liftedCornerExponentialPath_commute_stage — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.norm_rootRepresentation_stage — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.representedInitialFlag — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.representedRootFlag — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.representedShellLink — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.separableSpace_traceHilbertSpace — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.tendsto_representative_transported_compression — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.traceVector_ne_zero — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.transportedFlag_root — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.initialFixedProjection_eq_zero_on_otherCyclic — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.initialFixedProjection_maps_ownCyclic — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.instHasOrthogonalProjectionRepresentedInitialFlag — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.instHasOrthogonalProjectionRepresentedRootFlag — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.liftedCornerExponentialPairPath_commute_stage — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.nontrivial_traceHilbertSpace — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.norm_rootRepresentation — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.representedFinalFlag — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.representedGeneratorUnitary — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.restrictedRepresentation — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.separableSpace_separableCounterexampleHilbertSpace — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.instHasOrthogonalProjectionRepresentedFinalFlag — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.representedGenerator_comp_sourceShell — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.rootRepresentation_injective — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.selectedAtomicRepresentation_rootFlag_eq_starProjection — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.selectedAtomicRepresentation_transportedFlag_eq_starProjection — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.exists_rootState_mul_ne_zero — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.instHasOrthogonalProjectionIInfRepresentedFinalFlag — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.instHasOrthogonalProjectionIInfRepresentedInitialFlag — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.exists_rootFlag_mem_of_ne_zero_mem — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.exists_targetDefectVectors_of_fixedSpace_ne_bot — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.isIrreducible_restrictedRepresentation_of_all_fixed_bot — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.limitIsSimpleRing — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.exists_targetDefectVectors — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.representation_injective — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.selectedRootRepresentation_injective — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.selectedAtomicRepresentation_injective — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.not_finiteDimensional_range_rootCorner — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.exists_rootCornerSupported_exponential_apply_eq_involution — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.shellFamilyLinks — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.ShellFamilyTarget — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.shellFamilyLinks_map_selectedVector — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.shellFamilyLinks_root — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.shellFamilyLinks_sourceShell — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.shellFamilyLinks_unitary — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.exists_delta_liftedCornerUnitary_path_apply_sub_norm_lt — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.isClosed_shellFamilyTarget — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.shellFamilyGenerator — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.shellFamilyTargetPartialOrder — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.exists_delta_stageCentral_unitary_path_apply_sub_norm_lt — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.exists_shell_sums_eq_on_cyclicSubspace — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.isIrreducible_shellFamilyInclusion — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.shellFamilyInclusion_injective — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.shellFamilySourceHom_injective — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.shellFamilySourceHom_map_one — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.shellFamilyTargetStarOrderedRing — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.apply_shellFamilySourceHom_eq_trace_of_apply_one_of_mul_comm — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.exists_delta_exact_unitary_path_apply_eq_and_stage_commutator — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.isUniqueIrreducibleModel_shellFamilyInclusion — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.not_finiteDimensional_shellFamilyTarget — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.reduces_cyclicSubspace_of_trace — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.shellFamilyTargetNontrivial — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.cyclicSubspace_eq_top_of_trace_of_cyclic — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.isUniqueIrreducibleModelAmongNonUnital_shellFamilyInclusion — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.nontrivial_shellFamilyTarget — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.traceExtension — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.denseRange_source_orbit_of_trace_of_cyclic — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.shellFamilyTarget_closedIdeal_dichotomy — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.shellFamilyTarget_not_compactOperatorModel — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.stronglyConverges_shell_sums_of_trace_of_cyclic — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.traceExtension_mem_stateSpace — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.traceExtension_shellFamilySourceHom — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.nonempty_initialState — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.nonempty_transition — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.shellFamily_captures_nonunital — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.traceExtensionPositive — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.TracialHilbertSpace — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.chosenTransition — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.initialState — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.traceExtensionPositive_one — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.alternatingStates — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.tracialVector — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.alternatingTransitions — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.denseRange_tracialRepresentation_orbit — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.inner_tracialVector_tracialRepresentation — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.leftAutomorphisms — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.norm_tracialVector — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.outputUnitary — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.rightAutomorphisms — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.leftAutomorphisms_step — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.leftAutomorphisms_symm_step — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.outputAutomorphisms — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.rightAutomorphisms_step — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.rightAutomorphisms_symm_step — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.tracialVector_ne_zero — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.vectorFunctional_tracialRepresentation — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.vectorFunctional_tracialRepresentation_source — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.denseRange_tracialRepresentation_source_orbit — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.eq_traceExtension_of_mem_stateSpace_of_apply_shellFamilySourceHom_eq_trace — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.leftAutomorphisms_cauchy — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.leftAutomorphisms_symm_cauchy — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.nontrivial_tracialHilbertSpace — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.outputAutomorphisms_eq — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.rightAutomorphisms_cauchy — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.rightAutomorphisms_symm_cauchy — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.eq_traceExtension_of_mem_stateSpace_of_mul_comm — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.exists_linearIsometryEquiv_traceHilbertSpace — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.leftAutomorphisms_succ_cauchy — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.leftAutomorphisms_succ_symm_cauchy — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.outputAutomorphisms_state_dense — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.traceExtension_star_unitary_mul_mul — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.outputAutomorphisms_cauchy — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.outputAutomorphisms_symm_cauchy — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.tendsto_outputAutomorphisms_state — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.traceExtension_shellFamilySourceHom_mul — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.traceGNSUnitary — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.hasInnerIntertwiningSequence_vectorFunctional — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.traceExtension_shellFamilyGenerator_mul — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.representativeShellDataOfHomogeneity — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.representativeShellDataOfHomogeneity_root_alpha — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.representativeShellDataOfHomogeneity_root_link — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.AtomicCounterexampleEndpoint — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.continuum_le_cardinalMk_dense_atomicCounterexampleAlgebra — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.cardinalMk_atomicCounterexampleAlgebra_le_continuum — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.cardinalMk_atomicCounterexampleAlgebra — earlier Project view
- MathlibAnnex.CStarAlgebra.CAR.continuum_eq_aleph_one_iff_existsNaimarkCounterexampleOfDensity — earlier Project view