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 .

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.

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

Supporting route explanation

Lean source signature (exact)

theorem hasDensityCharacter_atomicCounterexampleAlgebra :
    HasDensityCharacter AtomicCounterexampleAlgebra Cardinal.continuum
In the source Mathematical meaning
AtomicCounterexampleAlgebra The one fixed CAR shell-generated algebra , equipped with its operator-norm topology.
Cardinal.continuum The continuum cardinal , rather than a linear or Hilbert-space dimension.
HasDensityCharacter AtomicCounterexampleAlgebra Cardinal.continuum The full conclusion has two clauses: there is a norm-dense subset with ; and every norm-dense satisfies . Thus . The separate equality mentioned in the text is not substituted for this minimality assertion.
Dense s; #s In the linked exact definition of HasDensityCharacter, Dense s means norm density of the subset here and #s is its cardinality, not its vector-space dimension.

Further source notes: 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 · Back to Project

Earlier published Card and PDF

Exact content identity

Declaration: MathlibAnnex.CStarAlgebra.CAR.hasDensityCharacter_atomicCounterexampleAlgebra

Accepted content SHA-256: b40286a5ff6686d5c043943f269bb42e40bbe62442dae691b3332697d8177473

Accepted source guide SHA-256: c9883867d594fea0ac7aa0919806e625452543972c701d32bb858d343b9d75a6

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Back to top ↑