Ranks into the countable ordinals

A map r : X → Ordinal whose values are all countable ordinals (below ω₁) controls the size of X and the countability of its subsets as soon as its fibres are small:

• if every fibre has at most c elements, then X has at most ℵ₁ * c elements; with countable fibres, X has at most ℵ₁ elements, and exactly ℵ₁ when it is uncountable;
• with countable fibres, a subset of X is countable exactly when r is bounded below ω₁ on it.

These are the cardinal estimates behind stratifying a class of countable structures by a Scott-rank-like invariant: there are ℵ₁ strata, each stratum is small, and a family of structures is countable precisely when its ranks are bounded below ω₁. The ordinals may live in any universe, independent of the universe of X.

Main results

• TauCeti.mk_le_aleph_one_mul_of_mk_preimage_le: fibres of size at most c give #X ≤ ℵ₁ * c.
• TauCeti.mk_le_aleph_one_of_countable_preimage: countable fibres give #X ≤ ℵ₁.
• TauCeti.mk_eq_aleph_one_of_countable_preimage: if moreover X is uncountable, #X = ℵ₁.
• Set.Countable.exists_lt_omega_one_forall_lt: on a countable set, a rank below ω₁ is bounded below ω₁.
• TauCeti.countable_preimage_Iio_of_lt_omega_one: below a countable ordinal, countably many countable fibres have a countable union.
• TauCeti.countable_iff_exists_lt_omega_one_forall_lt: with countable fibres, a set is countable iff the rank is bounded below ω₁ on it.
• TauCeti.exists_surjective_Iio_omega_one: an uncountable type maps onto the countable ordinals, so a rank below ω₁ can be unbounded on it.

References

The countable-fibre statements, for ranks into Ordinal.{0}, are also proved in InfinitaryLogic/OrdinalCountability.lean of Cameron Freer's Lean formalization cameronfreer/infinitary-logic (checkpoint 518a366, Apache-2.0).

theorem Set.Countable.exists_lt_omega_one_forall_lt {X : Type u} {r : X → Ordinal.{w}} {s : Set X} (hs : s.Countable) (hr : ∀ x ∈ s, r x < Ordinal.omega 1) : ∃ β < Ordinal.omega 1, ∀ x ∈ s, r x < β

A countable set of countable ordinals is bounded below ω₁. If r takes values below ω₁ on a countable set s, some single countable ordinal strictly bounds r on s.

theorem TauCeti.mk_le_aleph_one_mul_of_mk_preimage_le {X : Type u} {r : X → Ordinal.{w}} {c : Cardinal.{u}} (hr : ∀ (x : X), r x < Ordinal.omega 1) (hc : ∀ o < Ordinal.omega 1, Cardinal.mk ↑(r ⁻¹' {o}) ≤ c) : Cardinal.mk X ≤ Cardinal.aleph 1 * c

Bounding a set by a rank below ω₁. If r takes values below ω₁ and every fibre of r over a countable ordinal has at most c elements, then X has at most ℵ₁ * c elements.

theorem TauCeti.mk_le_aleph_one_of_countable_preimage {X : Type u} {r : X → Ordinal.{w}} (hr : ∀ (x : X), r x < Ordinal.omega 1) (hfib : ∀ o < Ordinal.omega 1, (r ⁻¹' {o}).Countable) : Cardinal.mk X ≤ Cardinal.aleph 1

Countable fibres over the countable ordinals bound a set by ℵ₁. If r takes values below ω₁ and each of its fibres over a countable ordinal is countable, then #X ≤ ℵ₁.

theorem TauCeti.mk_eq_aleph_one_of_countable_preimage {X : Type u} {r : X → Ordinal.{w}} [Uncountable X] (hr : ∀ (x : X), r x < Ordinal.omega 1) (hfib : ∀ o < Ordinal.omega 1, (r ⁻¹' {o}).Countable) : Cardinal.mk X = Cardinal.aleph 1

An uncountable set with a rank below ω₁ and countable fibres has exactly ℵ₁ elements.

theorem TauCeti.countable_preimage_Iio_of_lt_omega_one {X : Type u} {r : X → Ordinal.{w}} {β : Ordinal.{w}} (hβ : β < Ordinal.omega 1) (hfib : ∀ o < β, (r ⁻¹' {o}).Countable) : (r ⁻¹' Set.Iio β).Countable

Countably many countable fibres. If the fibres of r over the ordinals below a countable ordinal β are countable, then so is the set of points of rank below β.

theorem TauCeti.countable_iff_exists_lt_omega_one_forall_lt {X : Type u} {r : X → Ordinal.{w}} {s : Set X} (hr : ∀ x ∈ s, r x < Ordinal.omega 1) (hfib : ∀ o < Ordinal.omega 1, (r ⁻¹' {o}).Countable) : s.Countable ↔ ∃ β < Ordinal.omega 1, ∀ x ∈ s, r x < β

Countable means bounded below ω₁. For a rank r below ω₁ on s whose fibres over the countable ordinals are countable, s is countable exactly when r is bounded on s by a countable ordinal.

theorem TauCeti.exists_surjective_Iio_omega_one {X : Type u} [Uncountable X] : ∃ (f : X → ↑(Set.Iio (Ordinal.omega 1))), Function.Surjective f

An uncountable type maps onto the countable ordinals. Some rank on an uncountable type takes every value below ω₁, in any universe of ordinals.