Simplicity from a faithful representative of the unique irreducible-representation class

MathlibAnnex.Analysis.CStarAlgebra.Representation.isSimpleCStarAlgebra_of_singleton_of_injective

theorem

Converts a faithful representative of the unique irreducible-representation class into closed-two-sided-ideal simplicity of the algebra.

Statement

Let A be a nonzero unital complex C*-algebra, H a complex Hilbert space, and π a representation of A on H that is a representative of the unique unitary-equivalence class of nonzero irreducible representations of A. Assume additionally that π is injective. No separability assumption on H is required. A is simple in the exact closed-two-sided-ideal sense IsSimpleCStarAlgebra A.

Assumptions

Let A be a nonzero unital complex C*-algebra, H a complex Hilbert space, and π a representation of A on H that is a representative of the unique unitary-equivalence class of nonzero irreducible representations of A. Assume additionally that π is injective. No separability assumption on H is required.

Conclusion

A is simple in the exact closed-two-sided-ideal sense IsSimpleCStarAlgebra A.

Proof route

For a closed two-sided ideal I, the source splits I=⊤ from a proper I. In the proper case an irreducible GNS representation annihilating I belongs to the unique class represented by π; the intertwiner makes π vanish on each x∈I, and injectivity forces x=0, so I=⊥.

Main citations

• MathlibAnnex.Analysis.CStarAlgebra.isIrreducible_pureState_gnsStarAlgHom

  Exact formal dependency; inspect the linked Card and exact source.

Lean source signature (exact)

theorem isSimpleCStarAlgebra_of_singleton_of_injective [Nontrivial A]
    (pi : Representation A H)
    (hsingle : IsSingletonIrreducibleModel.{u, v, u} pi)
    (hinj : Function.Injective pi) : IsSimpleCStarAlgebra A

Read exact source with highlighted declaration · Raw UTF-8 source · Card PDF · Card JSON