Isolation of an equivalence relation by a family of equivalence relations

An equivalence relation R on X is isolated by a family E : I → Setoid X when every point x has an index i, depending on x, such that every y that is E i-equivalent to x is R-equivalent to x. Then each R-class is pinned by one class of one E i, so the R-classes inject into the dependent sum of the E i-classes. Over a countable index type, countably many E i-classes each give countably many R-classes, and more generally the R-classes are bounded by any infinite bound on both the index type and the E i-classes.

Isolation is one-sided: the E i-class of x decides R-equivalence with x, for the index chosen for x.

Isolation is an assumption, not a consequence of the sizes of the quotients: on Cantor space the relations "agreeing on the first n coordinates" each have finitely many classes, while their intersection, equality, has continuum many classes.

Main definitions

• Setoid.IsolatedBy R E: R is isolated by the family E.

Main results

• Setoid.IsolatedBy.exists_injective_sigma: the R-classes inject into the dependent sum of the E i-classes.
• Setoid.IsolatedBy.countable_quotient: countably many relations with countable quotients give R a countable quotient.
• Setoid.IsolatedBy.lift_mk_quotient_le: the general cardinal transfer: at most κ relations with at most κ classes each give at most κ classes, for an infinite κ.

References

• Adapted from Setoid.IsolatedBy and its transfer theorems in cameronfreer/infinitary-logic at commit 518a366cba97b1ae8c4dc64a297a396939bc3e0b, InfinitaryLogic/ModelTheory/BFLimitIsolation.lean; only the generic part about setoids is taken, without back-and-forth levels.
• Divergences from that source: the target relation is the first argument, so that isolation is written R.IsolatedBy E, and the transfer theorems are stated on the isolation hypothesis; the cardinal transfer uses Mathlib's bound on sums by suprema.

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

R is isolated by the family E: every point x has an index i such that every point E i-equivalent to x is R-equivalent to x. The index may depend on the point.

theorem Setoid.isolatedBy_iff {X : Type u} {I : Type v} {R : Setoid X} {E : I → Setoid X} : R.IsolatedBy E ↔ ∀ (x : X), ∃ (i : I), ∀ (y : X), (E i) x y → R x y

Unfolding lemma for Setoid.IsolatedBy.

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

The classes inject into the dependent sum. Send an R-class to an isolating index of a representative, together with the class of that representative there.

theorem Setoid.IsolatedBy.countable_quotient {X : Type u} {I : Type v} {R : Setoid X} {E : I → Setoid X} [Countable I] [∀ (i : I), Countable (Quotient (E i))] (h : R.IsolatedBy E) : Countable (Quotient R)

Countable transfer. If R is isolated by countably many relations with countable quotients, then R has countably many classes.

theorem Setoid.IsolatedBy.lift_mk_quotient_le {X : Type u} {I : Type v} {R : Setoid X} {E : I → Setoid X} {κ : Cardinal.{max u v}} (hκ : Cardinal.aleph0 ≤ κ) (hI : Cardinal.lift.{u, v} (Cardinal.mk I) ≤ κ) (hE : ∀ (i : I), Cardinal.lift.{v, u} (Cardinal.mk (Quotient (E i))) ≤ κ) (h : R.IsolatedBy E) : Cardinal.lift.{v, u} (Cardinal.mk (Quotient R)) ≤ κ

Cardinal transfer. If R is isolated by at most κ relations, each with at most κ classes for an infinite cardinal κ, then R has at most κ classes.