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.

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.

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.

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

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

Earlier published Card and PDF