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.

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.

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
In the source Mathematical meaning
Limit The fixed completed CAR algebra .
MathlibAnnex.CStarAlgebra.IsSimpleCStarAlgebra Limit The conclusion combines with: every norm-closed two-sided ideal is either or . It does not quantify over arbitrary nonclosed algebraic ideals.
isSimpleCStarAlgebra_limit A theorem about this fixed algebra, without a supplied representation. The root-state GNS representation mentioned in the Proof steps is used by the proof, not added as a hypothesis.

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

Earlier published Card and PDF

Exact content identity

Declaration: MathlibAnnex.CStarAlgebra.CAR.isSimpleCStarAlgebra_limit

Accepted content SHA-256: acf5eafa7756b2289ee490a885da3d73b66e3e2855468a26708cae01824f9b96

Accepted source guide SHA-256: fae31cbf7ac913c3e8784e2c79c0d184ba1c88251ff3cdb5867dfd85a3cac3c6

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Back to top ↑