MATHLIBANNEX / CANONICAL DECLARATION CARD

Compact operators lie in a singleton representation range

MathlibAnnex.Analysis.CStarAlgebra.NonUnitalCStarRepresentation.exists_preimage_of_compact_singleton

theorem

Obtains the inclusion of all compact operators in the image of the original algebra.

Statement

Let be a nonzero complex -algebra, with no unit assumed, let be a separable complex Hilbert space, and let be a -representation representing the unique unitary-equivalence class of nonzero irreducible -representations of . If is compact, then Thus .

Assumptions

Separability is assumed for , not for . The singleton hypothesis includes nonzero irreducibility of and the universal unitary-equivalence condition. Faithfulness is not an input to this theorem.

Conclusion

The preimage belongs to itself. The reverse inclusion is a separate result.

Proof route

Use faithfulness to close the range, put every rank-one operator in it, and approximate an arbitrary compact operator by finite sums of rank-one operators.

Proof steps

  1. Use the inner product linear in its second argument. Apply Faithfulness of a non-unital singleton model to this nonzero ordered and this singleton model to obtain injectivity. An injective -homomorphism is isometric, so completeness of makes norm closed. Apply Every rank-one operator has a preimage to the same , using separability of , to obtain preimages of every operator . Additivity then supplies preimages of their finite sums.

  2. Here is the compact approximation in Compact approximation inside the closed representation range. For , the set is compact, so choose a finite -net for it. Let and let be its orthogonal projection. Since is finite dimensional, exists and minimizes distance to . For , choose with ; then

    Taking the operator norm gives .

  3. Choose an orthonormal basis of . By the inner-product convention just fixed,

    Step 1 puts this finite sum in ; the empty sum when is also allowed. Arbitrarily close such approximants place in the closure of , which equals . Unpacking membership gives the required .

Main citations

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
In the source Mathematical meaning
[Nontrivial A] The algebra is nonzero: . This condition does not say whether a unit is assumed; that information comes from the surrounding -algebra structure.
[PartialOrder A] [StarOrderedRing A] These typeclasses provide the usual order on a -algebra, equivalently when is positive. They are used by the state and positivity arguments.
[TopologicalSpace.SeparableSpace H] The Hilbert space has a countable dense subset; no separability of is imposed.
pi : NonUnitalCStarRepresentation A H The -representation , with no unit-preservation requirement.
hsingle : IsSingletonIrreducibleModel.{u, v, u} pi The specified representation is nonzero irreducible, and every nonzero irreducible -representation of the same algebra is unitarily equivalent to it.
(T : H →L[ℂ] H) (hT : IsCompactOperator T) A specified bounded complex-linear operator that maps bounded sets to relatively compact sets.
∃ a : A, pi a = T For this there is an element of the original algebra whose represented operator equals on all of .

Exact source and proof.

Read exact source with highlighted declaration · Raw UTF-8 source · Card PDF · Back to Project

Earlier published Card and PDF

Exact content identity

Declaration: MathlibAnnex.Analysis.CStarAlgebra.NonUnitalCStarRepresentation.exists_preimage_of_compact_singleton

Accepted content SHA-256: 3593258cf54fff6f9cd7afc24323a54b8790b170e38472e9a463b82324dde7a0

Accepted source guide SHA-256: c1010bd37214d8f3d3ffef75e6170fa0c50744e44483cf7f4f2e1a8f4904aa16

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Back to top ↑