MATHLIBANNEX / CANONICAL DECLARATION CARD

Closed-ideal simplicity of the shell-generated algebra

MathlibAnnex.CStarAlgebra.CAR.isSimpleCStarAlgebra_shellFamilyTarget

theorem

Uses a faithful irreducible representation in the unique unitary-equivalence class to rule out proper nonzero closed two-sided ideals.

Statement

For the fixed algebra described below, every norm-closed two-sided ideal satisfies or . The algebra is nonzero, so it is simple as a C*-algebra.

Assumptions

Let be the completed CAR algebra with matrix stages embedded by . Write for the image of the first diagonal matrix unit, , and for the root state characterized by on each stage, where is its canonical embedding.

Index chosen pure-state Gelfand-Naimark-Segal (GNS) representations by their unitary-equivalence classes , with root index and representative states .

A fixed shell family consists of complex-linear unital star automorphisms and elements satisfying , and .

At the root, is the identity and .

Let be the Hilbert direct sum of these GNS spaces, their representation of , and its embedded unit cyclic vector, where is the selected unit cyclic vector and is coordinate inclusion.

Choose once a family of unitary operators from the construction of the shell unitaries: , , and . Here denotes the bounded complex-linear operators on .

Put , the norm-closed unital star algebra generated by these operators. Let be with its codomain restricted to , and let be inclusion.

The ideals in this assertion are two-sided algebraic ideals whose underlying sets are norm closed. The family is supplied as input. The shell-model realization theorem provides the faithful source representation and irreducible inclusion; the universal capture theorem identifies every irreducible class with that inclusion.

Conclusion

The conclusion is simplicity with respect to closed two-sided ideals. It is not a claim that every algebraic ideal, with no closure hypothesis, is trivial.

Proof route

Let be proper and closed. The ideal-separating pure-state GNS argument in the closed-ideal simplicity criterion gives an irreducible representation that annihilates . It is unitarily equivalent to the faithful inclusion . For , the intertwining equation therefore makes zero. Since is injective, . Thus every proper closed ideal is zero.

Proof steps

  1. If there is nothing to prove. Otherwise use a pure GNS representation with for every .

  2. Choose the unitary from the faithful inclusion to . For , for all .

  3. Injectivity of gives ; injectivity of gives . Nonzeroness of follows from its embedded copy of .

Main citations

Lean source signature (exact)

theorem isSimpleCStarAlgebra_shellFamilyTarget (family : RepresentativeShellFamily) :
    MathlibAnnex.CStarAlgebra.IsSimpleCStarAlgebra (ShellFamilyTarget family)

Here ShellFamilyTarget family is . IsSimpleCStarAlgebra means that is nonzero and every norm-closed two-sided ideal is either zero or the whole algebra. This is exactly the closed-ideal assertion above; no condition on arbitrary nonclosed ideals is added.

Lean realization notes

The proof uses capture for the Hilbert spaces of canonical pure GNS representations, which lie in the source-algebra universe. The stronger universe-polymorphic capture result supplies this case. Faithfulness is essential: uniqueness of an irreducible class without a faithful representation would not justify this argument.

Exact Card identity

Language: en

CARD_CONTENT_COMPLETE

Card UID: lfh:lfh-declaration-card:sha256:2f74196f22042b6e02ddfbd323ee500f1cd0f3bc297f30b91ccaed55116f7c26

Card revision: 1 · SHA-256: 12b80e1f736ab61c746ad43545eeac483af19f4bccd6ea10d04993b56aef591b

Exposition revision: 1 · SHA-256: 005b0ef073045c52c392495d5e4a3ee8cd3df099dfa9b8d3e4a9c7911e96ad05

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Header SHA-256: 11ce02f9ecd62e77a48900b052502494bc3255c31ea40339b246ccee1f615d77

Back to top ↑