MATHLIBANNEX / CANONICAL DECLARATION CARD

Structural properties of one shell-generated C*-algebra

MathlibAnnex.CStarAlgebra.CAR.shellFamilyEndpoint

theorem

Collects the proved properties of a single generated algebra, keeping the shell-family input separate from its consequences.

Statement

For every fixed shell family, form , and as below. Then is nonzero, norm closed and infinite-dimensional, is injective and unital, and is faithful and irreducible. Every nonzero irreducible complex star representation of , even if not initially required to preserve the unit, is unitarily equivalent to . The only norm-closed two-sided ideals of are and , and has no injective star representation whose range is precisely all compact operators on any complex Hilbert space.

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 comparison Hilbert space may be any complete complex Hilbert space in an arbitrary independent universe. No separability or dimension bound on is added. The chosen family, links and algebra do not depend on that comparison universe.

Conclusion

All conclusions concern this same concrete . In the capture assertion, unitary equivalence means there is a surjective complex-linear isometry with for all and . In the compact-operator assertion, the competing map need not be unital and the zero Hilbert space is also covered.

Proof route

The construction of the shell unitaries gives a faithful source map and irreducible inclusion. The unital copy of the infinite-dimensional CAR algebra makes nonzero and infinite-dimensional. The universal capture theorem supplies unitary equivalence for unital irreducible representations; irreducibility forces any nonzero possibly nonunital representation to preserve the unit. Ideal-separating pure GNS representations then yield simplicity. Finally a unital infinite-dimensional algebra cannot be represented injectively onto all compact operators.

Proof steps

  1. Choose the links once, restrict to the generated algebra, and use its faithful root summand. Norm closure is part of the construction of .

  2. If were finite-dimensional, its injective complex-linear source map would make finite-dimensional, contradicting the growing matrix stages.

  3. Apply the unitary-equivalence theorem, the nonunital-to-unital argument, and the closed-ideal consequence. Exclude an isomorphism of this same infinite-dimensional algebra onto all compact operators. These are separate proved results supplying the listed fields.

Main citations

Lean source signature (exact)

theorem shellFamilyEndpoint (family : RepresentativeShellFamily) :
    ShellFamilyEndpoint.{v} family

Here ShellFamilyTarget family is , shellFamilySourceHom family is , and shellFamilyInclusion family is . ShellFamilyEndpoint is the proposition listing the properties in the Statement; the theorem shellFamilyEndpoint proves it. Its exact structure declaration is linked as “Properties of the fixed target” above. The family, and hence , are fixed before the comparison Hilbert space is chosen.

Lean realization notes

The separately linked Lean structure lists these properties; defining that proposition does not prove it. This theorem proves that proposition for every supplied family. The family hypothesis remains explicit. The structural theorem for the homogeneity-based algebra and its faithful representation on a separable Hilbert space specialize this fixed-family result.

Exact Card identity

Language: en

CARD_CONTENT_COMPLETE

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

Card revision: 1 · SHA-256: 963ba28055994c54f1f2a45c157c1d4c74f37952b595c5894c0c051169f78338

Exposition revision: 1 · SHA-256: de7fb04f639023fa54e46122ba7aed2b46a74ac72668314c3322290d884fae3f

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Header SHA-256: 26f34455f56899e7460e8f2200e418326a3bf2d65dc459b8a8e0c90328f1d41c

Back to top ↑