Exact source: MathlibAnnex/Analysis/CStarAlgebra/Representation/SimpleFaithful.lean
Pinned GitHub source · Raw UTF-8 source
Back to Faithfulness of the target-state GNS representation
1import MathlibAnnex.Analysis.CStarAlgebra.Representation.VectorFunctional2import Mathlib.RingTheory.TwoSidedIdeal.Kernel34/-!5# Faithfulness from the closed-ideal dichotomy67Irreducibility is unnecessary here: a unital representation on a nonzero8Hilbert space has proper kernel. This small lemma keeps the faithful-model9argument independent of any separable irreducible-representation claim.10-/1112set_option autoImplicit false1314namespace MathlibAnnex.Analysis.CStarAlgebra.Representation1516universe u v17variable {A : Type u} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A]18variable {H : Type v} [NormedAddCommGroup H] [InnerProductSpace ℂ H]19 [CompleteSpace H] [Nontrivial H]2021/-- Every unital representation of an algebra with no nontrivial closed22two-sided ideals is faithful, provided its Hilbert space is nonzero. -/23theorem injective_of_closed_ideal_dichotomy24 (hA : ∀ I : TwoSidedIdeal A, IsClosed (I : Set A) → I = ⊥ ∨ I = ⊤)25 (ρ : Representation A H) : Function.Injective ρ := by26 let I : TwoSidedIdeal A := TwoSidedIdeal.ker ρ.toRingHom27 have hclosed : IsClosed (I : Set A) := by28 have hset : (I : Set A) =29 (continuousLinearMap ρ) ⁻¹' ({0} : Set (H →L[ℂ] H)) := by30 ext a31 exact TwoSidedIdeal.mem_ker ρ.toRingHom32 rw [hset]33 exact isClosed_singleton.preimage (continuousLinearMap ρ).continuous34 rcases hA I hclosed with hbot | htop35 · exact (TwoSidedIdeal.ker_eq_bot ρ.toRingHom).mp hbot36 · have hone : (1 : A) ∈ I := by rw [htop]; trivial37 have hzero := (TwoSidedIdeal.mem_ker ρ.toRingHom).mp hone38 have hbad : (1 : H →L[ℂ] H) = 0 := by simpa only [map_one] using hzero39 exact (one_ne_zero hbad).elim4041end MathlibAnnex.Analysis.CStarAlgebra.Representation