Exact source: MathlibAnnex/Analysis/CStarAlgebra/State/Extension.lean
Pinned GitHub source · Raw UTF-8 source
Back to A character becomes a joint unit eigenvector · Back to A character extends to a pure state · Back to A pure state detects a nonzero square
1import Mathlib.Analysis.CStarAlgebra.GelfandDuality2import Mathlib.Analysis.Normed.Module.HahnBanach3import MathlibAnnex.Analysis.CStarAlgebra.PureState4import MathlibAnnex.Analysis.CStarAlgebra.State.Basic56/-!7# Pure extension of characters89Characters of a unital C-star subalgebra are pure states. Hahn--Banach and10Krein--Milman then give a pure state of the ambient algebra extending any11such character.12-/1314set_option autoImplicit false1516open Metric Set17open scoped ComplexOrder Convex1819namespace MathlibAnnex.Analysis.CStarAlgebra2021universe u2223variable {A : Type u} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A]2425local instance extensionWeakDualIsScalarTower : IsScalarTower ℝ ℂ (WeakDual ℂ A) :=26 inferInstanceAs (IsScalarTower ℝ ℂ (StrongDual ℂ A))2728local instance extensionWeakDualLocallyConvexSpace : LocallyConvexSpace ℝ (WeakDual ℂ A) :=29 inferInstanceAs (LocallyConvexSpace ℝ (WeakBilin (topDualPairing ℂ A)))3031/-- A continuous character of a unital C-star algebra is positive. -/32theorem character_nonnegative (chi : WeakDual.characterSpace ℂ A) :33 ∀ a : A, 0 ≤ a → 0 ≤ chi a := by34 intro a ha35 rw [StarOrderedRing.nonneg_iff] at ha ⊢36 induction ha using AddSubmonoid.closure_induction with37 | mem x hx =>38 obtain ⟨b, rfl⟩ := hx39 refine AddSubmonoid.subset_closure ⟨chi b, ?_⟩40 rw [map_mul, map_star]41 | zero => simp42 | add x y _ _ hx hy => simpa using AddSubmonoid.add_mem _ hx hy4344/-- A character, regarded as a continuous linear functional, is a state. -/45theorem character_mem_stateSpace (chi : WeakDual.characterSpace ℂ A) :46 WeakDual.CharacterSpace.toCLM chi ∈ stateSpace A :=47 ⟨character_nonnegative chi, map_one chi⟩4849/-- Every character of a unital C-star algebra is a pure state. -/50theorem isPureState_character (chi : WeakDual.characterSpace ℂ A) :51 IsPureState A (WeakDual.CharacterSpace.toCLM chi) := by52 rw [IsPureState, mem_extremePoints]53 refine ⟨character_mem_stateSpace chi, ?_⟩54 intro psi hpsi theta htheta hseg55 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 := by61 apply ContinuousLinearMap.ext62 intro a63 let x : A := a - algebraMap ℂ A (chi a)64 have hchix : chi x = 0 := by65 have hc : chi (algebraMap ℂ A (chi a)) = chi a := by66 simpa using AlgHomClass.commutes chi (chi a)67 calc68 chi x = chi a - chi (algebraMap ℂ A (chi a)) := by69 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 := by73 rw [map_mul, map_star, hchix]74 simp75 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 hvalue78 have hzero :79 r * (rho (star x * x)).re + q * (other (star x * x)).re = 0 := by80 have := congrArg Complex.re hvalue81 simpa [hchixx, Complex.real_smul] using this82 have hrho_nonneg := RCLike.nonneg_iff.mp83 (hrho.1 (star x * x) (star_mul_self_nonneg x))84 have hother_nonneg := RCLike.nonneg_iff.mp85 (hother.1 (star x * x) (star_mul_self_nonneg x))86 have hrho_re : (rho (star x * x)).re = 0 := by87 have hleft : 0 ≤ r * (rho (star x * x)).re :=88 mul_nonneg hr.le hrho_nonneg.189 have hright : 0 ≤ q * (other (star x * x)).re :=90 mul_nonneg hq.le hother_nonneg.191 have hmul : r * (rho (star x * x)).re = 0 := by linarith92 exact (mul_eq_zero.mp hmul).resolve_left hr.ne'93 have hrho_xx : rho (star x * x) = 0 := by94 apply Complex.ext95 · simpa using hrho_re96 · simpa using hrho_nonneg.297 have hrho_x : rho x = 0 :=98 apply_eq_zero_of_star_mul_self_eq_zero rho hrho.1 hrho_xx99 calc100 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 := by103 rw [hrho_x, zero_add, Algebra.algebraMap_eq_smul_one, map_smul, hrho.2]104 simp105 _ = WeakDual.CharacterSpace.toCLM chi a := rfl106 have hpsi_eq : psi = WeakDual.CharacterSpace.toCLM chi :=107 endpoint psi hpsi theta htheta s t hs ht hconv108 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⟩111112section Extension113114variable [Nontrivial A]115116/-- Weak-star states whose restriction to `D` equals `chi`. -/117def weakStateExtensionFace (D : StarSubalgebra ℂ A)118 (chi : WeakDual.characterSpace ℂ D) : Set (WeakDual ℂ A) :=119 {phi | phi ∈ weakStateSpace A ∧ ∀ d : D, phi d = chi d}120121private theorem character_norm_eq_one (D : StarSubalgebra ℂ A) [IsClosed (D : Set A)]122 (chi : WeakDual.characterSpace ℂ D) :123 ‖WeakDual.CharacterSpace.toCLM chi‖ = 1 := by124 apply le_antisymm125 · change ‖WeakDual.toStrongDual (chi : WeakDual ℂ D)‖ ≤ 1126 simpa using WeakDual.CharacterSpace.norm_le_norm_one chi127 · have h := (WeakDual.CharacterSpace.toCLM chi).le_opNorm (1 : D)128 simpa using h129130/-- Hahn--Banach extends a character to an ambient state. -/131theorem 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 := by134 let p : Submodule ℂ A := D.toSubalgebra.toSubmodule135 let f : StrongDual ℂ p := WeakDual.CharacterSpace.toCLM chi136 obtain ⟨phi, hext, hnorm⟩ := exists_extension_norm_eq p f137 have hfone : f (⟨1, D.one_mem⟩ : p) = 1 := by138 change chi (1 : D) = 1139 exact map_one chi140 have hphi_one : phi 1 = 1 := by141 calc142 phi 1 = f (⟨1, D.one_mem⟩ : p) := hext (⟨1, D.one_mem⟩ : p)143 _ = 1 := hfone144 have hphi_norm : ‖phi‖ ≤ 1 := by145 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 d150 simpa [p, f] using hext (show p from d)151152theorem isClosed_weakStateExtensionFace (D : StarSubalgebra ℂ A)153 (chi : WeakDual.characterSpace ℂ D) :154 IsClosed (weakStateExtensionFace D chi) := by155 simp only [weakStateExtensionFace, setOf_and, setOf_forall]156 exact isClosed_weakStateSpace.inter157 (isClosed_iInter fun d =>158 isClosed_eq (WeakDual.eval_continuous (d : A)) continuous_const)159160theorem weakStateExtensionFace_subset_closedBall (D : StarSubalgebra ℂ A)161 (chi : WeakDual.characterSpace ℂ D) :162 weakStateExtensionFace D chi ⊆163 WeakDual.toStrongDual ⁻¹' closedBall (0 : StrongDual ℂ A) 1 := by164 intro phi hphi165 simpa only [mem_preimage, mem_closedBall_zero_iff] using166 norm_le_one_of_mem_weakStateSpace hphi.1167168theorem 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_subset172 (isClosed_weakStateExtensionFace D chi)173 (weakStateExtensionFace_subset_closedBall D chi)174175theorem weakStateExtensionFace_nonempty (D : StarSubalgebra ℂ A) [IsClosed (D : Set A)]176 (chi : WeakDual.characterSpace ℂ D) :177 (weakStateExtensionFace D chi).Nonempty := by178 obtain ⟨phi, hphi, hext⟩ := exists_state_extension D chi179 exact ⟨StrongDual.toWeakDual phi, hphi, hext⟩180181/-- The extension set is a face of the ambient state space. -/182theorem isExtreme_weakStateExtensionFace (D : StarSubalgebra ℂ A) [IsClosed (D : Set A)]183 (chi : WeakDual.characterSpace ℂ D) :184 IsExtreme ℝ (weakStateSpace A) (weakStateExtensionFace D chi) := by185 let spectralOrderD : PartialOrder D := CStarAlgebra.spectralOrder D186 letI : LE D := spectralOrderD.toLE187 letI : LT D := spectralOrderD.toLT188 letI : PartialOrder D := spectralOrderD189 letI : StarOrderedRing D := CStarAlgebra.spectralOrderedRing D190 have coe_nonnegative {d : D} (hd : 0 ≤ d) : 0 ≤ (d : A) := by191 rw [StarOrderedRing.nonneg_iff] at hd192 induction hd using AddSubmonoid.closure_induction with193 | mem x hx =>194 obtain ⟨y, rfl⟩ := hx195 simpa using star_mul_self_nonneg (y : A)196 | zero => simp197 | add x y _ _ hx hy =>198 simpa using add_nonneg hx hy199 refine ⟨fun _ h => h.1, ?_⟩200 intro psi hpsi theta htheta phi hphi hseg201 refine ⟨hpsi, ?_⟩202 let p : Submodule ℂ A := D.toSubalgebra.toSubmodule203 let psiD : D →L[ℂ] ℂ := psi.toStrongDual.comp p.subtypeL204 let thetaD : D →L[ℂ] ℂ := theta.toStrongDual.comp p.subtypeL205 have hpsiD : psiD ∈ stateSpace D := by206 refine ⟨?_, ?_⟩207 · intro d hd208 exact hpsi.1 (d : A) (coe_nonnegative hd)209 · exact hpsi.2210 have hthetaD : thetaD ∈ stateSpace D := by211 refine ⟨?_, ?_⟩212 · intro d hd213 exact htheta.1 (d : A) (coe_nonnegative hd)214 · exact htheta.2215 have hchi := isPureState_character chi216 rw [IsPureState, mem_extremePoints] at hchi217 have hsegD : WeakDual.CharacterSpace.toCLM chi ∈218 openSegment ℝ psiD thetaD := by219 rcases hseg with ⟨s, t, hs, ht, hst, hconv⟩220 refine ⟨s, t, hs, ht, hst, ?_⟩221 apply ContinuousLinearMap.ext222 intro d223 have hv := congrArg (fun q : WeakDual ℂ A => q (d : A)) hconv224 change s • psi (d : A) + t • theta (d : A) = phi (d : A) at hv225 change s • psi (d : A) + t • theta (d : A) = chi d226 simpa only [hphi.2 d] using hv227 have hends := hchi.2 psiD hpsiD thetaD hthetaD hsegD228 intro d229 exact congrArg (fun q : D →L[ℂ] ℂ => q d) hends.1230231/-- Every character of a unital star subalgebra has a pure state extension232to the ambient C-star algebra. -/233theorem 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 := by237 obtain ⟨f, hfext⟩ := (isCompact_weakStateExtensionFace D chi).extremePoints_nonempty238 (weakStateExtensionFace_nonempty D chi)239 have hfstate : f ∈ (weakStateSpace A).extremePoints ℝ :=240 (isExtreme_weakStateExtensionFace D chi).extremePoints_subset_extremePoints hfext241 refine ⟨f.toStrongDual, hfext.1.1, ?_, hfext.1.2⟩242 rw [IsPureState, mem_extremePoints_iff_left]243 rw [mem_extremePoints_iff_left] at hfstate244 refine ⟨hfstate.1, ?_⟩245 intro psi hpsi theta htheta hseg246 let psi' : WeakDual ℂ A := StrongDual.toWeakDual psi247 let theta' : WeakDual ℂ A := StrongDual.toWeakDual theta248 have hseg' : f ∈ openSegment ℝ psi' theta' := by249 rcases hseg with ⟨s, t, hs, ht, hst, hconv⟩250 refine ⟨s, t, hs, ht, hst, ?_⟩251 apply DFunLike.ext _ _252 intro a253 change s • psi a + t • theta a = f a254 exact congrArg (fun q : StrongDual ℂ A => q a) hconv255 have heq : psi' = f := hfstate.2 psi' hpsi theta' htheta hseg'256 apply ContinuousLinearMap.ext257 intro a258 exact congrArg (fun q : WeakDual ℂ A => q a) heq259260end Extension261262end MathlibAnnex.Analysis.CStarAlgebra