MATHLIBANNEX / CANONICAL DECLARATION CARD

Every operator in a singleton image is compact

MathlibAnnex.Analysis.CStarAlgebra.NonUnitalCStarRepresentation.isCompactOperator_map_of_singleton

theorem

Excludes a noncompact image by making one separating character take both zero and one on the same projection.

Statement

Let be a nonzero complex -algebra, with no unit assumed, let be a separable complex Hilbert space, and let represent the unique unitary-equivalence class of nonzero irreducible -representations of . Then

Assumptions

No simplicity or separability of is assumed. The argument uses faithfulness of on , not faithfulness of its unital extension on the whole unitization.

Conclusion

This proves the inclusion for the specified representation.

Proof route

Separate a noncompact self-adjoint image from the compact-preimage ideal in a maximal abelian subalgebra. Its character produces a rank-one projection which belongs to the ideal but has character value one.

Proof steps

  1. Suppose is noncompact. Write

    If both self-adjoint parts had compact images, their sum would too. Choose a self-adjoint part with noncompact . Write , , , and . Apply A maximal abelian subalgebra containing a self-adjoint element to the self-adjoint in the unital , obtaining a maximal abelian unital -subalgebra containing it. Such a is norm closed.

  2. For the representation , form The compact-preimage ideal and use Norm closedness of the compact-preimage ideal to obtain the closed ideal

    Commutativity makes it an ordinary ideal of the commutative -algebra . The element is outside , since . Apply A character separating a closed ideal to : obtain one character with and .

  3. The scalar character vanishes at , so . The closedness of and the singleton assumptions allow A unit eigenvector for a non-scalar character to give a unit vector with for all . Apply Preimages of all rank-one operators to , using separability of , and obtain with

  4. For , both and lie in , so

    Fix any and use the inner product linear in its second argument. The two products are

    and

    The last equality uses conjugate linearity in the first argument. Thus these operators commute.

  5. Write the same as with . Substituting and in the commutation identity and cancelling the scalar terms gives

    By Faithfulness on the original algebra, the original is injective; hence . Consequently

    This holds for every , so The commutant of a maximal abelian subalgebra gives . No injectivity of is used.

  6. The represented operator of is , which is compact. Thus and

    On the other hand, the eigenvector equation for this very element gives

    Since , this implies , contradicting its value zero. The original noncompact image is therefore impossible.

Main citations

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)
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.
[TopologicalSpace.SeparableSpace H] The complex Hilbert space is separable; this is used for the rank-one preimage theorem.
(pi : NonUnitalCStarRepresentation A H) The specified -representation ; no unit-preservation equation is required.
(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.
∀ a : A, IsCompactOperator (pi a) For every element of the original , its represented operator on is compact. This is one inclusion of ranges, not the assertion that every bounded operator is compact.

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

Accepted content SHA-256: f79220a4f16a92981cbec2e619933d9fb9036f47e6d4befb8d603d3251a50a10

Accepted source guide SHA-256: b6ba701dfb421c73c8e5234aa471c1e541b6c154fa2619ca1315fa315c63a54c

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Back to top ↑