MATHLIBANNEX / EXACT SOURCE v0.4.0
MathlibAnnex.Analysis.CStarAlgebra.exists_pureState_nonzero_on_star_mul_self
theorem exists_pureState_nonzero_on_star_mul_self [Nontrivial A]
{a : A} (ha : a ≠ 0) :
∃ phi : A →L[ℂ] ℂ,
phi ∈ stateSpace A ∧ IsPureState A phi ∧ phi (star a * a) ≠ 01 import Mathlib.Analysis.CStarAlgebra.GelfandDuality 2 import MathlibAnnex.Analysis.CStarAlgebra.Representation.Singleton 3 import MathlibAnnex.Analysis.CStarAlgebra.State.Extension 4 5 /-! 6 # Faithfulness from a singleton irreducible model 7 8 Pure states obtained by extending characters of singly generated commutative 9 C-star subalgebras separate the points of a unital C-star algebra. Comparing 10 their irreducible GNS representations with a singleton irreducible model then 11 forces that model to be faithful. 12 -/ 13 14 set_option autoImplicit false 15 16 open Set 17 open scoped ComplexOrder InnerProduct 18 19 namespace MathlibAnnex.Analysis.CStarAlgebra 20 21 universe u v 22 23 variable {A : Type u} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] 24 variable {H : Type v} 25 variable [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] 26 27 /-- Every nonzero element is detected, after forming `a⋆a`, by a pure state. 28 The construction uses only the commutative C-star algebra generated by 29 `a⋆a`, so no separability hypothesis on the ambient algebra is involved. -/ 30 theorem exists_pureState_nonzero_on_star_mul_self [Nontrivial A] 31 {a : A} (ha : a ≠ 0) : 32 ∃ phi : A →L[ℂ] ℂ, 33 phi ∈ stateSpace A ∧ IsPureState A phi ∧ phi (star a * a) ≠ 0 := by 34 let b : A := star a * a 35 have hb : b ≠ 0 := by 36 simpa only [b, CStarRing.star_mul_self_ne_zero_iff] using ha 37 letI : IsStarNormal b := (IsSelfAdjoint.star_mul_self a).isStarNormal 38 have hbself : IsSelfAdjoint b := by 39 simpa only [b] using IsSelfAdjoint.star_mul_self a 40 let D : StarSubalgebra ℂ A := StarAlgebra.elemental ℂ b 41 let bd : D := ⟨b, StarAlgebra.elemental.self_mem ℂ b⟩ 42 obtain ⟨z, hzmem, hzrad⟩ := spectrum.exists_nnnorm_eq_spectralRadius b 43 have hz : z ≠ 0 := by 44 intro hzero 45 subst z 46 have hnorm : ‖b‖₊ = 0 := by 47 apply ENNReal.coe_injective 48 change (↑‖b‖₊ : ENNReal) = (0 : ENNReal) 49 rw [← hbself.spectralRadius_eq_nnnorm] 50 simpa using hzrad.symm 51 exact hb (nnnorm_eq_zero.mp hnorm) 52 obtain ⟨chi, hchi⟩ := 53 (StarAlgebra.elemental.bijective_characterSpaceToSpectrum b).2 54 (⟨z, hzmem⟩ : spectrum ℂ b) 55 have hchi_ne : chi bd ≠ 0 := by 56 have hvalue := congrArg Subtype.val hchi 57 change chi bd = z at hvalue 58 exact hvalue.symm ▸ hz 59 letI : IsClosed (D : Set A) := StarAlgebra.elemental.isClosed ℂ b 60 obtain ⟨phi, hphi, hpure, hext⟩ := exists_pureState_extension D chi 61 refine ⟨phi, hphi, hpure, ?_⟩ 62 have hvalue := hext bd 63 change phi b = chi bd at hvalue 64 exact fun hzero => hchi_ne (hvalue ▸ hzero) 65 66 namespace Representation 67 68 /-- A unital representation representing the sole unitary-equivalence class 69 of nonzero irreducible representations is faithful. -/ 70 theorem injective_of_singleton [Nontrivial A] 71 (pi : Representation A H) 72 (hsingle : IsSingletonIrreducibleModel.{u, v, u} pi) : 73 Function.Injective pi := by 74 intro x y hxy 75 let a : A := x - y 76 have ha : pi a = 0 := by 77 simp only [a, map_sub, hxy, sub_self] 78 have hazero : a = 0 := by 79 by_contra hane 80 obtain ⟨phi, hphi, hpure, hdetect⟩ := 81 exists_pureState_nonzero_on_star_mul_self hane 82 let f : A →ₚ[ℂ] ℂ := positiveLinearMapOfMemStateSpace phi hphi 83 let xi : f.GNS := f.gnsCyclicVector 84 have hxi : ‖xi‖ = 1 := 85 PositiveLinearMap.norm_gnsCyclicVector f 86 (positiveLinearMapOfMemStateSpace_one phi hphi) 87 have hxi_ne : xi ≠ 0 := by 88 intro hzero 89 simp [hzero] at hxi 90 letI : Nontrivial f.GNS := nontrivial_of_ne xi 0 hxi_ne 91 have hirr : Representation.IsIrreducible f.gnsStarAlgHom := 92 (Representation.isIrreducible_iff_starAlgHom f.gnsStarAlgHom).2 93 (isIrreducible_pureState_gnsStarAlgHom phi hphi hpure) 94 obtain ⟨U, hU⟩ := hsingle.2 f.GNS f.gnsStarAlgHom hirr 95 have hfa : f.gnsStarAlgHom a = 0 := by 96 apply ContinuousLinearMap.ext 97 intro z 98 obtain ⟨q, rfl⟩ := U.surjective z 99 calc 100 f.gnsStarAlgHom a (U q) = U (pi a q) := (hU a q).symm 101 _ = 0 := by rw [ha]; simp 102 apply hdetect 103 calc 104 phi (star a * a) = 105 inner ℂ xi (f.gnsStarAlgHom (star a * a) xi) := 106 (PositiveLinearMap.inner_gnsCyclicVector_gnsStarAlgHom f _).symm 107 _ = 0 := by rw [map_mul, map_star, hfa]; simp 108 exact sub_eq_zero.mp hazero 109 110 end Representation 111 112 end MathlibAnnex.Analysis.CStarAlgebra