MATHLIBANNEX / CANONICAL DECLARATION CARD

Simplicity of the completed CAR algebra

MathlibAnnex.CStarAlgebra.CAR.isSimpleCStarAlgebra_limit

theorem

Every nonzero closed two-sided ideal of the CAR algebra contains the identity.

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. Then is nonzero and simple as a C*-algebra: for every norm-closed two-sided ideal , either or .

Assumptions

The algebra is the fixed completed CAR system above. Ideals are two-sided, and the stated simplicity property quantifies over norm-closed ideals. No representation is an extra assumption.

Conclusion

There is no proper nonzero closed two-sided ideal. The proof finds a finite-stage root projection in any nonzero ideal and uses simplicity of a full matrix algebra to force the unit into that ideal.

Proof route

Use the product-vector state , characterized by , and its root projections . Its GNS representation is faithful. Thus a nonzero ideal contains an element with . Root compression approximates closely enough to recover by multiplication with an invertible element. The ideal then contains the whole finite stage and hence .

Proof steps

  1. Let be the GNS representation of the positive normalized functional . Left multiplication obeys , so the action extends to the GNS completion and is contractive. On each full matrix stage it is injective and isometric. Density of the stage union extends the norm equality to every , proving faithfulness.

  2. If , the matrix-coefficient separation result for the cyclic root vector gives with . Put . Indeed, vanishing of all these coefficients would force the GNS operator of to vanish on its dense cyclic orbit, contradicting faithfulness.

  3. For sufficiently large , set and . The root-compression estimate gives . Hence is invertible by the Neumann-series criterion. Since , it follows that .

  4. The inverse image of in is a two-sided ideal containing the nonzero matrix unit . Simplicity of the full matrix algebra makes that inverse image all of . Its identity maps to , so .

Main citations

Lean source signature (exact)

theorem isSimpleCStarAlgebra_limit : MathlibAnnex.CStarAlgebra.IsSimpleCStarAlgebra Limit

Here Limit is , and IsSimpleCStarAlgebra Limit asserts nontriviality and the closed-two-sided-ideal alternative in the Statement. rootPositiveState is the positive form of ; its gnsStarAlgHom is . These objects occur in the cited proof route, not as extra parameters of the short final theorem.

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

Lean realization notes

The source obtains a stronger algebraic ideal fact on the way, but this Card states the selected closed-ideal simplicity theorem. The GNS representation used in the argument is constructed from the root state, rather than supplied as an additional hypothesis.

Exact Card identity

Language: en

CARD_CONTENT_COMPLETE

Card UID: lfh:lfh-declaration-card:sha256:d01780d70500992bccb2c17598d8cea950b7abc05535fe00cccfa4b9c4c41ee1

Card revision: 1 · SHA-256: 2244ff28318d41f3e5b2a408f2bedc931a02313217d3dbf06bda30342d3f9497

Exposition revision: 1 · SHA-256: acd5f695f6a7ac65a56746c2b970998868a6a24d1740ad2aaaebb48b0cd12d2a

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Header SHA-256: a96ca55074f190a5b4460596423a1d40d37f92c06235de4a6fa7790b872946fa

Back to top ↑