MATHLIBANNEX / CANONICAL DECLARATION CARD

Exact norm density of the fixed atomic algebra

MathlibAnnex.CStarAlgebra.CAR.hasDensityCharacter_atomicCounterexampleAlgebra

theorem

Combines a cardinality bound from a faithful representation on a separable Hilbert space with a lower bound for every norm-dense subset.

Statement

Let be the completed CAR algebra and the algebra generated by the selected direct sum of pure-state GNS representations indexed by their unitary-equivalence classes and the unitaries from the fixed homogeneity and shell construction. Write for the embedding . Write . The norm-density character of is exactly : there is a norm-dense subset with , and every norm-dense subset satisfies The density character is the least cardinality of a norm-dense subset.

Assumptions

The fixed algebra is infinite dimensional, has exactly one unitary-equivalence class of nonzero irreducible representations, and has a faithful representation on the separable space . These are established properties of this , not additional hypotheses on an arbitrary algebra.

Conclusion

Thus . Separately, the underlying set also has . In particular is not norm separable, although it is faithfully represented on .

Proof route

The faithful representation on gives an upper bound for . The cited density theorem for an infinite-dimensional unital C*-algebra with a unique irreducible representation class gives a lower bound for every dense subset. Applying it also to itself proves that this bound is attained.

Proof steps

  1. Injectivity of and separability of give This is the cited cardinality bound for an algebra faithfully represented on a separable Hilbert space.

  2. Let be the inclusion representation and let be norm dense. The cited lower-bound theorem applies to the irreducible inclusion , the fact that every nonzero irreducible unital representation is equivalent to it, and infinite dimensionality of . It gives . Its argument is by contradiction: would give a dense set of size less than in an irreducible representation space, and the finite-dimensionality theorem at that density would force to be finite dimensional.

  3. Taking gives , hence . The choice then attains the lower bound, proving the exact density statement.

Main citations

Lean source signature (exact)

theorem hasDensityCharacter_atomicCounterexampleAlgebra :
    HasDensityCharacter AtomicCounterexampleAlgebra Cardinal.continuum

HasDensityCharacter AtomicCounterexampleAlgebra Cardinal.continuum means both existence of a dense subset of size and minimality among all dense subsets. In the linked proof, the first supplier bounds #AtomicCounterexampleAlgebra; the second bounds #s for each dense set s. The # notation is cardinality, not dimension.

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

Lean realization notes

The dense-set lower bound is a statement about every norm-dense subset, not merely about the whole carrier. Neither cardinality is a Hamel dimension or a Hilbert-space dimension.

Exact Card identity

Language: en

CARD_CONTENT_COMPLETE

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

Card revision: 2 · SHA-256: bbaa38f0690d7b0ca134e7875ae37f1e48d6f2cd8dc0d5b1d6b4c3701fa214c4

Exposition revision: 3 · SHA-256: 971e28fa2f885c071331a719260720f3987fc339922a7783cd9b38fbd00a9a40

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Header SHA-256: 46c9526d98725ff67438db0b8721a2be0a2a154d3876b9a9b17b9b773f3b7cc7

Back to top ↑