Back to Project mathematical routes
Representations without a unit equation, nonzero irreducibility and unitary equivalence set the language of the theorem. The singleton condition names one representative of the unique nonzero irreducible class.
4 direct Cards + 0 reused prerequisites = 4 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: R32 — Representations without a unit-preservation requirement · R24 — Nonzero irreducibility without a unit assumption · R25 — Unitary equivalence of two representations · R05 — A representative of the unique irreducible class
Reused prerequisites: None in this scope.
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.
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
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
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: None in this selected scope