MATHLIBANNEX / CANONICAL DECLARATION CARD

An irreducible CAR representation has no nonzero compact image

MathlibAnnex.CStarAlgebra.CAR.eq_zero_of_isCompactOperator_image

theorem

Simplicity and infinite dimensionality rule out compact operators coming from nonzero CAR elements.

Statement

Let be the completed CAR algebra: the norm completion of the increasing union of under the unital embeddings (with the fixed coordinate reindexing). Write for the canonical isometric inclusion and for its matrix units. A representation is a unital complex star homomorphism into the bounded operators on a complex Hilbert space. Irreducibility means nonzero action and no proper nonzero closed reducing subspace. Let be irreducible on a complex Hilbert space . If and is compact, then . In particular .

Assumptions

The representation is unital and irreducible in the nonzero, closed-reducing-subspace sense. The space is complete. Compactness is assumed only for the represented operator .

Conclusion

No nonzero element of can act compactly in this representation. Faithfulness makes the vanishing conclusion a statement about itself, not merely about its image.

Proof route

Simplicity makes the nonzero unital representation faithful. The preimage of the compact operators is a closed two-sided ideal of . If it were all of , the identity on would be compact; this would make , and then the faithfully represented algebra , finite-dimensional. That contradicts infinite dimensionality of the CAR limit.

Proof steps

  1. The exact result representation_injective gives injectivity of from simplicity and the nonzero irreducible action.

  2. Let . Compact operators form a norm-closed two-sided ideal in , and the representation is continuous, so is a norm-closed two-sided ideal in .

  3. Simplicity yields or . In the second case is compact, so is finite-dimensional. Injectivity then embeds linearly in the finite-dimensional space , a contradiction. Therefore and .

Main citations

Lean source signature (exact)

theorem eq_zero_of_isCompactOperator_image
    (rho : Representation Limit H) (hrho : rho.IsIrreducible)
    {a : Limit} (ha : IsCompactOperator (rho a)) : a = 0

Here rho is , rho.IsIrreducible includes nonzero action, and IsCompactOperator (rho a) is the compactness of . Operators H →L[ℂ] H are bounded complex-linear maps. The source concludes a = 0; it does not only conclude that rho a vanishes.

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

Lean realization notes

This does not say that has no compact operators. It describes the intersection of its compact ideal with the represented CAR algebra. Infinite dimensionality of is a proved property of the fixed CAR limit, not an extra assumption on an arbitrary algebra.

Exact Card identity

Language: en

CARD_CONTENT_COMPLETE

Card UID: lfh:lfh-declaration-card:sha256:681004362f65370ff8743e0b17874135c5c9f291724bf7cd44c92d7fccd93c47

Card revision: 1 · SHA-256: 9892f57506259945bed6f87c5473fdeaef7cc54fcd944baf1b6bc42e834115e7

Exposition revision: 1 · SHA-256: 61307ca098e5a089ae180589d995aead4157dbae9f7503c4fea5a0bb576e8585

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Header SHA-256: edaadb9321c0a357b05f03c5a84367200e5f8e2ba339458e6d010736b149c539

Back to top ↑