Preimages of every compact operator

MathlibAnnex.Analysis.CStarAlgebra.NonUnitalCStarRepresentation.exists_preimage_of_compact_singleton

theorem

Establishes the inclusion K(H) ⊆ π(A) by giving a preimage for every compact operator.

Statement

Let A be a nonzero complex C*-algebra, not assumed unital; let H be a separable complex Hilbert space; let π be a representation of A on H that is a representative of the unique unitary-equivalence class of nonzero irreducible representations of A; and let T be a compact bounded operator on H. There exists a∈A with π(a)=T. This is the inclusion K(H)⊆π(A); compactness of each π(a) is proved separately.

Assumptions

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

Conclusion

There exists a∈A with π(a)=T. This is the inclusion K(H)⊆π(A); compactness of each π(a) is proved separately.

Proof route

The source combines injectivity of π with the preimages of every rank-one operator, then applies the closed-range/compact-operator generation lemma to obtain an exact preimage of T.

Main citations

• MathlibAnnex.Analysis.CStarAlgebra.NonUnitalCStarRepresentation.exists_preimage_rankOne_of_singleton

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

Lean source signature (exact)

theorem exists_preimage_of_compact_singleton [Nontrivial A]
    [PartialOrder A] [StarOrderedRing A]
    [TopologicalSpace.SeparableSpace H]
    (pi : NonUnitalCStarRepresentation A H)
    (hsingle : IsSingletonIrreducibleModel.{u, v, u} pi)
    (T : H →L[ℂ] H) (hT : IsCompactOperator T) :
    ∃ a : A, pi a = T

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