The norm density of A is exactly the continuum

MathlibAnnex.CStarAlgebra.CAR.hasDensityCharacter_atomicCounterexampleAlgebra

theorem

Proves both existence of a dense set of the stated size and minimality of that size.

Statement

The fixed CAR-based C*-algebra A has norm density character exactly 𝔠 = 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. Density is computed in the norm topology on A; no CH assumption is made.

Conclusion

There exists a norm-dense subset D ⊆ A with |D| = 𝔠, and every norm-dense subset E ⊆ A satisfies 𝔠 ≤ |E|. Thus dens(A) = 𝔠.

Proof route

Combine the carrier-cardinality upper bound with the lower bound for every norm-dense subset.

Main citations

• MathlibAnnex.CStarAlgebra.CAR.continuum_le_cardinalMk_dense_atomicCounterexampleAlgebra

  Exact source attribution.

• MathlibAnnex.Topology.HasDensityCharacter.of_cardinalMk_le_of_forall_dense

  Exact source attribution.

Lean source declaration (exact)

/-- The exact norm density of the same fixed algebra is continuum. -/
theorem hasDensityCharacter_atomicCounterexampleAlgebra :
    HasDensityCharacter AtomicCounterexampleAlgebra Cardinal.continuum :=
  HasDensityCharacter.of_cardinalMk_le_of_forall_dense
    cardinalMk_atomicCounterexampleAlgebra_le_continuum
    continuum_le_cardinalMk_dense_atomicCounterexampleAlgebra

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

Lean realization notes

HasDensityCharacter contains an attained dense witness and a universal lower bound. This is not a statement about the strong-operator topology on a represented copy of A or an algebraic dimension.