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

MathlibAnnex.Analysis.CStarAlgebra.Representation.finiteDimensional_space_of_singleton

theorem

Shows that the Hilbert space of a separably acting unital 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 representation of A on H that is a representative of the unique unitary-equivalence class of nonzero irreducible representations of A. H is finite-dimensional over ℂ. The conclusion is conditional on the unique-class hypothesis, not a statement about all unital irreducible representations.

Assumptions

Let A be a nonzero unital complex C*-algebra, H a separable 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.

Conclusion

H is finite-dimensional over ℂ. The conclusion is conditional on the unique-class hypothesis, not a statement about all unital irreducible representations.

Proof route

The source first obtains injectivity and simplicity from the unique-class hypothesis for π, then a nonzero scalar-corner projection with compact image. The compact-preimage ideal is nonzero and closed, hence all of A by simplicity. Thus π(1)=id_H is compact, and the compact-identity criterion makes H finite-dimensional.

Main citations

• MathlibAnnex.Analysis.CStarAlgebra.IsMaximalAbelian

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

• MathlibAnnex.Analysis.CStarAlgebra.Representation.isSimpleCStarAlgebra_of_singleton_of_injective

  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.CStarAlgebra.compactPreimageIdeal

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

• MathlibAnnex.Topology.exists_isOpen_singleton

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

Lean source signature (exact)

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

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