Back to Project mathematical routes
A pure state detects a hypothetical nonzero kernel element and its GNS representation is irreducible. Unitary equivalence to the singleton representative then contradicts that kernel element, giving faithfulness and the related simplicity consequence.
5 direct Cards + 5 reused prerequisites = 10 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: R08 — Pure states as real extreme points · R20 — The GNS representation of a pure state is irreducible · R07 — A pure state detects a nonzero square · R12 — Faithfulness from a unique irreducible class · R03 — A faithful singleton model forces simplicity
Reused prerequisites: R05 — A representative of the unique irreducible class · R24 — Nonzero irreducibility without a unit assumption · R25 — Unitary equivalence of two representations · R30 — A character extends to a pure state · R32 — Representations without a unit-preservation requirement
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.
Defines purity inside the normalized positive state space.
MathlibAnnex.Analysis.CStarAlgebra.IsPureState
Immediate Card prerequisites: None in this selected scope
Used by in this scope: The GNS representation of a pure state is irreducible · A character extends to a pure state
Names -representations of a complex -algebra on a Hilbert space when no unit equation is required.
MathlibAnnex.Analysis.CStarAlgebra.NonUnitalCStarRepresentation
Immediate Card prerequisites: None in this selected scope
Used by in this scope: Nonzero irreducibility without a unit assumption · Unitary equivalence of two representations
Applies the cyclic pure-state criterion to the space and vector constructed from the same state.
MathlibAnnex.Analysis.CStarAlgebra.isIrreducible_pureState_gnsStarAlgHom
Immediate Card prerequisites: Pure states as real extreme points
Used by in this scope: A faithful singleton model forces simplicity · Faithfulness from a unique irreducible class
Chooses an extreme state in the compact face of all extensions of one prescribed character.
MathlibAnnex.Analysis.CStarAlgebra.exists_pureState_extension
Immediate Card prerequisites: Pure states as real extreme points
Used by in this scope: A pure state detects a nonzero square
Defines equivalence by one surjective isometry intertwining all algebra actions.
MathlibAnnex.Analysis.CStarAlgebra.NonUnitalCStarRepresentation.UnitaryEquivalent
Immediate Card prerequisites: Representations without a unit-preservation requirement
Used by in this scope: A representative of the unique irreducible class
Requires nonzero action as well as the absence of proper closed reducing subspaces.
MathlibAnnex.Analysis.CStarAlgebra.NonUnitalCStarRepresentation.IsIrreducible
Immediate Card prerequisites: Representations without a unit-preservation requirement
Used by in this scope: A representative of the unique irreducible class
Detects a nonzero element through its positive square without an algebra separability assumption.
MathlibAnnex.Analysis.CStarAlgebra.exists_pureState_nonzero_on_star_mul_self
Immediate Card prerequisites: A character extends to a pure state
Used by in this scope: Faithfulness from a unique irreducible class
Uses irreducible representations annihilating proper ideals to rule out nonzero proper closed ideals.
MathlibAnnex.Analysis.CStarAlgebra.Representation.isSimpleCStarAlgebra_of_singleton_of_injective
Immediate Card prerequisites: The GNS representation of a pure state is irreducible
Used by in this scope: None in this selected scope
Defines when one nonzero irreducible -representation represents the sole unitary-equivalence class of such representations.
MathlibAnnex.Analysis.CStarAlgebra.NonUnitalCStarRepresentation.IsSingletonIrreducibleModel
Immediate Card prerequisites: Nonzero irreducibility without a unit assumption · Unitary equivalence of two representations
Used by in this scope: Faithfulness from a unique irreducible class
Uses a pure state on the unitization to detect any hypothetical nonzero element of the kernel.
MathlibAnnex.Analysis.CStarAlgebra.NonUnitalCStarRepresentation.injective_of_singleton
Immediate Card prerequisites: A representative of the unique irreducible class · A pure state detects a nonzero square · The GNS representation of a pure state is irreducible
Used by in this scope: None in this selected scope