Exact source: MathlibAnnex/Analysis/CStarAlgebra/PureStateGNS/IrreduciblePure.lean, lines 212–232.
Back to An irreducible target representation has a surviving fixed space
1import Mathlib.Analysis.Normed.Operator.Extend 2import MathlibAnnex.Analysis.CStarAlgebra.Intertwiner 3import MathlibAnnex.Analysis.CStarAlgebra.PureStateGNS.PureIrreducible 4import MathlibAnnex.Analysis.CStarAlgebra.Representation.PureStateRepresentatives 5 6/-! 7# Irreducible representations and pure vector states 8 9The reverse pure-state/GNS implication is proved by extending the dominated 10GNS orbit map to a contraction. Its positive initial operator lies in the 11commutant, so the arbitrary-dimensional Schur theorem makes it scalar. 12-/ 13 14set_option autoImplicit false 15 16open Set 17open scoped ComplexOrder Convex InnerProduct 18 19namespace MathlibAnnex.CStarAlgebra 20 21universe u v 22 23variable {A : Type u} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] 24variable {H : Type v} 25variable [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] 26 27open MathlibAnnex.Analysis.CStarAlgebra 28 29/-- A positive functional dominated by an irreducible unit vector state is a 30real scalar multiple of that state. The dominated functional may be zero; 31no normalization or nonzero hypothesis is used. -/ 32theorem eq_smul_of_irreducible_vectorFunctional_of_nonnegative_le 33 (pi : Representation A H) (hirr : pi.IsIrreducible) 34 (xi : H) (hxi : ‖xi‖ = 1) 35 (rho : A →L[ℂ] ℂ) (hrho : ∀ a : A, 0 ≤ a → 0 ≤ rho a) 36 (hle : ∀ a : A, 0 ≤ a → rho a ≤ Representation.vectorFunctional pi xi a) : 37 ∃ t : ℝ, 0 ≤ t ∧ t ≤ 1 ∧ 38 rho = t • Representation.vectorFunctional pi xi := by 39 letI : Nontrivial H := Representation.nontrivial_of_isNonzero pi hirr.1 40 have hxi_ne : xi ≠ 0 := by 41 intro hzero 42 simpa [hzero] using hxi 43 have hdense : DenseRange (StarAlgHom.orbitMap pi xi) := 44 Representation.denseRange_orbitMap_of_isIrreducible pi hirr hxi_ne 45 let f : A →ₚ[ℂ] ℂ := PositiveLinearMap.mk₀ rho.toLinearMap hrho 46 let sigma : Representation A f.GNS := f.gnsStarAlgHom 47 let eta : f.GNS := f.gnsCyclicVector 48 let p : A →ₗ[ℂ] H := StarAlgHom.orbitMap pi xi 49 let q : A →ₗ[ℂ] f.GNS := StarAlgHom.orbitMap sigma eta 50 have hq_inner (a : A) : inner ℂ (q a) (q a) = rho (star a * a) := by 51 calc 52 inner ℂ (q a) (q a) = 53 Representation.vectorFunctional sigma eta (star a * a) := by 54 simpa [p, q, StarAlgHom.orbitMap] using 55 (Representation.vectorFunctional_star_mul sigma eta a a).symm 56 _ = f (star a * a) := by 57 exact PositiveLinearMap.inner_gnsCyclicVector_gnsStarAlgHom f (star a * a) 58 _ = rho (star a * a) := rfl 59 have hp_inner (a : A) : inner ℂ (p a) (p a) = 60 Representation.vectorFunctional pi xi (star a * a) := by 61 simpa [p, StarAlgHom.orbitMap] using 62 (Representation.vectorFunctional_star_mul pi xi a a).symm 63 have hnorm (a : A) : ‖q a‖ ≤ (1 : ℝ) * ‖p a‖ := by 64 rw [one_mul] 65 apply (sq_le_sq₀ (norm_nonneg _) (norm_nonneg _)).mp 66 rw [norm_sq_eq_re_inner (𝕜 := ℂ) (q a), 67 norm_sq_eq_re_inner (𝕜 := ℂ) (p a), hq_inner, hp_inner] 68 have hdiff := RCLike.nonneg_iff.mp 69 (sub_nonneg.mpr (hle (star a * a) (star_mul_self_nonneg a))) 70 simpa using hdiff.1 71 let T : H →L[ℂ] f.GNS := q.extendOfNorm p 72 have hT_orbit (a : A) : T (pi a xi) = sigma a eta := by 73 simpa [T, p, q, StarAlgHom.orbitMap] using 74 (LinearMap.extendOfNorm_eq hdense ⟨(1 : ℝ), hnorm⟩ a) 75 have hT_intertwines : StarAlgHom.Intertwines pi sigma T := by 76 intro b 77 apply ContinuousLinearMap.ext 78 intro x 79 exact hdense.induction_on x 80 (isClosed_eq ((T.comp (pi b)).continuous) (((sigma b).comp T).continuous)) 81 fun a ↦ by 82 change T (pi b (pi a xi)) = sigma b (T (pi a xi)) 83 have hpi_mul : pi (b * a) xi = pi b (pi a xi) := by 84 rw [map_mul] 85 rfl 86 have hsigma_mul : sigma (b * a) eta = sigma b (sigma a eta) := by 87 rw [map_mul] 88 rfl 89 calc 90 T (pi b (pi a xi)) = T (pi (b * a) xi) := congrArg T hpi_mul.symm 91 _ = sigma (b * a) eta := hT_orbit (b * a) 92 _ = sigma b (sigma a eta) := hsigma_mul 93 _ = sigma b (T (pi a xi)) := by rw [hT_orbit a] 94 let D : H →L[ℂ] H := (T†).comp T 95 have hD_self : IsSelfAdjoint D := by 96 rw [isSelfAdjoint_iff, ContinuousLinearMap.star_eq_adjoint, 97 ContinuousLinearMap.adjoint_comp, ContinuousLinearMap.adjoint_adjoint] 98 have hD_comm : StarAlgHom.InCommutant pi D := by 99 exact hT_intertwines.inCommutant_adjoint_comp_self 100 obtain ⟨t, hD⟩ := StarAlgHom.eq_algebraMap_of_isSelfAdjoint_of_irreducible 101 pi (Representation.isIrreducible_starAlgHom pi hirr) D hD_self hD_comm 102 have hTxi : T xi = eta := by 103 simpa using hT_orbit (1 : A) 104 have heta_sq : ‖eta‖ ^ 2 = (rho 1).re := by 105 rw [norm_sq_eq_re_inner (𝕜 := ℂ) eta] 106 have hcoeff : inner ℂ eta eta = rho 1 := by 107 calc 108 inner ℂ eta eta = inner ℂ eta (sigma 1 eta) := by simp 109 _ = f 1 := PositiveLinearMap.inner_gnsCyclicVector_gnsStarAlgHom f 1 110 _ = rho 1 := rfl 111 rw [hcoeff] 112 rw [RCLike.re_eq_complex_re] 113 have ht_eq : t = (rho 1).re := by 114 have hnormD := ContinuousLinearMap.apply_norm_sq_eq_inner_adjoint_right T xi 115 rw [hTxi, heta_sq] at hnormD 116 rw [show (T†).comp T = D by rfl, hD] at hnormD 117 rw [ContinuousLinearMap.algebraMap_apply, 118 RCLike.real_smul_eq_coe_smul (K := ℂ), inner_smul_real_right, 119 RCLike.smul_re, ← norm_sq_eq_re_inner (𝕜 := ℂ), hxi] at hnormD 120 simpa using hnormD.symm 121 have ht_nonneg : 0 ≤ t := by 122 rw [ht_eq] 123 exact (RCLike.nonneg_iff.mp 124 (hrho 1 (by simpa using star_mul_self_nonneg (1 : A)))).1 125 have ht_le_one : t ≤ 1 := by 126 rw [ht_eq] 127 have hdiff := RCLike.nonneg_iff.mp 128 (sub_nonneg.mpr (hle 1 (by simpa using star_mul_self_nonneg (1 : A)))) 129 simpa [Representation.vectorFunctional_one pi hxi] using hdiff.1 130 refine ⟨t, ht_nonneg, ht_le_one, ?_⟩ 131 apply ContinuousLinearMap.ext 132 intro a 133 calc 134 rho a = inner ℂ eta (sigma a eta) := by 135 exact (PositiveLinearMap.inner_gnsCyclicVector_gnsStarAlgHom f a).symm 136 _ = inner ℂ (T xi) (sigma a (T xi)) := by rw [hTxi] 137 _ = inner ℂ (T xi) (T (pi a xi)) := by 138 have h := congrArg (fun R : H →L[ℂ] f.GNS ↦ R xi) (hT_intertwines a) 139 simpa [ContinuousLinearMap.comp_apply] using congrArg (inner ℂ (T xi)) h.symm 140 _ = inner ℂ xi (D (pi a xi)) := by 141 simpa [D, ContinuousLinearMap.comp_apply] using 142 (ContinuousLinearMap.adjoint_inner_right T xi (T (pi a xi))).symm 143 _ = inner ℂ xi ((algebraMap ℝ (H →L[ℂ] H) t) (pi a xi)) := by rw [hD] 144 _ = (t • Representation.vectorFunctional pi xi) a := by 145 rw [ContinuousLinearMap.algebraMap_apply, 146 RCLike.real_smul_eq_coe_smul (K := ℂ), inner_smul_right] 147 simp [Representation.vectorFunctional_apply, Complex.real_smul] 148 149/-- Every unit vector state of an explicitly nonzero irreducible unital 150representation is pure. -/ 151theorem isPureState_vectorFunctional_of_isIrreducible 152 (pi : Representation A H) (hirr : pi.IsIrreducible) 153 (xi : H) (hxi : ‖xi‖ = 1) : 154 IsPureState A (Representation.vectorFunctional pi xi) := by 155 rw [IsPureState, mem_extremePoints_iff_left] 156 refine ⟨vectorFunctional_mem_stateSpace pi xi hxi, ?_⟩ 157 intro psi hpsi chi hchi hsegment 158 rcases hsegment with ⟨s, t, hs, ht, hst, hconv⟩ 159 let rho : A →L[ℂ] ℂ := s • psi 160 have hrho : ∀ a : A, 0 ≤ a → 0 ≤ rho a := by 161 intro a ha 162 exact smul_nonneg hs.le (hpsi.1 a ha) 163 have hle : ∀ a : A, 0 ≤ a → 164 rho a ≤ Representation.vectorFunctional pi xi a := by 165 intro a ha 166 rw [← hconv] 167 simp only [ContinuousLinearMap.add_apply, ContinuousLinearMap.smul_apply] 168 exact le_add_of_nonneg_right (smul_nonneg ht.le (hchi.1 a ha)) 169 obtain ⟨r, -, -, hrho_eq⟩ := 170 eq_smul_of_irreducible_vectorFunctional_of_nonnegative_le 171 pi hirr xi hxi rho hrho hle 172 have hrs : r = s := by 173 have h := congrArg (fun f : A →L[ℂ] ℂ ↦ f 1) hrho_eq 174 have hre := congrArg Complex.re h 175 simpa [rho, hpsi.2, Representation.vectorFunctional_one pi hxi, 176 Complex.real_smul] using hre.symm 177 apply smul_right_injective (A →L[ℂ] ℂ) hs.ne' 178 simpa [rho, hrs] using hrho_eq 179 180/-- Ordinary pure states are exactly those whose canonical GNS 181representations are irreducible. -/ 182theorem isPureState_iff_gnsStarAlgHom_isIrreducible 183 (phi : A →L[ℂ] ℂ) (hphi : phi ∈ stateSpace A) : 184 IsPureState A phi ↔ 185 StarAlgHom.IsIrreducible 186 (positiveLinearMapOfMemStateSpace phi hphi).gnsStarAlgHom := by 187 constructor 188 · exact isIrreducible_pureState_gnsStarAlgHom phi hphi 189 · intro hirr 190 let f : A →ₚ[ℂ] ℂ := positiveLinearMapOfMemStateSpace phi hphi 191 let xi : f.GNS := f.gnsCyclicVector 192 have hxi : ‖xi‖ = 1 := by 193 exact PositiveLinearMap.norm_gnsCyclicVector f 194 (positiveLinearMapOfMemStateSpace_one phi hphi) 195 have hxi_ne : xi ≠ 0 := by 196 intro hzero 197 simpa [hzero] using hxi 198 letI : Nontrivial f.GNS := nontrivial_of_ne xi 0 hxi_ne 199 have hirr' : Representation.IsIrreducible f.gnsStarAlgHom := 200 (Representation.isIrreducible_iff_starAlgHom f.gnsStarAlgHom).2 hirr 201 have hpure := isPureState_vectorFunctional_of_isIrreducible 202 f.gnsStarAlgHom hirr' xi hxi 203 have hfunctional : Representation.vectorFunctional f.gnsStarAlgHom xi = phi := by 204 apply ContinuousLinearMap.ext 205 intro a 206 exact inner_gnsStarAlgHom_stateGNSVector phi hphi a 207 rw [hfunctional] at hpure 208 exact hpure 209 210/-- The existing chosen pure-GNS transversal covers every nonzero 211irreducible representation on an arbitrary target Hilbert-space universe. -/ 212theorem irreducible_covered_by_pureState_representative 213 (root : PureState A) (pi : Representation A H) (hirr : pi.IsIrreducible) : 214 ∃ j : PureState.GNSClass A, 215 Representation.UnitaryEquivalent pi 216 (PureState.representative root j).positiveFunctional.gnsStarAlgHom := by 217 obtain ⟨xi, hxi, hcyclic, -, hpi⟩ := irreducible_exists_vectorStateGNS pi hirr 218 have hpure : IsPureState A (Representation.vectorFunctional pi xi) := 219 isPureState_vectorFunctional_of_isIrreducible pi hirr xi hxi 220 let phi : PureState A := ⟨Representation.vectorFunctional pi xi, hpure⟩ 221 have hpositive : phi.positiveFunctional = vectorPositiveFunctional pi xi hxi := by 222 ext a 223 rfl 224 have hpi' : Representation.UnitaryEquivalent pi phi.positiveFunctional.gnsStarAlgHom := by 225 rw [hpositive] 226 exact hpi 227 have hrep : Representation.UnitaryEquivalent 228 (PureState.representative root phi.classOf).positiveFunctional.gnsStarAlgHom 229 phi.positiveFunctional.gnsStarAlgHom := 230 PureState.representative_covers root phi 231 exact ⟨phi.classOf, Representation.unitaryEquivalent_trans hpi' 232 (Representation.unitaryEquivalent_symm hrep)⟩ 233 234end MathlibAnnex.CStarAlgebra