MathlibAnnex.Analysis.CStarAlgebra.IrreducibleSpectrum
def
Defines the irreducible spectrum using unitary equivalence classes of pure-state GNS representations.
Statement
Let be a complex C*-algebra with compatible order, not necessarily unital or nonzero. The irreducible spectrum here is the quotient of its pure states by unitary equivalence of their GNS representations of .
Definition
A pure state is a positive norm-one bounded complex-linear functional , extreme among such functionals for real convexity. Let denote the GNS representation of its canonical extension to the forced unitization, restricted to the original algebra . The pure-state GNS irreducibility theorem guarantees irreducibility of this action.
Write when and are unitarily equivalent: there is a surjective complex-linear isometry between their Hilbert spaces such that for every . The definition is
The quotient uses this unitary-equivalence relation. Equality of representation kernels is not substituted for unitary equivalence. The definition assigns no topology; the later ordinary spectrum topology is induced through the representation-kernel map, not specified here as a pure-state quotient topology.
Assumptions
Only the complex C*-algebra and its compatible order are required. The set of pure states may be empty. No auxiliary Hilbert space or separability assumption is required.
Conclusion
The result is the set of unitary equivalence classes of pure-state GNS representations. The definition permits an empty quotient when there are no pure-state representatives.
Main citations
Lean source signature (exact)
The following is the complete defining right-hand side, copied from the fixed source.
def IrreducibleSpectrum := Quotient (pureStateGNSSetoid A)
| In the source | Mathematical meaning |
|---|---|
Exact declarationNonUnitalPureState A inside the setoid |
The pure states of defined above: positive norm-one bounded complex-linear functionals that are extreme among such functionals. |
Exact declarationpureStateGNSSetoid A |
The relation of unitary equivalence between and . |
Exact declarationQuotient (pureStateGNSSetoid A) |
The quotient for precisely that relation. No kernel equivalence or topology is included in this one-line RHS. |
Exact surrounding source context (separate excerpts)
Source lines 23–26:
namespace MathlibAnnex.Analysis.CStarAlgebra
universe u
variable (A : Type u) [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A]
Read exact source with highlighted declaration · Raw UTF-8 source · LFH Companion ·