Faithfulness of a representative of the unique irreducible-representation class

MathlibAnnex.Analysis.CStarAlgebra.NonUnitalCStarRepresentation.injective_of_singleton

theorem

Shows that a representative of the unique irreducible-representation class of a nonzero C*-algebra is faithful.

Statement

Let A be a nonzero complex C*-algebra, not assumed unital, 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. No separability assumption on H is required. Then π is injective.

Assumptions

Let A be a nonzero complex C*-algebra, not assumed unital, 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. No separability assumption on H is required.

Conclusion

Then π is injective.

Proof route

For π(x−y)=0, the source assumes x−y≠0, embeds it into the minimal unitization, and finds a pure state detecting its star-square. Its GNS representation restricts to a nonzero irreducible representation of A. The unique-class hypothesis gives a unitary equivalence to π, which would force the detected element to act as zero there, a contradiction.

Main citations

• MathlibAnnex.Analysis.CStarAlgebra.NonUnitalCStarRepresentation.IsSingletonIrreducibleModel

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

• MathlibAnnex.Analysis.CStarAlgebra.exists_pureState_nonzero_on_star_mul_self

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

• MathlibAnnex.Analysis.CStarAlgebra.isIrreducible_pureState_gnsStarAlgHom

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

Lean source signature (exact)

theorem injective_of_singleton [Nontrivial A]
    (pi : NonUnitalCStarRepresentation A H)
    (hsingle : IsSingletonIrreducibleModel.{u, v, u} pi) :
    Function.Injective pi

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