Exact source: MathlibAnnex/Analysis/CStarAlgebra/Representation/PureStateRepresentatives.lean, lines 83–83.
Back to The selected GNS representation of a pure-state class
1import Mathlib.Data.Quot 2import MathlibAnnex.Analysis.CStarAlgebra.GNSCyclic 3import MathlibAnnex.Analysis.CStarAlgebra.Representation 4import MathlibAnnex.Analysis.CStarAlgebra.PureStateHomogeneity.KishimotoOzawaSakai 5 6/-! 7# Set-indexed representatives of pure-state GNS classes 8 9Pure states live in one ordinary continuous-dual type. Quotienting that type 10by unitary equivalence of its GNS representations therefore produces a genuine 11set-sized index type. A supplied root state is retained literally as the 12representative of its class. 13 14This file deliberately stops short of claiming coverage of arbitrary 15irreducible representations: that additional statement requires the full 16pure-state/GNS irreducibility bridge. 17-/ 18 19set_option autoImplicit false 20 21open Set 22open scoped ComplexOrder 23 24namespace MathlibAnnex.CStarAlgebra 25 26universe u 27 28variable (A : Type u) [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] 29 30/-- A pure state, bundled inside the continuous dual. -/ 31abbrev PureState := {phi : A →L[ℂ] ℂ // IsPureState A phi} 32 33namespace PureState 34 35variable {A} 36 37theorem mem_stateSpace (phi : PureState A) : phi.1 ∈ stateSpace A := by 38 exact extremePoints_subset phi.2 39 40/-- 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.1 43 44@[simp] 45theorem positiveFunctional_apply (phi : PureState A) (a : A) : 46 phi.positiveFunctional a = phi.1 a := rfl 47 48@[simp] 49theorem positiveFunctional_one (phi : PureState A) : 50 phi.positiveFunctional 1 = 1 := 51 phi.mem_stateSpace.2 52 53/-- Equivalence of the GNS representations associated to two pure states. -/ 54def GNSEquivalent (phi psi : PureState A) : Prop := 55 StarAlgHom.UnitaryEquivalent phi.positiveFunctional.gnsStarAlgHom 56 psi.positiveFunctional.gnsStarAlgHom 57 58theorem GNSEquivalent.refl (phi : PureState A) : phi.GNSEquivalent phi := 59 StarAlgHom.unitaryEquivalent_refl _ 60 61theorem GNSEquivalent.symm {phi psi : PureState A} (h : phi.GNSEquivalent psi) : 62 psi.GNSEquivalent phi := 63 StarAlgHom.UnitaryEquivalent.symm h 64 65theorem 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₂ 69 70/-- The equivalence relation used for selecting GNS classes. -/ 71def gnsSetoid : Setoid (PureState A) where 72 r := GNSEquivalent 73 iseqv := ⟨GNSEquivalent.refl, GNSEquivalent.symm, GNSEquivalent.trans⟩ 74 75/-- 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)) 78 79def classOf (phi : PureState A) : GNSClass A := 80 Quotient.mk (gnsSetoid (A := A)) phi 81 82/-- 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 by 85 classical 86 exact if j = root.classOf then root else Quotient.out j 87 88@[simp] 89theorem classOf_representative (root : PureState A) (j : GNSClass A) : 90 (representative root j).classOf = j := by 91 classical 92 by_cases h : j = root.classOf 93 · simp [representative, h] 94 · change Quotient.mk (gnsSetoid (A := A)) 95 (if j = root.classOf then root else Quotient.out j) = j 96 rw [if_neg h] 97 exact Quotient.out_eq j 98 99@[simp] 100theorem representative_root (root : PureState A) : 101 representative root root.classOf = root := by 102 classical 103 simp [representative] 104 105/-- 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 := by 108 rw [← classOf_representative root i, ← classOf_representative root j] 109 exact Quotient.sound h 110 111/-- 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 := by 114 exact @Quotient.exact _ (gnsSetoid (A := A)) (representative root phi.classOf) phi 115 (classOf_representative root phi.classOf) 116 117/-- 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 := by 120 exact (representative root j).positiveFunctional.norm_gnsCyclicVector 121 (representative root j).positiveFunctional_one 122 123/-- 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 a 127 (representative root j).positiveFunctional.gnsCyclicVector) := by 128 exact (representative root j).positiveFunctional 129 |>.denseRange_gnsStarAlgHom_apply_gnsCyclicVector 130 131end PureState 132 133end MathlibAnnex.CStarAlgebra