MathlibAnnex/Analysis/CStarAlgebra/Spectrum/Basic.lean

Exact source · gss-v0.5.0

Fixed commit original · Raw UTF-8 source · Back to GSS Companion

Select a source link from a manuscript to highlight its exact range.

1/-2Copyright (c) 2026 Ryotaro Tanaka. All rights reserved.3Released under Apache 2.0 license as described in the file LICENSE.4Authors: Ryotaro Tanaka5-/6import MathlibAnnex.Analysis.CStarAlgebra.FacialStructure.NonUnitalStateGNS7import MathlibAnnex.Analysis.CStarAlgebra.GeometricStructure.RepresentationEquivalence89/-!10# A small space of irreducible representation classes1112The representatives are actual pure continuous positive functionals on A.13The equivalence relation uses their actual canonical-extension GNS actions,14restricted to A, and an actual surjective linear isometry intertwining them.15It is NOT equality of kernels. No topology is inherited from the pure-state16space here: the spectrum topology is defined later through the kernel map.17The construction is meaningful even when the pure-state type is empty.18-/1920set_option autoImplicit false21noncomputable section2223namespace MathlibAnnex.Analysis.CStarAlgebra2425universe u26variable (A : Type u) [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A]2728/-- Actual pure norm-one positive functionals, in the universe of A. -/29abbrev NonUnitalPureState := {phi : StrongDual ℂ A // IsPureNonUnitalState A phi}3031namespace NonUnitalPureState32variable {A}3334/-- The genuine Hilbert-space GNS construction of the canonical state extension. -/35abbrev GNS (phi : NonUnitalPureState A) := NonUnitalStateGNS.Space phi.val phi.property.13637/-- Its representation of the ORIGINAL algebra, not just its formal unitization. -/38def gnsRepresentation (phi : NonUnitalPureState A) : NonUnitalCStarRepresentation A phi.GNS :=39  NonUnitalStateGNS.representation phi.val phi.property.14041theorem isIrreducible_gnsRepresentation (phi : NonUnitalPureState A) :42    phi.gnsRepresentation.IsIrreducible :=43  NonUnitalStateGNS.isIrreducible_representation phi.val phi.property.1 phi.property4445/-- The distinguished vector belongs to the actual extension GNS Hilbert space. -/46abbrev gnsVector (phi : NonUnitalPureState A) : phi.GNS :=47  NonUnitalStateGNS.vector phi.val phi.property.14849theorem norm_gnsVector (phi : NonUnitalPureState A) : ‖phi.gnsVector‖ = 1 :=50  NonUnitalStateGNS.norm_vector phi.val phi.property.15152theorem gnsVector_ne_zero (phi : NonUnitalPureState A) : phi.gnsVector ≠ 0 :=53  norm_ne_zero_iff.mp (by rw [phi.norm_gnsVector]; exact one_ne_zero)5455/-- Canonical pointed coefficient recovery in the original algebra. -/56theorem matrixCoefficient_gnsRepresentation (phi : NonUnitalPureState A) :57    NonUnitalCStarRepresentation.matrixCoefficient phi.gnsRepresentation58      (NonUnitalStateGNS.vector phi.val phi.property.1)59      (NonUnitalStateGNS.vector phi.val phi.property.1) = phi.val :=60  NonUnitalStateGNS.matrixCoefficient_representation phi.val phi.property.16162end NonUnitalPureState6364/-- Equivalence of actual GNS representations, with no kernel identification. -/65def pureStateGNSSetoid : Setoid (NonUnitalPureState A) where66  r phi psi := phi.gnsRepresentation.UnitaryEquivalent psi.gnsRepresentation67  iseqv :=68    ⟨fun phi => NonUnitalCStarRepresentation.unitaryEquivalent_refl phi.gnsRepresentation,69      fun h => h.symm, fun h k => h.trans k⟩7071/-- The small irreducible spectrum: pure states modulo GNS unitary equivalence.72Its topology is specified in `Spectrum.Topology`, not by a state-space quotient. -/73def IrreducibleSpectrum := Quotient (pureStateGNSSetoid A)7475namespace IrreducibleSpectrum76variable {A}7778/-- Send an actual pure state to its representation class. -/79def ofPureState (phi : NonUnitalPureState A) : IrreducibleSpectrum A :=80  Quotient.mk (pureStateGNSSetoid A) phi8182theorem ofPureState_eq_iff (phi psi : NonUnitalPureState A) :83    ofPureState phi = ofPureState psi ↔84      phi.gnsRepresentation.UnitaryEquivalent psi.gnsRepresentation :=85  Quotient.eq8687theorem ofPureState_surjective : Function.Surjective (ofPureState (A := A)) := by88  intro q89  refine Quotient.inductionOn q ?_90  intro phi91  exact ⟨phi, rfl⟩9293end IrreducibleSpectrum94end MathlibAnnex.Analysis.CStarAlgebra