Back-and-forth levels via pointwise isolation from lower levels

The motivating application is a limit ordinal λ: there BFEquiv λ is the conjunction of the BFEquiv β for β < λ (BFEquiv.limit), so a depth-λ class is a coherent family of classes at the lower levels, and countably many classes at every lower level do not by themselves bound the number of depth-λ classes — a countable product of countable sets can have the size of the continuum.

A sufficient condition is pointwise isolation: every model is determined, up to depth-λ equivalence, by its class at some lower level β < λ, where β may depend on the model. Then each depth-λ class is pinned by one node of a countable collection of lower-level quotients, so level λ inherits the cardinal bound of the lower levels. The results below assume only this isolation hypothesis and λ < ω₁; they do not assume λ is a limit and never use BFEquiv.limit (at a successor the hypothesis holds trivially with β := λ - 1).

The generic statement is about an arbitrary family of setoids E : I → Setoid X with I countable and a target setoid L (Setoid.IsolatedBy); no uniformity in the isolating index is required, and nothing about a product of the lower levels is used.

Main results

• Setoid.exists_injective_sigma_of_isolatedBy — the L-classes inject into the dependent sum of the E i-classes.
• Setoid.countable_quotient_of_isolatedBy, Setoid.lift_mk_quotient_le_of_isolatedBy — the countable and general cardinal transfers.
• countable_bfEquivSetoid_quotient_of_isolated, mk_bfEquivSetoid_quotient_le_aleph_one_of_isolated — the instances for bfEquivSetoid φ λ, λ < ω₁, from the levels β < λ.

def Setoid.IsolatedBy {X : Type u} {I : Type w} (E : I → Setoid X) (L : Setoid X) : Prop

Pointwise isolation: every point has an index i such that its E i-class determines its L-class. The index may depend on the point.

Equations

• Setoid.IsolatedBy E L = ∀ (x : X), ∃ (i : I), ∀ (y : X), (E i) x y → L x y

theorem Setoid.exists_injective_sigma_of_isolatedBy {X : Type u} {I : Type w} {E : I → Setoid X} {L : Setoid X} (h : IsolatedBy E L) : ∃ (f : Quotient L → (i : I) × Quotient (E i)), Function.Injective f

Under pointwise isolation, the L-classes inject into the dependent sum of the E i-classes: send a class to (an isolating index of a representative, the representative's class there).

theorem Setoid.countable_quotient_of_isolatedBy {X : Type u} {I : Type w} [Countable I] {E : I → Setoid X} {L : Setoid X} [∀ (i : I), Countable (Quotient (E i))] (h : IsolatedBy E L) : Countable (Quotient L)

Countable lower levels and pointwise isolation give a countable limit level.

theorem Setoid.lift_mk_quotient_le_of_isolatedBy {X : Type u} {I : Type w} [Countable I] {E : I → Setoid X} {L : Setoid X} {κ : Cardinal.{max u w}} (hκ : Cardinal.aleph0 ≤ κ) (hE : ∀ (i : I), Cardinal.lift.{w, u} (Cardinal.mk (Quotient (E i))) ≤ κ) (h : IsolatedBy E L) : Cardinal.lift.{w, u} (Cardinal.mk (Quotient L)) ≤ κ

The general cardinal transfer: lower levels of size ≤ κ (for infinite κ, countably many of them) and pointwise isolation give a limit level of size ≤ κ. Stated with the lifts needed when the index type and the carrier live in different universes.

def FirstOrder.Language.BFIsolatedBelow {L : Language} [L.IsRelational] (φ : L.Sentenceω) (lam : Ordinal.{0}) : Prop

Pointwise isolation from lower levels for coded models: every model is determined, up to depth-λ back-and-forth equivalence, by its depth-β class for some β < λ depending on the model. The intended λ is a limit ordinal, but nothing below requires it.

Equations

• FirstOrder.Language.BFIsolatedBelow φ lam = Setoid.IsolatedBy (fun (β : ↑(Set.Iio lam)) => FirstOrder.Language.bfEquivSetoid φ ↑β) (FirstOrder.Language.bfEquivSetoid φ lam)

theorem FirstOrder.Language.countable_bfEquivSetoid_quotient_of_isolated {L : Language} [L.IsRelational] (φ : L.Sentenceω) {lam : Ordinal.{0}} (hlam : lam < Ordinal.omega 1) (hlevel : ∀ (β : ↑(Set.Iio lam)), Countable (Quotient (bfEquivSetoid φ ↑β))) (hiso : BFIsolatedBelow φ lam) : Countable (Quotient (bfEquivSetoid φ lam))

Countable levels below a countable λ, with pointwise isolation, give a countable level λ.

theorem FirstOrder.Language.mk_bfEquivSetoid_quotient_le_aleph_one_of_isolated {L : Language} [L.IsRelational] (φ : L.Sentenceω) {lam : Ordinal.{0}} (hlam : lam < Ordinal.omega 1) (hlevel : ∀ (β : ↑(Set.Iio lam)), Cardinal.mk (Quotient (bfEquivSetoid φ ↑β)) ≤ Cardinal.aleph 1) (hiso : BFIsolatedBelow φ lam) : Cardinal.mk (Quotient (bfEquivSetoid φ lam)) ≤ Cardinal.aleph 1

Levels of size ≤ ℵ₁ below a countable λ, with pointwise isolation, give a level λ of size ≤ ℵ₁.