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

MathlibAnnex.Analysis.CStarAlgebra.Representation.faithful_and_compactOperatorModel_of_singleton_amongNonUnital

theorem

Shows that a separably acting unital representative of the unique irreducible-representation class is faithful and has image exactly K(H).

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. π is injective; its underlying nonunital star homomorphism is injective, maps every a∈A to a compact operator, and represents every compact operator on H.

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

π is injective; its underlying nonunital star homomorphism is injective, maps every a∈A to a compact operator, and represents every compact operator on H.

Proof route

The source passes from the nonunital-interface formulation of the unique-class condition to its unital formulation and applies the unital faithful-and-compact-model theorem. The model entails injectivity, compactness of each image and a preimage for every compact T; no bundled StarAlgEquiv is produced.

Main citations

• MathlibAnnex.Analysis.CStarAlgebra.IsCompactOperatorModel

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

• 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.

• MathlibAnnex.Analysis.CStarAlgebra.Representation.surjective_of_irreducible_of_finiteDimensional

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

Lean source signature (exact)

theorem faithful_and_compactOperatorModel_of_singleton_amongNonUnital
    [Nontrivial A] [TopologicalSpace.SeparableSpace H]
    (pi : Representation A H)
    (hsingle : IsSingletonIrreducibleModelAmongNonUnital.{u, v, u} pi) :
    Function.Injective pi ∧
      IsCompactOperatorModel pi.toNonUnitalStarAlgHom

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