Exact source: MathlibAnnex/Analysis/CStarAlgebra/Representation/UniqueModelConsequences.lean, lines 29–54.
Back to Closed-ideal simplicity of the shell-generated algebra
1import MathlibAnnex.Analysis.CStarAlgebra.CompactModel 2import MathlibAnnex.Analysis.CStarAlgebra.PureStateGNS.Ideal 3 4/-! 5# Consequences of ideal-separating pure GNS representations 6 7The representation-capture hypothesis remains explicit. The pure GNS 8representation used to test a proper closed ideal is constructed in 9`MathlibAnnex.CStarAlgebra.GNS.Ideal`; no KOS input occurs here. 10-/ 11 12set_option autoImplicit false 13 14open Set 15open scoped ComplexOrder 16 17namespace MathlibAnnex.CStarAlgebra 18 19open MathlibAnnex.Analysis.CStarAlgebra 20 21universe u v 22 23variable {A : Type u} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] 24variable {H : Type v} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] 25 26/-- A faithful displayed irreducible representation which captures every 27irreducible representation (in particular every canonical pure GNS 28representation) forces ordinary closed-two-sided-ideal simplicity. -/ 29theorem isSimpleCStarAlgebra_of_uniqueIrreducibleModel [Nontrivial A] 30 (pi : Representation A H) 31 (hmodel : Representation.IsUniqueIrreducibleModel.{u, v, u} pi) : 32 IsSimpleCStarAlgebra A := by 33 refine ⟨inferInstance, ?_⟩ 34 intro I hclosed 35 by_cases hI : I = ⊤ 36 · exact Or.inr hI 37 · left 38 apply le_antisymm 39 · intro x hx 40 obtain ⟨phi, hphi, _hpure, hirr, hann⟩ := 41 exists_irreducibleGNS_annihilating I hI hclosed 42 let f : A →ₚ[ℂ] ℂ := positiveLinearMapOfMemStateSpace phi hphi 43 obtain ⟨U, hU⟩ := hmodel.2.2 f.GNS f.gnsStarAlgHom hirr 44 have hpi : pi x = 0 := by 45 apply ContinuousLinearMap.ext 46 intro y 47 apply U.injective 48 calc 49 U (pi x y) = f.gnsStarAlgHom x (U y) := hU x y 50 _ = 0 := by rw [hann x hx]; rfl 51 _ = U 0 := (map_zero U).symm 52 have hxzero : x = 0 := hmodel.1 (by simpa using hpi) 53 exact hxzero 54 · exact bot_le 55 56end MathlibAnnex.CStarAlgebra