Exact source: MathlibAnnex/Analysis/CStarAlgebra/Representation/Singleton.lean
Pinned GitHub source · Raw UTF-8 source
Back to A unital singleton model acts in finite dimension · Back to A faithful singleton model forces simplicity
1import MathlibAnnex.Analysis.CStarAlgebra.State.Ideal23/-!4# A single unitary-equivalence class of irreducible representations5-/67set_option autoImplicit false89open scoped ComplexOrder1011namespace MathlibAnnex.Analysis.CStarAlgebra1213universe u v w1415variable {A : Type u} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A]16variable {H : Type v}17variable [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]1819namespace Representation2021/-- The represented irreducible is a model for every irreducible22representation. Faithfulness is deliberately not part of this predicate. -/23def IsSingletonIrreducibleModel (pi : Representation A H) : Prop :=24 pi.IsIrreducible ∧25 ∀ (K : Type w) [NormedAddCommGroup K] [InnerProductSpace ℂ K]26 [CompleteSpace K] (rho : Representation A K),27 rho.IsIrreducible → pi.UnitaryEquivalent rho2829/-- Once faithfulness has been proved separately, a singleton irreducible30model forces closed-two-sided-ideal simplicity. -/31theorem isSimpleCStarAlgebra_of_singleton_of_injective [Nontrivial A]32 (pi : Representation A H)33 (hsingle : IsSingletonIrreducibleModel.{u, v, u} pi)34 (hinj : Function.Injective pi) : IsSimpleCStarAlgebra A := by35 refine ⟨inferInstance, ?_⟩36 intro I hclosed37 by_cases hI : I = ⊤38 · exact Or.inr hI39 · left40 apply le_antisymm41 · intro x hx42 obtain ⟨phi, hphi, _hpure, hirr, hann⟩ :=43 exists_irreducibleGNS_annihilating I hI hclosed44 let f : A →ₚ[ℂ] ℂ := positiveLinearMapOfMemStateSpace phi hphi45 obtain ⟨U, hU⟩ := hsingle.2 f.GNS f.gnsStarAlgHom hirr46 have hpi : pi x = 0 := by47 apply ContinuousLinearMap.ext48 intro y49 apply U.injective50 calc51 U (pi x y) = f.gnsStarAlgHom x (U y) := hU x y52 _ = 0 := by rw [hann x hx]; rfl53 _ = U 0 := (map_zero U).symm54 exact hinj (by simpa using hpi)55 · exact bot_le5657end Representation5859end MathlibAnnex.Analysis.CStarAlgebra