No separably acting representative of all nonzero irreducible representations

MathlibAnnex.Analysis.CStarAlgebra.Representation.not_singleton_amongNonUnital_of_infiniteDimensional

theorem

Shows that, for an infinite-dimensional unital C*-algebra, no representation on a separable Hilbert space is a representative of the unique unitary-equivalence class of all nonzero irreducible representations.

Statement

Let A be a nonzero infinite-dimensional unital complex C*-algebra, H a separable complex Hilbert space, and π a unital representation of A on H. The representation π is not a representative of the unique unitary-equivalence class of nonzero irreducible representations of A. Equivalently, π is not both irreducible and unitarily equivalent to every nonzero irreducible representation of A. This does not rule out separable irreducible representations in general.

Assumptions

Let A be a nonzero infinite-dimensional unital complex C*-algebra, H a separable complex Hilbert space, and π a unital representation of A on H.

Conclusion

The representation π is not a representative of the unique unitary-equivalence class of nonzero irreducible representations of A. Equivalently, π is not both irreducible and unitarily equivalent to every nonzero irreducible representation of A. This does not rule out separable irreducible representations in general.

Proof route

If π represented the unique irreducible-representation class of A, the preceding finite-dimensional-algebra theorem would force A to be finite-dimensional, contradicting the hypothesis.

Main citations

• MathlibAnnex.Analysis.CStarAlgebra.Representation.finiteDimensional_algebra_of_singleton_amongNonUnital

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

Lean source signature (exact)

theorem not_singleton_amongNonUnital_of_infiniteDimensional
    [Nontrivial A] (hA : ¬ FiniteDimensional ℂ A)
    [TopologicalSpace.SeparableSpace H]
    (pi : Representation A H) :
    ¬ IsSingletonIrreducibleModelAmongNonUnital.{u, v, u} pi

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