MATHLIBANNEX / CANONICAL DECLARATION CARD

The shell-generated algebra is not an algebra of all compact operators

MathlibAnnex.CStarAlgebra.CAR.not_isCompactOperatorModel_shellFamilyTarget

theorem

Excludes an injective representation of the infinite-dimensional unital algebra onto all compact operators.

Statement

For the fixed shell-generated algebra below and any complete complex Hilbert space , there is no injective complex-linear star representation whose image is exactly the compact operators on . The map is not assumed to preserve the unit.

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 space may have any dimension and belongs to an arbitrary independent universe. The exact range condition says both that each is compact and that every compact operator on equals some . Inner products in the rank-one formula are linear in the second argument.

Conclusion

Thus is not isomorphic to the C*-algebra of all compact operators on any complete complex Hilbert space , including the zero Hilbert space. No preservation of the identity is imposed on the candidate representation.

Proof route

Assume such a map exists. Injectivity and first force . Since every rank-one operator is in the image, acts as the identity on every vector: apply to a rank-one operator sending a fixed unit vector to the desired vector. Thus . But is compact, forcing to be finite-dimensional. Then and its complex-linear subspace are finite-dimensional, contradicting the infinite dimension of .

Proof steps

  1. The zero Hilbert space admits only the zero operator, so it cannot receive an injective representation of the nonzero algebra .

  2. For , choose a unit vector . The rank-one operator lies in the image for any ; evaluating at gives .

  3. A compact identity operator forces finite dimension. Injectivity of the complex-linear map then transfers finite dimension back to , a contradiction.

Main citations

Lean source signature (exact)

theorem not_isCompactOperatorModel_shellFamilyTarget
    (family : RepresentativeShellFamily)
    {K : Type v} [NormedAddCommGroup K] [InnerProductSpace ℂ K]
    [CompleteSpace K]
    (e : ShellFamilyTarget family →⋆ₙₐ[ℂ] (K →L[ℂ] K)) :
    ¬ IsCompactOperatorModel e

Here ShellFamilyTarget family is , and e is the possibly nonunital star representation into . IsCompactOperatorModel e combines three conditions: injectivity, compactness of every , and surjectivity onto all compact operators. Its negation excludes an injective star representation of whose range is exactly the algebra of all compact operators on .

Lean realization notes

The obstruction uses that is unital and infinite-dimensional, with infinite dimension established in the target-dimension theorem using its injective copy of the completed CAR algebra. It is distinct from results about the intersection of one represented image with the compact operators.

Exact Card identity

Language: en

CARD_CONTENT_COMPLETE

Card UID: lfh:lfh-declaration-card:sha256:613fdafd1f323fb659d8b89d248b1f5902a2cc42585e5fe30392ece18490eeea

Card revision: 1 · SHA-256: 63eb23bc6a8d3e7555fba85b8fa2b3034c6655a355c5a79f27854ee042fbc82b

Exposition revision: 1 · SHA-256: eca1da9d8c8943a3bf1bd549653590a608fec2d3e8df1a4568ca82366332c2a2

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Header SHA-256: 2f51b63ed49da6a9858c2c5c44633ffb35dbc65d72a058ccf36b0f1705919bd3

Back to top ↑