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.

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.

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
In the source Mathematical meaning
H; Representation Limit H A complete complex Hilbert space and a unital complex-linear star homomorphism , with the completed CAR algebra. Its value at is a bounded complex-linear operator on .
rho; hrho : rho.IsIrreducible The representation is named in the text. Assume its action is nonzero and has no proper nonzero closed reducing subspace.
{a : Limit} An arbitrary element , inferred if possible from the compactness hypothesis; braces do not impose an additional condition on .
ha : IsCompactOperator (rho a) The operator is compact: the image of the closed unit ball has compact closure. Compactness is a property of its operator image, not of the element as a map.
a = 0 The conclusion is that itself is zero in , not just that is the zero operator.

Further source notes: 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 · Back to Project

Earlier published Card and PDF

Exact content identity

Declaration: MathlibAnnex.CStarAlgebra.CAR.eq_zero_of_isCompactOperator_image

Accepted content SHA-256: 00fd316c67ed3da3aa765b70633ce2e24039a792d2d14401f89ba81c6f781460

Accepted source guide SHA-256: d13fb3e33c31eaaa8e29c6302e742e4b39b2390883c7c3d82240697ce08bfe6a

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Back to top ↑