Compact-operator model from a representative of the unique irreducible-representation class

MathlibAnnex.Analysis.CStarAlgebra.NonUnitalCStarRepresentation.faithful_and_compactOperatorModel_of_singleton

theorem

Shows that a representative of the unique irreducible-representation class on a separable Hilbert space is faithful and has image exactly K(H).

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 separability of A, prior faithfulness, or simplicity is assumed. π is injective and satisfies the full unbundled compact-operator model: every π(a) is compact and every compact T on H has an exact preimage in A.

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 separability of A, prior faithfulness, or simplicity is assumed.

Conclusion

π is injective and satisfies the full unbundled compact-operator model: every π(a) is compact and every compact T on H has an exact preimage in A.

Proof route

The source combines the faithfulness theorem for the unique-class representative with the compact-operator-model theorem. The latter gives compactness of every image and a preimage for every compact operator. This establishes the stated unbundled property; it does not construct a bundled StarAlgEquiv.

Main citations

• MathlibAnnex.Analysis.CStarAlgebra.IsCompactOperatorModel

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

• MathlibAnnex.Analysis.CStarAlgebra.NonUnitalCStarRepresentation.exists_preimage_of_compact_singleton

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

• MathlibAnnex.Analysis.CStarAlgebra.NonUnitalCStarRepresentation.isCompactOperator_map_of_singleton

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

Lean source signature (exact)

theorem faithful_and_compactOperatorModel_of_singleton [Nontrivial A]
    [TopologicalSpace.SeparableSpace H]
    (pi : NonUnitalCStarRepresentation A H)
    (hsingle : IsSingletonIrreducibleModel.{u, v, u} pi) :
    Function.Injective pi ∧ IsCompactOperatorModel pi

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