The underlying set of A has size at most the continuum

MathlibAnnex.CStarAlgebra.CAR.cardinalMk_atomicCounterexampleAlgebra_le_continuum

theorem

Obtains a carrier-cardinality bound from a faithful representation on a separable Hilbert space.

Statement

The underlying set of the fixed CAR-based C*-algebra A has cardinality at most 𝔠 = 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. No additional hypotheses are supplied to this theorem. Its proof uses the previously constructed faithful representation on the separable CAR trace-GNS space.

Conclusion

|A| ≤ 𝔠.

Proof route

Apply the cardinality bound for an algebra admitting an injective representation on a separable Hilbert space.

Main citations

• MathlibAnnex.Analysis.CStarAlgebra.Representation.cardinalMk_le_continuum_of_injective

  Exact source attribution.

Lean source declaration (exact)

/-- The existing faithful separable representation bounds the fixed carrier. -/
theorem cardinalMk_atomicCounterexampleAlgebra_le_continuum :
    #AtomicCounterexampleAlgebra ≤ Cardinal.continuum := by
  letI : TopologicalSpace.SeparableSpace SeparableCounterexampleHilbertSpace :=
    separableSpace_separableCounterexampleHilbertSpace
  exact Representation.cardinalMk_le_continuum_of_injective
    separableCounterexampleRepresentation separableCounterexampleRepresentation_injective

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

Lean realization notes

Cardinal.mk here refers to the underlying set, not the density character or a vector-space dimension. No CH premise is used. The lower bound required for equality is supplied separately.