Exact source: MathlibAnnex/Analysis/CStarAlgebra/Representation/UniqueModelConsequences.lean
Pinned GitHub source · Raw UTF-8 source
Back to Closed-ideal simplicity of the shell-generated algebra
1import MathlibAnnex.Analysis.CStarAlgebra.CompactModel2import MathlibAnnex.Analysis.CStarAlgebra.PureStateGNS.Ideal34/-!5# Consequences of ideal-separating pure GNS representations67The representation-capture hypothesis remains explicit. The pure GNS8representation used to test a proper closed ideal is constructed in9`MathlibAnnex.CStarAlgebra.GNS.Ideal`; no KOS input occurs here.10-/1112set_option autoImplicit false1314open Set15open scoped ComplexOrder1617namespace MathlibAnnex.CStarAlgebra1819open MathlibAnnex.Analysis.CStarAlgebra2021universe u v2223variable {A : Type u} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A]24variable {H : Type v} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]2526/-- A faithful displayed irreducible representation which captures every27irreducible representation (in particular every canonical pure GNS28representation) 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 := by33 refine ⟨inferInstance, ?_⟩34 intro I hclosed35 by_cases hI : I = ⊤36 · exact Or.inr hI37 · left38 apply le_antisymm39 · intro x hx40 obtain ⟨phi, hphi, _hpure, hirr, hann⟩ :=41 exists_irreducibleGNS_annihilating I hI hclosed42 let f : A →ₚ[ℂ] ℂ := positiveLinearMapOfMemStateSpace phi hphi43 obtain ⟨U, hU⟩ := hmodel.2.2 f.GNS f.gnsStarAlgHom hirr44 have hpi : pi x = 0 := by45 apply ContinuousLinearMap.ext46 intro y47 apply U.injective48 calc49 U (pi x y) = f.gnsStarAlgHom x (U y) := hU x y50 _ = 0 := by rw [hann x hx]; rfl51 _ = U 0 := (map_zero U).symm52 have hxzero : x = 0 := hmodel.1 (by simpa using hpi)53 exact hxzero54 · exact bot_le5556end MathlibAnnex.CStarAlgebra