Compact image of a representative of the unique irreducible-representation class

MathlibAnnex.Analysis.CStarAlgebra.NonUnitalCStarRepresentation.isCompactOperator_map_of_singleton

theorem

Shows that every operator in the image of a separably acting representative of the unique irreducible-representation class is compact.

Statement

Let A be a nonzero complex C*-algebra, not assumed unital, 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. No simplicity assumption is made. Every operator π(a), a∈A, is compact.

Assumptions

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

Conclusion

Every operator π(a), a∈A, is compact.

Proof route

Assuming a noncompact image, the source takes a noncompact self-adjoint part and embeds it in a maximal abelian unitization subalgebra D. The closed compact-preimage ideal in D does not contain that element; character separation produces χ. The eigenvector associated with a character distinct from the scalar character and a compact rank-one projection contradict χ's annihilation of the ideal. This follows the source's character route, not a norm-separable pure-state plan.

Main citations

• MathlibAnnex.Analysis.CStarAlgebra.NonUnitalCStarRepresentation.exists_preimage_rankOne_of_singleton

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

• MathlibAnnex.Analysis.CStarAlgebra.exists_character_annihilating_closedIdeal_of_not_mem

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

• MathlibAnnex.CStarAlgebra.compactPreimageIdeal

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

Lean source signature (exact)

theorem isCompactOperator_map_of_singleton [Nontrivial A]
    [TopologicalSpace.SeparableSpace H]
    (pi : NonUnitalCStarRepresentation A H)
    (hsingle : IsSingletonIrreducibleModel.{u, v, u} pi) :
    ∀ a : A, IsCompactOperator (pi a)

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