Exact source: MathlibAnnex/Analysis/CStarAlgebra/Representation/SimpleFaithful.lean, lines 23–39.
Back to Faithfulness of the target-state GNS representation
1import MathlibAnnex.Analysis.CStarAlgebra.Representation.VectorFunctional 2import Mathlib.RingTheory.TwoSidedIdeal.Kernel 3 4/-! 5# Faithfulness from the closed-ideal dichotomy 6 7Irreducibility is unnecessary here: a unital representation on a nonzero 8Hilbert space has proper kernel. This small lemma keeps the faithful-model 9argument independent of any separable irreducible-representation claim. 10-/ 11 12set_option autoImplicit false 13 14namespace MathlibAnnex.Analysis.CStarAlgebra.Representation 15 16universe u v 17variable {A : Type u} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] 18variable {H : Type v} [NormedAddCommGroup H] [InnerProductSpace ℂ H] 19 [CompleteSpace H] [Nontrivial H] 20 21/-- Every unital representation of an algebra with no nontrivial closed 22two-sided ideals is faithful, provided its Hilbert space is nonzero. -/ 23theorem injective_of_closed_ideal_dichotomy 24 (hA : ∀ I : TwoSidedIdeal A, IsClosed (I : Set A) → I = ⊥ ∨ I = ⊤) 25 (ρ : Representation A H) : Function.Injective ρ := by 26 let I : TwoSidedIdeal A := TwoSidedIdeal.ker ρ.toRingHom 27 have hclosed : IsClosed (I : Set A) := by 28 have hset : (I : Set A) = 29 (continuousLinearMap ρ) ⁻¹' ({0} : Set (H →L[ℂ] H)) := by 30 ext a 31 exact TwoSidedIdeal.mem_ker ρ.toRingHom 32 rw [hset] 33 exact isClosed_singleton.preimage (continuousLinearMap ρ).continuous 34 rcases hA I hclosed with hbot | htop 35 · exact (TwoSidedIdeal.ker_eq_bot ρ.toRingHom).mp hbot 36 · have hone : (1 : A) ∈ I := by rw [htop]; trivial 37 have hzero := (TwoSidedIdeal.mem_ker ρ.toRingHom).mp hone 38 have hbad : (1 : H →L[ℂ] H) = 0 := by simpa only [map_one] using hzero 39 exact (one_ne_zero hbad).elim 40 41end MathlibAnnex.Analysis.CStarAlgebra.Representation