The underlying set of A has cardinality continuum

MathlibAnnex.CStarAlgebra.CAR.cardinalMk_atomicCounterexampleAlgebra

theorem

Identifies the exact cardinality of the same fixed algebra.

Statement

The underlying set of the fixed CAR-based C*-algebra A has cardinality 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. This is an unconditional theorem about that fixed construction, with no CH assumption.

Conclusion

|A| = 𝔠.

Proof route

Combine the upper bound from the faithful separable representation with the dense-set lower bound applied to the whole space A.

Main citations

• MathlibAnnex.CStarAlgebra.CAR.cardinalMk_atomicCounterexampleAlgebra_le_continuum

  Exact source attribution.

• MathlibAnnex.CStarAlgebra.CAR.continuum_le_cardinalMk_dense_atomicCounterexampleAlgebra

  Exact source attribution.

Lean source declaration (exact)

/-- The cardinality of the underlying set of the fixed algebra is continuum. -/
theorem cardinalMk_atomicCounterexampleAlgebra :
    #AtomicCounterexampleAlgebra = Cardinal.continuum := by
  apply le_antisymm cardinalMk_atomicCounterexampleAlgebra_le_continuum
  simpa using continuum_le_cardinalMk_dense_atomicCounterexampleAlgebra Set.univ dense_univ

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

Lean realization notes

This declaration concerns carrier cardinality. The exact norm-density theorem for A is a separate result; neither is a statement about Hamel dimension.