Exact source: MathlibAnnex/Analysis/CStarAlgebra/State/Ideal.lean
Pinned GitHub source · Raw UTF-8 source
Back to A faithful singleton model forces simplicity
1import MathlibAnnex.Analysis.CStarAlgebra.PureState2import MathlibAnnex.Analysis.CStarAlgebra.State.Irreducible34/-!5# Pure GNS representations separated from closed ideals6-/78set_option autoImplicit false910open Set11open scoped ComplexOrder InnerProduct1213namespace MathlibAnnex.Analysis.CStarAlgebra1415universe u1617variable {A : Type u} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A]1819/-- Simplicity with respect to norm-closed two-sided ideals. The definition20does not require a multiplicative unit. -/21def IsSimpleCStarAlgebra (A : Type u) [NonUnitalCStarAlgebra A] : Prop :=22 Nontrivial A ∧23 ∀ I : TwoSidedIdeal A, IsClosed (I : Set A) → I = ⊥ ∨ I = ⊤2425/-- A proper closed two-sided ideal is annihilated by a pure state. -/26theorem exists_pureState_annihilating [Nontrivial A]27 (I : TwoSidedIdeal A) (hI : I ≠ ⊤) (hclosed : IsClosed (I : Set A)) :28 ∃ phi : A →L[ℂ] ℂ,29 phi ∈ stateSpace A ∧ IsPureState A phi ∧30 ∀ x : A, x ∈ I → phi x = 0 := by31 obtain ⟨phi, hpure, hann⟩ := exists_extreme_state_annihilating I hI hclosed32 exact ⟨phi, hpure.1, hpure, hann⟩3334/-- An ideal element annihilated by a state acts as zero in its GNS35representation. -/36theorem gnsStarAlgHom_eq_zero_of_mem37 (phi : A →L[ℂ] ℂ) (hphi : phi ∈ stateSpace A)38 (I : TwoSidedIdeal A) (hann : ∀ x : A, x ∈ I → phi x = 0)39 {x : A} (hx : x ∈ I) :40 (positiveLinearMapOfMemStateSpace phi hphi).gnsStarAlgHom x = 0 := by41 let f : A →ₚ[ℂ] ℂ := positiveLinearMapOfMemStateSpace phi hphi42 let pi : Representation A f.GNS := f.gnsStarAlgHom43 let xi : f.GNS := f.gnsCyclicVector44 have hdense : DenseRange (StarAlgHom.orbitMap pi xi) :=45 PositiveLinearMap.denseRange_gnsStarAlgHom_apply_gnsCyclicVector f46 apply ContinuousLinearMap.ext47 intro y48 exact hdense.induction_on y49 (isClosed_eq (pi x).continuous continuous_const) fun a => by50 have hxa : x * a ∈ I := I.mul_mem_right x a hx51 have hsq : star (x * a) * (x * a) ∈ I :=52 I.mul_mem_left (star (x * a)) (x * a) hxa53 have hinner : inner ℂ (pi (x * a) xi) (pi (x * a) xi) = 0 := by54 calc55 inner ℂ (pi (x * a) xi) (pi (x * a) xi) =56 Representation.vectorFunctional pi xi57 (star (x * a) * (x * a)) := by58 simpa using59 (Representation.vectorFunctional_star_mul pi xi (x * a) (x * a)).symm60 _ = f (star (x * a) * (x * a)) :=61 PositiveLinearMap.inner_gnsCyclicVector_gnsStarAlgHom f _62 _ = phi (star (x * a) * (x * a)) := rfl63 _ = 0 := hann _ hsq64 have hzero : pi (x * a) xi = 0 := inner_self_eq_zero.mp hinner65 change (pi x * pi a) xi = 066 rw [← map_mul]67 exact hzero6869/-- A proper closed ideal has a nonzero irreducible GNS representation that70annihilates it. -/71theorem exists_irreducibleGNS_annihilating [Nontrivial A]72 (I : TwoSidedIdeal A) (hI : I ≠ ⊤) (hclosed : IsClosed (I : Set A)) :73 ∃ (phi : A →L[ℂ] ℂ) (hphi : phi ∈ stateSpace A),74 IsPureState A phi ∧75 Representation.IsIrreducible76 (positiveLinearMapOfMemStateSpace phi hphi).gnsStarAlgHom ∧77 ∀ x : A, x ∈ I →78 (positiveLinearMapOfMemStateSpace phi hphi).gnsStarAlgHom x = 0 := by79 obtain ⟨phi, hphi, hpure, hann⟩ :=80 exists_pureState_annihilating I hI hclosed81 let f : A →ₚ[ℂ] ℂ := positiveLinearMapOfMemStateSpace phi hphi82 let xi : f.GNS := f.gnsCyclicVector83 have hxi : ‖xi‖ = 1 :=84 PositiveLinearMap.norm_gnsCyclicVector f85 (positiveLinearMapOfMemStateSpace_one phi hphi)86 have hxi_ne : xi ≠ 0 := by87 intro hzero88 simp [hzero] at hxi89 letI : Nontrivial f.GNS := nontrivial_of_ne xi 0 hxi_ne90 have hirr : Representation.IsIrreducible f.gnsStarAlgHom :=91 (Representation.isIrreducible_iff_starAlgHom f.gnsStarAlgHom).292 (isIrreducible_pureState_gnsStarAlgHom phi hphi hpure)93 exact ⟨phi, hphi, hpure, hirr, fun x hx =>94 gnsStarAlgHom_eq_zero_of_mem phi hphi I hann hx⟩9596end MathlibAnnex.Analysis.CStarAlgebra