Finite-dimensional space for a separable representative of the unique irreducible-representation class

MathlibAnnex.Analysis.CStarAlgebra.Representation.finiteDimensional_space_of_singleton_amongNonUnital

theorem

Shows that the Hilbert space of a separably acting representative of the unique irreducible-representation class is finite-dimensional.

Statement

Let A be a nonzero unital complex C*-algebra, H a separable complex Hilbert space, and π a unital representation of A on H that is a representative of the unique unitary-equivalence class of nonzero irreducible representations of A. Then H is finite-dimensional over ℂ.

Assumptions

Let A be a nonzero unital complex C*-algebra, H a separable complex Hilbert space, and π a unital representation of A on H that is a representative of the unique unitary-equivalence class of nonzero irreducible representations of A.

Conclusion

H is finite-dimensional over ℂ.

Proof route

The source passes from the nonunital-interface formulation of the unique-class condition to its unital formulation and applies the finite-dimensional-space theorem, whose compact-identity route yields the result.

Main citations

• MathlibAnnex.Analysis.CStarAlgebra.Representation.IsSingletonIrreducibleModelAmongNonUnital

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

• MathlibAnnex.Analysis.CStarAlgebra.Representation.finiteDimensional_space_of_singleton

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

Lean source signature (exact)

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

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