Exact source: MathlibAnnex/Analysis/CStarAlgebra/Representation/PureStateRepresentatives.lean
Pinned GitHub source · Raw UTF-8 source
Back to Distinct GNS classes have no unitary intertwiner
1import Mathlib.Data.Quot2import MathlibAnnex.Analysis.CStarAlgebra.GNSCyclic3import MathlibAnnex.Analysis.CStarAlgebra.Representation4import MathlibAnnex.Analysis.CStarAlgebra.PureStateHomogeneity.KishimotoOzawaSakai56/-!7# Set-indexed representatives of pure-state GNS classes89Pure states live in one ordinary continuous-dual type. Quotienting that type10by unitary equivalence of its GNS representations therefore produces a genuine11set-sized index type. A supplied root state is retained literally as the12representative of its class.1314This file deliberately stops short of claiming coverage of arbitrary15irreducible representations: that additional statement requires the full16pure-state/GNS irreducibility bridge.17-/1819set_option autoImplicit false2021open Set22open scoped ComplexOrder2324namespace MathlibAnnex.CStarAlgebra2526universe u2728variable (A : Type u) [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A]2930/-- A pure state, bundled inside the continuous dual. -/31abbrev PureState := {phi : A →L[ℂ] ℂ // IsPureState A phi}3233namespace PureState3435variable {A}3637theorem mem_stateSpace (phi : PureState A) : phi.1 ∈ stateSpace A := by38 exact extremePoints_subset phi.23940/-- The positive-linear-map view used by Mathlib's GNS construction. -/41noncomputable def positiveFunctional (phi : PureState A) : A →ₚ[ℂ] ℂ :=42 PositiveLinearMap.mk₀ phi.1.toLinearMap phi.mem_stateSpace.14344@[simp]45theorem positiveFunctional_apply (phi : PureState A) (a : A) :46 phi.positiveFunctional a = phi.1 a := rfl4748@[simp]49theorem positiveFunctional_one (phi : PureState A) :50 phi.positiveFunctional 1 = 1 :=51 phi.mem_stateSpace.25253/-- Equivalence of the GNS representations associated to two pure states. -/54def GNSEquivalent (phi psi : PureState A) : Prop :=55 StarAlgHom.UnitaryEquivalent phi.positiveFunctional.gnsStarAlgHom56 psi.positiveFunctional.gnsStarAlgHom5758theorem GNSEquivalent.refl (phi : PureState A) : phi.GNSEquivalent phi :=59 StarAlgHom.unitaryEquivalent_refl _6061theorem GNSEquivalent.symm {phi psi : PureState A} (h : phi.GNSEquivalent psi) :62 psi.GNSEquivalent phi :=63 StarAlgHom.UnitaryEquivalent.symm h6465theorem GNSEquivalent.trans {phi psi chi : PureState A}66 (h₁ : phi.GNSEquivalent psi) (h₂ : psi.GNSEquivalent chi) :67 phi.GNSEquivalent chi :=68 StarAlgHom.UnitaryEquivalent.trans h₁ h₂6970/-- The equivalence relation used for selecting GNS classes. -/71def gnsSetoid : Setoid (PureState A) where72 r := GNSEquivalent73 iseqv := ⟨GNSEquivalent.refl, GNSEquivalent.symm, GNSEquivalent.trans⟩7475/-- The set-sized quotient of pure states by unitary equivalence of GNS representations. -/76abbrev GNSClass (A : Type u) [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] :=77 Quotient (gnsSetoid (A := A))7879def classOf (phi : PureState A) : GNSClass A :=80 Quotient.mk (gnsSetoid (A := A)) phi8182/-- Select one state per GNS class, but retain the requested root state literally. -/83noncomputable def representative (root : PureState A) (j : GNSClass A) : PureState A :=84 by85 classical86 exact if j = root.classOf then root else Quotient.out j8788@[simp]89theorem classOf_representative (root : PureState A) (j : GNSClass A) :90 (representative root j).classOf = j := by91 classical92 by_cases h : j = root.classOf93 · simp [representative, h]94 · change Quotient.mk (gnsSetoid (A := A))95 (if j = root.classOf then root else Quotient.out j) = j96 rw [if_neg h]97 exact Quotient.out_eq j9899@[simp]100theorem representative_root (root : PureState A) :101 representative root root.classOf = root := by102 classical103 simp [representative]104105/-- Distinct selected indices have inequivalent GNS representations. -/106theorem representative_injective_on_classes (root : PureState A) {i j : GNSClass A}107 (h : (representative root i).GNSEquivalent (representative root j)) : i = j := by108 rw [← classOf_representative root i, ← classOf_representative root j]109 exact Quotient.sound h110111/-- Every pure-state GNS class is represented by the selected family. -/112theorem representative_covers (root phi : PureState A) :113 (representative root phi.classOf).GNSEquivalent phi := by114 exact @Quotient.exact _ (gnsSetoid (A := A)) (representative root phi.classOf) phi115 (classOf_representative root phi.classOf)116117/-- Every selected GNS cyclic vector has norm one. -/118theorem norm_representative_gnsCyclicVector (root : PureState A) (j : GNSClass A) :119 ‖(representative root j).positiveFunctional.gnsCyclicVector‖ = 1 := by120 exact (representative root j).positiveFunctional.norm_gnsCyclicVector121 (representative root j).positiveFunctional_one122123/-- Every selected GNS algebra orbit is dense. -/124theorem denseRange_representative_gns_orbit (root : PureState A) (j : GNSClass A) :125 DenseRange (fun a : A ↦126 (representative root j).positiveFunctional.gnsStarAlgHom a127 (representative root j).positiveFunctional.gnsCyclicVector) := by128 exact (representative root j).positiveFunctional129 |>.denseRange_gnsStarAlgHom_apply_gnsCyclicVector130131end PureState132133end MathlibAnnex.CStarAlgebra