Every norm-dense subset of A has size at least the continuum

MathlibAnnex.CStarAlgebra.CAR.continuum_le_cardinalMk_dense_atomicCounterexampleAlgebra

theorem

Gives a lower bound for every dense subset, not merely for a selected generating set.

Statement

Every norm-dense subset D of the fixed CAR-based C*-algebra A has cardinality at least 𝔠 = 2^ℵ₀.

Assumptions

Let A ⊆ B(Hₐₜ) be the fixed unital C*-algebra obtained by adjoining the chosen shell-link unitaries to the atomic representation of the CAR algebra C, and then taking the norm-closed unital *-algebra they generate. Let D ⊆ A and assume that D is dense in the norm topology of A.

Conclusion

𝔠 ≤ |D|. In particular, A has no countable norm-dense subset.

Proof route

Apply the proved density obstruction for an infinite-dimensional algebra with one irreducible representation class to the atomic inclusion of A.

Main citations

• MathlibAnnex.CStarAlgebra.CAR.not_finiteDimensional_shellFamilyTarget

  Exact source attribution.

• MathlibAnnex.Analysis.CStarAlgebra.Representation.continuum_le_cardinalMk_dense_algebra_of_singleton_of_not_finiteDimensional

  Exact source attribution.

Lean source declaration (exact)

/-- No norm-dense subset of the fixed algebra is smaller than the continuum. -/
theorem continuum_le_cardinalMk_dense_atomicCounterexampleAlgebra
    (s : Set AtomicCounterexampleAlgebra) (hs : Dense s) :
    Cardinal.continuum ≤ #s :=
  Representation.continuum_le_cardinalMk_dense_algebra_of_singleton_of_not_finiteDimensional
    (shellFamilyInclusion homogeneityShellFamily)
    (isUniqueIrreducibleModel_shellFamilyInclusion.{0} homogeneityShellFamily).2
    (not_finiteDimensional_shellFamilyTarget homogeneityShellFamily) s hs

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

Lean realization notes

The exact statement quantifies over s : Set A and takes hs : Dense s. The conclusion is Cardinal.continuum ≤ #s, with #s the cardinality of the subtype. This is a norm-topology statement, not a weak-operator or strong-operator density statement. Faithful representability on a separable Hilbert space does not assert norm separability of A.