MATHLIBANNEX / EXACT SOURCE v0.4.0
MathlibAnnex.Analysis.CStarAlgebra.exists_pureState_extension
theorem exists_pureState_extension (D : StarSubalgebra ℂ A) [IsClosed (D : Set A)]
(chi : WeakDual.characterSpace ℂ D) :
∃ phi : A →L[ℂ] ℂ,
phi ∈ stateSpace A ∧ IsPureState A phi ∧ ∀ d : D, phi d = chi d1 import Mathlib.Analysis.CStarAlgebra.GelfandDuality 2 import Mathlib.Analysis.Normed.Module.HahnBanach 3 import MathlibAnnex.Analysis.CStarAlgebra.PureState 4 import MathlibAnnex.Analysis.CStarAlgebra.State.Basic 5 6 /-! 7 # Pure extension of characters 8 9 Characters of a unital C-star subalgebra are pure states. Hahn--Banach and 10 Krein--Milman then give a pure state of the ambient algebra extending any 11 such character. 12 -/ 13 14 set_option autoImplicit false 15 16 open Metric Set 17 open scoped ComplexOrder Convex 18 19 namespace MathlibAnnex.Analysis.CStarAlgebra 20 21 universe u 22 23 variable {A : Type u} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] 24 25 local instance extensionWeakDualIsScalarTower : IsScalarTower ℝ ℂ (WeakDual ℂ A) := 26 inferInstanceAs (IsScalarTower ℝ ℂ (StrongDual ℂ A)) 27 28 local instance extensionWeakDualLocallyConvexSpace : LocallyConvexSpace ℝ (WeakDual ℂ A) := 29 inferInstanceAs (LocallyConvexSpace ℝ (WeakBilin (topDualPairing ℂ A))) 30 31 /-- A continuous character of a unital C-star algebra is positive. -/ 32 theorem character_nonnegative (chi : WeakDual.characterSpace ℂ A) : 33 ∀ a : A, 0 ≤ a → 0 ≤ chi a := by 34 intro a ha 35 rw [StarOrderedRing.nonneg_iff] at ha ⊢ 36 induction ha using AddSubmonoid.closure_induction with 37 | mem x hx => 38 obtain ⟨b, rfl⟩ := hx 39 refine AddSubmonoid.subset_closure ⟨chi b, ?_⟩ 40 rw [map_mul, map_star] 41 | zero => simp 42 | add x y _ _ hx hy => simpa using AddSubmonoid.add_mem _ hx hy 43 44 /-- A character, regarded as a continuous linear functional, is a state. -/ 45 theorem character_mem_stateSpace (chi : WeakDual.characterSpace ℂ A) : 46 WeakDual.CharacterSpace.toCLM chi ∈ stateSpace A := 47 ⟨character_nonnegative chi, map_one chi⟩ 48 49 /-- Every character of a unital C-star algebra is a pure state. -/ 50 theorem isPureState_character (chi : WeakDual.characterSpace ℂ A) : 51 IsPureState A (WeakDual.CharacterSpace.toCLM chi) := by 52 rw [IsPureState, mem_extremePoints] 53 refine ⟨character_mem_stateSpace chi, ?_⟩ 54 intro psi hpsi theta htheta hseg 55 rcases hseg with ⟨s, t, hs, ht, hst, hconv⟩ 56 have endpoint (rho : A →L[ℂ] ℂ) (hrho : rho ∈ stateSpace A) 57 (other : A →L[ℂ] ℂ) (hother : other ∈ stateSpace A) 58 (r q : ℝ) (hr : 0 < r) (hq : 0 < q) 59 (hconv' : r • rho + q • other = WeakDual.CharacterSpace.toCLM chi) : 60 rho = WeakDual.CharacterSpace.toCLM chi := by 61 apply ContinuousLinearMap.ext 62 intro a 63 let x : A := a - algebraMap ℂ A (chi a) 64 have hchix : chi x = 0 := by 65 have hc : chi (algebraMap ℂ A (chi a)) = chi a := by 66 simpa using AlgHomClass.commutes chi (chi a) 67 calc 68 chi x = chi a - chi (algebraMap ℂ A (chi a)) := by 69 simp only [x, map_sub] 70 _ = chi a - chi a := by rw [hc] 71 _ = 0 := sub_self _ 72 have hchixx : chi (star x * x) = 0 := by 73 rw [map_mul, map_star, hchix] 74 simp 75 have hvalue := congrArg (fun f : A →L[ℂ] ℂ => f (star x * x)) hconv' 76 change r • rho (star x * x) + q • other (star x * x) = 77 chi (star x * x) at hvalue 78 have hzero : 79 r * (rho (star x * x)).re + q * (other (star x * x)).re = 0 := by 80 have := congrArg Complex.re hvalue 81 simpa [hchixx, Complex.real_smul] using this 82 have hrho_nonneg := RCLike.nonneg_iff.mp 83 (hrho.1 (star x * x) (star_mul_self_nonneg x)) 84 have hother_nonneg := RCLike.nonneg_iff.mp 85 (hother.1 (star x * x) (star_mul_self_nonneg x)) 86 have hrho_re : (rho (star x * x)).re = 0 := by 87 have hleft : 0 ≤ r * (rho (star x * x)).re := 88 mul_nonneg hr.le hrho_nonneg.1 89 have hright : 0 ≤ q * (other (star x * x)).re := 90 mul_nonneg hq.le hother_nonneg.1 91 have hmul : r * (rho (star x * x)).re = 0 := by linarith 92 exact (mul_eq_zero.mp hmul).resolve_left hr.ne' 93 have hrho_xx : rho (star x * x) = 0 := by 94 apply Complex.ext 95 · simpa using hrho_re 96 · simpa using hrho_nonneg.2 97 have hrho_x : rho x = 0 := 98 apply_eq_zero_of_star_mul_self_eq_zero rho hrho.1 hrho_xx 99 calc 100 rho a = rho (x + algebraMap ℂ A (chi a)) := by simp [x] 101 _ = rho x + rho (algebraMap ℂ A (chi a)) := map_add rho _ _ 102 _ = chi a := by 103 rw [hrho_x, zero_add, Algebra.algebraMap_eq_smul_one, map_smul, hrho.2] 104 simp 105 _ = WeakDual.CharacterSpace.toCLM chi a := rfl 106 have hpsi_eq : psi = WeakDual.CharacterSpace.toCLM chi := 107 endpoint psi hpsi theta htheta s t hs ht hconv 108 have htheta_eq : theta = WeakDual.CharacterSpace.toCLM chi := 109 endpoint theta htheta psi hpsi t s ht hs (by simpa [add_comm] using hconv) 110 exact ⟨hpsi_eq, htheta_eq⟩ 111 112 section Extension 113 114 variable [Nontrivial A] 115 116 /-- Weak-star states whose restriction to `D` equals `chi`. -/ 117 def weakStateExtensionFace (D : StarSubalgebra ℂ A) 118 (chi : WeakDual.characterSpace ℂ D) : Set (WeakDual ℂ A) := 119 {phi | phi ∈ weakStateSpace A ∧ ∀ d : D, phi d = chi d} 120 121 private theorem character_norm_eq_one (D : StarSubalgebra ℂ A) [IsClosed (D : Set A)] 122 (chi : WeakDual.characterSpace ℂ D) : 123 ‖WeakDual.CharacterSpace.toCLM chi‖ = 1 := by 124 apply le_antisymm 125 · change ‖WeakDual.toStrongDual (chi : WeakDual ℂ D)‖ ≤ 1 126 simpa using WeakDual.CharacterSpace.norm_le_norm_one chi 127 · have h := (WeakDual.CharacterSpace.toCLM chi).le_opNorm (1 : D) 128 simpa using h 129 130 /-- Hahn--Banach extends a character to an ambient state. -/ 131 theorem exists_state_extension (D : StarSubalgebra ℂ A) [IsClosed (D : Set A)] 132 (chi : WeakDual.characterSpace ℂ D) : 133 ∃ phi : A →L[ℂ] ℂ, phi ∈ stateSpace A ∧ ∀ d : D, phi d = chi d := by 134 let p : Submodule ℂ A := D.toSubalgebra.toSubmodule 135 let f : StrongDual ℂ p := WeakDual.CharacterSpace.toCLM chi 136 obtain ⟨phi, hext, hnorm⟩ := exists_extension_norm_eq p f 137 have hfone : f (⟨1, D.one_mem⟩ : p) = 1 := by 138 change chi (1 : D) = 1 139 exact map_one chi 140 have hphi_one : phi 1 = 1 := by 141 calc 142 phi 1 = f (⟨1, D.one_mem⟩ : p) := hext (⟨1, D.one_mem⟩ : p) 143 _ = 1 := hfone 144 have hphi_norm : ‖phi‖ ≤ 1 := by 145 rw [hnorm] 146 exact le_of_eq (character_norm_eq_one D chi) 147 refine ⟨phi, ⟨nonnegative_of_norm_le_one_of_apply_one phi hphi_norm hphi_one, 148 hphi_one⟩, ?_⟩ 149 intro d 150 simpa [p, f] using hext (show p from d) 151 152 theorem isClosed_weakStateExtensionFace (D : StarSubalgebra ℂ A) 153 (chi : WeakDual.characterSpace ℂ D) : 154 IsClosed (weakStateExtensionFace D chi) := by 155 simp only [weakStateExtensionFace, setOf_and, setOf_forall] 156 exact isClosed_weakStateSpace.inter 157 (isClosed_iInter fun d => 158 isClosed_eq (WeakDual.eval_continuous (d : A)) continuous_const) 159 160 theorem weakStateExtensionFace_subset_closedBall (D : StarSubalgebra ℂ A) 161 (chi : WeakDual.characterSpace ℂ D) : 162 weakStateExtensionFace D chi ⊆ 163 WeakDual.toStrongDual ⁻¹' closedBall (0 : StrongDual ℂ A) 1 := by 164 intro phi hphi 165 simpa only [mem_preimage, mem_closedBall_zero_iff] using 166 norm_le_one_of_mem_weakStateSpace hphi.1 167 168 theorem isCompact_weakStateExtensionFace (D : StarSubalgebra ℂ A) 169 (chi : WeakDual.characterSpace ℂ D) : 170 IsCompact (weakStateExtensionFace D chi) := 171 (WeakDual.isCompact_closedBall (𝕜 := ℂ) (E := A) 0 1).of_isClosed_subset 172 (isClosed_weakStateExtensionFace D chi) 173 (weakStateExtensionFace_subset_closedBall D chi) 174 175 theorem weakStateExtensionFace_nonempty (D : StarSubalgebra ℂ A) [IsClosed (D : Set A)] 176 (chi : WeakDual.characterSpace ℂ D) : 177 (weakStateExtensionFace D chi).Nonempty := by 178 obtain ⟨phi, hphi, hext⟩ := exists_state_extension D chi 179 exact ⟨StrongDual.toWeakDual phi, hphi, hext⟩ 180 181 /-- The extension set is a face of the ambient state space. -/ 182 theorem isExtreme_weakStateExtensionFace (D : StarSubalgebra ℂ A) [IsClosed (D : Set A)] 183 (chi : WeakDual.characterSpace ℂ D) : 184 IsExtreme ℝ (weakStateSpace A) (weakStateExtensionFace D chi) := by 185 let spectralOrderD : PartialOrder D := CStarAlgebra.spectralOrder D 186 letI : LE D := spectralOrderD.toLE 187 letI : LT D := spectralOrderD.toLT 188 letI : PartialOrder D := spectralOrderD 189 letI : StarOrderedRing D := CStarAlgebra.spectralOrderedRing D 190 have coe_nonnegative {d : D} (hd : 0 ≤ d) : 0 ≤ (d : A) := by 191 rw [StarOrderedRing.nonneg_iff] at hd 192 induction hd using AddSubmonoid.closure_induction with 193 | mem x hx => 194 obtain ⟨y, rfl⟩ := hx 195 simpa using star_mul_self_nonneg (y : A) 196 | zero => simp 197 | add x y _ _ hx hy => 198 simpa using add_nonneg hx hy 199 refine ⟨fun _ h => h.1, ?_⟩ 200 intro psi hpsi theta htheta phi hphi hseg 201 refine ⟨hpsi, ?_⟩ 202 let p : Submodule ℂ A := D.toSubalgebra.toSubmodule 203 let psiD : D →L[ℂ] ℂ := psi.toStrongDual.comp p.subtypeL 204 let thetaD : D →L[ℂ] ℂ := theta.toStrongDual.comp p.subtypeL 205 have hpsiD : psiD ∈ stateSpace D := by 206 refine ⟨?_, ?_⟩ 207 · intro d hd 208 exact hpsi.1 (d : A) (coe_nonnegative hd) 209 · exact hpsi.2 210 have hthetaD : thetaD ∈ stateSpace D := by 211 refine ⟨?_, ?_⟩ 212 · intro d hd 213 exact htheta.1 (d : A) (coe_nonnegative hd) 214 · exact htheta.2 215 have hchi := isPureState_character chi 216 rw [IsPureState, mem_extremePoints] at hchi 217 have hsegD : WeakDual.CharacterSpace.toCLM chi ∈ 218 openSegment ℝ psiD thetaD := by 219 rcases hseg with ⟨s, t, hs, ht, hst, hconv⟩ 220 refine ⟨s, t, hs, ht, hst, ?_⟩ 221 apply ContinuousLinearMap.ext 222 intro d 223 have hv := congrArg (fun q : WeakDual ℂ A => q (d : A)) hconv 224 change s • psi (d : A) + t • theta (d : A) = phi (d : A) at hv 225 change s • psi (d : A) + t • theta (d : A) = chi d 226 simpa only [hphi.2 d] using hv 227 have hends := hchi.2 psiD hpsiD thetaD hthetaD hsegD 228 intro d 229 exact congrArg (fun q : D →L[ℂ] ℂ => q d) hends.1 230 231 /-- Every character of a unital star subalgebra has a pure state extension 232 to the ambient C-star algebra. -/ 233 theorem exists_pureState_extension (D : StarSubalgebra ℂ A) [IsClosed (D : Set A)] 234 (chi : WeakDual.characterSpace ℂ D) : 235 ∃ phi : A →L[ℂ] ℂ, 236 phi ∈ stateSpace A ∧ IsPureState A phi ∧ ∀ d : D, phi d = chi d := by 237 obtain ⟨f, hfext⟩ := (isCompact_weakStateExtensionFace D chi).extremePoints_nonempty 238 (weakStateExtensionFace_nonempty D chi) 239 have hfstate : f ∈ (weakStateSpace A).extremePoints ℝ := 240 (isExtreme_weakStateExtensionFace D chi).extremePoints_subset_extremePoints hfext 241 refine ⟨f.toStrongDual, hfext.1.1, ?_, hfext.1.2⟩ 242 rw [IsPureState, mem_extremePoints_iff_left] 243 rw [mem_extremePoints_iff_left] at hfstate 244 refine ⟨hfstate.1, ?_⟩ 245 intro psi hpsi theta htheta hseg 246 let psi' : WeakDual ℂ A := StrongDual.toWeakDual psi 247 let theta' : WeakDual ℂ A := StrongDual.toWeakDual theta 248 have hseg' : f ∈ openSegment ℝ psi' theta' := by 249 rcases hseg with ⟨s, t, hs, ht, hst, hconv⟩ 250 refine ⟨s, t, hs, ht, hst, ?_⟩ 251 apply DFunLike.ext _ _ 252 intro a 253 change s • psi a + t • theta a = f a 254 exact congrArg (fun q : StrongDual ℂ A => q a) hconv 255 have heq : psi' = f := hfstate.2 psi' hpsi theta' htheta hseg' 256 apply ContinuousLinearMap.ext 257 intro a 258 exact congrArg (fun q : WeakDual ℂ A => q a) heq 259 260 end Extension 261 262 end MathlibAnnex.Analysis.CStarAlgebra