Exact source: MathlibAnnex/Analysis/CStarAlgebra/Representation/Faithful.lean
Pinned GitHub source · Raw UTF-8 source
Back to Faithfulness from a unique irreducible class · Back to A pure state detects a nonzero square
1import Mathlib.Analysis.CStarAlgebra.GelfandDuality2import MathlibAnnex.Analysis.CStarAlgebra.Representation.Singleton3import MathlibAnnex.Analysis.CStarAlgebra.State.Extension45/-!6# Faithfulness from a singleton irreducible model78Pure states obtained by extending characters of singly generated commutative9C-star subalgebras separate the points of a unital C-star algebra. Comparing10their irreducible GNS representations with a singleton irreducible model then11forces that model to be faithful.12-/1314set_option autoImplicit false1516open Set17open scoped ComplexOrder InnerProduct1819namespace MathlibAnnex.Analysis.CStarAlgebra2021universe u v2223variable {A : Type u} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A]24variable {H : Type v}25variable [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]2627/-- Every nonzero element is detected, after forming `a⋆a`, by a pure state.28The construction uses only the commutative C-star algebra generated by29`a⋆a`, so no separability hypothesis on the ambient algebra is involved. -/30theorem 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 := by34 let b : A := star a * a35 have hb : b ≠ 0 := by36 simpa only [b, CStarRing.star_mul_self_ne_zero_iff] using ha37 letI : IsStarNormal b := (IsSelfAdjoint.star_mul_self a).isStarNormal38 have hbself : IsSelfAdjoint b := by39 simpa only [b] using IsSelfAdjoint.star_mul_self a40 let D : StarSubalgebra ℂ A := StarAlgebra.elemental ℂ b41 let bd : D := ⟨b, StarAlgebra.elemental.self_mem ℂ b⟩42 obtain ⟨z, hzmem, hzrad⟩ := spectrum.exists_nnnorm_eq_spectralRadius b43 have hz : z ≠ 0 := by44 intro hzero45 subst z46 have hnorm : ‖b‖₊ = 0 := by47 apply ENNReal.coe_injective48 change (↑‖b‖₊ : ENNReal) = (0 : ENNReal)49 rw [← hbself.spectralRadius_eq_nnnorm]50 simpa using hzrad.symm51 exact hb (nnnorm_eq_zero.mp hnorm)52 obtain ⟨chi, hchi⟩ :=53 (StarAlgebra.elemental.bijective_characterSpaceToSpectrum b).254 (⟨z, hzmem⟩ : spectrum ℂ b)55 have hchi_ne : chi bd ≠ 0 := by56 have hvalue := congrArg Subtype.val hchi57 change chi bd = z at hvalue58 exact hvalue.symm ▸ hz59 letI : IsClosed (D : Set A) := StarAlgebra.elemental.isClosed ℂ b60 obtain ⟨phi, hphi, hpure, hext⟩ := exists_pureState_extension D chi61 refine ⟨phi, hphi, hpure, ?_⟩62 have hvalue := hext bd63 change phi b = chi bd at hvalue64 exact fun hzero => hchi_ne (hvalue ▸ hzero)6566namespace Representation6768/-- A unital representation representing the sole unitary-equivalence class69of nonzero irreducible representations is faithful. -/70theorem injective_of_singleton [Nontrivial A]71 (pi : Representation A H)72 (hsingle : IsSingletonIrreducibleModel.{u, v, u} pi) :73 Function.Injective pi := by74 intro x y hxy75 let a : A := x - y76 have ha : pi a = 0 := by77 simp only [a, map_sub, hxy, sub_self]78 have hazero : a = 0 := by79 by_contra hane80 obtain ⟨phi, hphi, hpure, hdetect⟩ :=81 exists_pureState_nonzero_on_star_mul_self hane82 let f : A →ₚ[ℂ] ℂ := positiveLinearMapOfMemStateSpace phi hphi83 let xi : f.GNS := f.gnsCyclicVector84 have hxi : ‖xi‖ = 1 :=85 PositiveLinearMap.norm_gnsCyclicVector f86 (positiveLinearMapOfMemStateSpace_one phi hphi)87 have hxi_ne : xi ≠ 0 := by88 intro hzero89 simp [hzero] at hxi90 letI : Nontrivial f.GNS := nontrivial_of_ne xi 0 hxi_ne91 have hirr : Representation.IsIrreducible f.gnsStarAlgHom :=92 (Representation.isIrreducible_iff_starAlgHom f.gnsStarAlgHom).293 (isIrreducible_pureState_gnsStarAlgHom phi hphi hpure)94 obtain ⟨U, hU⟩ := hsingle.2 f.GNS f.gnsStarAlgHom hirr95 have hfa : f.gnsStarAlgHom a = 0 := by96 apply ContinuousLinearMap.ext97 intro z98 obtain ⟨q, rfl⟩ := U.surjective z99 calc100 f.gnsStarAlgHom a (U q) = U (pi a q) := (hU a q).symm101 _ = 0 := by rw [ha]; simp102 apply hdetect103 calc104 phi (star a * a) =105 inner ℂ xi (f.gnsStarAlgHom (star a * a) xi) :=106 (PositiveLinearMap.inner_gnsCyclicVector_gnsStarAlgHom f _).symm107 _ = 0 := by rw [map_mul, map_star, hfa]; simp108 exact sub_eq_zero.mp hazero109110end Representation111112end MathlibAnnex.Analysis.CStarAlgebra