Borel reducibility and smooth equivalence relations

An equivalence relation E on a measurable space X is Borel reducible to an equivalence relation F on Y when some measurable f : X → Y satisfies E x y ↔ F (f x) (f y): the classes of E are then classified by the classes of F, through a Borel map. Borel reducibility is a preorder across all measurable spaces, and it compares the complexity of classification problems.

The simplest relations in this order are the equalities. E is smooth when it is Borel reducible to equality on Cantor space ℕ → Bool, that is, when a Borel map into Cantor space classifies its classes. The main characterization is that E is smooth exactly when countably many E-invariant measurable sets separate its classes, which is to say that the quotient Quotient E, with Mathlib's quotient σ-algebra, is countably separated. A Borel reduction descends to a measurable injection of quotients, and Mathlib's measurable injection of a countably separated space into Cantor space gives the converse.

Further facts:

• a reduction to a relation with Borel graph pulls the graph back, so a smooth relation is Borel;
• a reduction induces an injection of quotients, so F has at least as many classes as E;
• equality on a standard Borel space X reduces to equality on a standard Borel space Y iff #X ≤ #Y. If X is countable, any injection works, as a countable standard Borel space is discrete; otherwise both spaces are uncountable and the Borel isomorphism theorem identifies them. In particular, for uncountable standard Borel Y, smoothness is reducibility to equality on Y;
• a relation with countably many classes, each measurable, is smooth, and it is bireducible with equality on its quotient, whose σ-algebra is then discrete. Among relations with measurable classes, reducibility to a countable quotient is exactly comparison of the numbers of classes. The countable normal forms are equality on some Fin n (including Fin 0 for the empty space) or on ℕ; no standard Borel hypothesis is needed;
• a Cantor antichain for E is a reduction of equality on Cantor space to E.

Main definitions

• Setoid.BorelReducible E F: a measurable map f with E x y ↔ F (f x) (f y).
• Setoid.BorelBireducible E F: each of E and F is Borel reducible to the other.
• Setoid.IsSmooth E: E is Borel reducible to equality on ℕ → Bool.

Main results

• Setoid.BorelReducible.trans, Setoid.BorelBireducible.symm, Setoid.BorelBireducible.trans: the preorder and its equivalence.
• Setoid.BorelReducible.exists_measurable_injective_quotient, Setoid.BorelReducible.lift_mk_quotient_le: the induced injection of quotients.
• Setoid.BorelReducible.measurableSet_setOf, Setoid.IsSmooth.measurableSet_setOf: reductions pull back Borel graphs, and smooth relations are Borel.
• Setoid.borelReducible_bot_bot_iff_lift_mk_le: reductions between equalities on standard Borel spaces.
• Setoid.isSmooth_iff_countablySeparated: smoothness is countable separation of the quotient.
• Setoid.isSmooth_iff_borelReducible_bot: smoothness is reducibility to equality on any uncountable standard Borel space.
• Setoid.isSmooth_of_countable_quotient, Setoid.borelBireducible_bot_quotient: relations with countably many measurable classes.
• Setoid.borelReducible_iff_lift_mk_quotient_le_of_countable, Setoid.borelBireducible_iff_lift_mk_quotient_eq_of_countable: comparison of countable quotients.
• Setoid.borelBireducible_bot_iff_nonempty_equiv_of_countable: equality on a countable discrete space is a normal form precisely when that space bijects with the quotient.
• Setoid.borelBireducible_bot_nat_iff, Setoid.exists_borelBireducible_bot_fin_or_nat: the countably infinite and finite-or-countably-infinite normal forms, using Setoid.borelBireducible_bot_quotient.
• Setoid.HasCantorAntichainOn.borelReducible_bot: a Cantor antichain reduces equality on Cantor space.

References

• S. Gao, Invariant Descriptive Set Theory, Chapman & Hall/CRC, 2009, Chapter 5 (Borel reducibility and smooth equivalence relations).
• A. S. Kechris, Classical Descriptive Set Theory, Graduate Texts in Mathematics 156, Springer, 1995, Theorem 15.6 (the Borel isomorphism theorem).

Borel reducibility

def Setoid.BorelReducible {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] (E : Setoid X) (F : Setoid Y) : Prop

E is Borel reducible to F: some measurable map f : X → Y satisfies E x y ↔ F (f x) (f y) for all x and y.

theorem Setoid.borelReducible_iff {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {E : Setoid X} {F : Setoid Y} : E.BorelReducible F ↔ ∃ (f : X → Y), Measurable f ∧ ∀ (x y : X), E x y ↔ F (f x) (f y)

theorem Setoid.borelReducible_iff_exists_eq_comap {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {E : Setoid X} {F : Setoid Y} : E.BorelReducible F ↔ ∃ (f : X → Y), Measurable f ∧ E = comap f F

E is Borel reducible to F iff it is the pullback F.comap f along a measurable map.

theorem Setoid.borelReducible_comap {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {f : X → Y} (hf : Measurable f) (F : Setoid Y) : (comap f F).BorelReducible F

The pullback of F along a measurable map is Borel reducible to F.

theorem Setoid.BorelReducible.refl {X : Type u} [MeasurableSpace X] (E : Setoid X) : E.BorelReducible E

theorem Setoid.BorelReducible.rfl {X : Type u} [MeasurableSpace X] {E : Setoid X} : E.BorelReducible E

theorem Setoid.BorelReducible.trans {X : Type u} {Y : Type v} {Z : Type w} [MeasurableSpace X] [MeasurableSpace Y] [MeasurableSpace Z] {E : Setoid X} {F : Setoid Y} {G : Setoid Z} (h₁ : E.BorelReducible F) (h₂ : F.BorelReducible G) : E.BorelReducible G

theorem Setoid.BorelReducible.exists_measurable_injective_quotient {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {E : Setoid X} {F : Setoid Y} (h : E.BorelReducible F) : ∃ (g : Quotient E → Quotient F), Measurable g ∧ Function.Injective g

A Borel reduction of E to F descends to a measurable injection Quotient E → Quotient F, for Mathlib's quotient σ-algebras.

theorem Setoid.BorelReducible.lift_mk_quotient_le {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {E : Setoid X} {F : Setoid Y} (h : E.BorelReducible F) : Cardinal.lift.{v, u} (Cardinal.mk (Quotient E)) ≤ Cardinal.lift.{u, v} (Cardinal.mk (Quotient F))

If E is Borel reducible to F, then F has at least as many classes as E.

theorem Setoid.BorelReducible.mk_quotient_le {X : Type u} [MeasurableSpace X] {E : Setoid X} {Y : Type u} [MeasurableSpace Y] {F : Setoid Y} (h : E.BorelReducible F) : Cardinal.mk (Quotient E) ≤ Cardinal.mk (Quotient F)

If E is Borel reducible to F, on spaces in the same universe, then F has at least as many classes as E.

theorem Setoid.BorelReducible.measurableSet_setOf {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {E : Setoid X} {F : Setoid Y} (h : E.BorelReducible F) (hF : MeasurableSet {p : Y × Y | F p.1 p.2}) : MeasurableSet {p : X × X | E p.1 p.2}

A Borel reduction pulls a Borel graph back: if E is Borel reducible to F and the graph of F is measurable, so is the graph of E.

Borel bireducibility

def Setoid.BorelBireducible {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] (E : Setoid X) (F : Setoid Y) : Prop

E and F are Borel bireducible: each is Borel reducible to the other.

theorem Setoid.borelBireducible_iff {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {E : Setoid X} {F : Setoid Y} : E.BorelBireducible F ↔ E.BorelReducible F ∧ F.BorelReducible E

theorem Setoid.BorelBireducible.refl {X : Type u} [MeasurableSpace X] (E : Setoid X) : E.BorelBireducible E

theorem Setoid.BorelBireducible.rfl {X : Type u} [MeasurableSpace X] {E : Setoid X} : E.BorelBireducible E

theorem Setoid.BorelBireducible.symm {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {E : Setoid X} {F : Setoid Y} (h : E.BorelBireducible F) : F.BorelBireducible E

theorem Setoid.borelBireducible_comm {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {E : Setoid X} {F : Setoid Y} : E.BorelBireducible F ↔ F.BorelBireducible E

theorem Setoid.BorelBireducible.trans {X : Type u} {Y : Type v} {Z : Type w} [MeasurableSpace X] [MeasurableSpace Y] [MeasurableSpace Z] {E : Setoid X} {F : Setoid Y} {G : Setoid Z} (h₁ : E.BorelBireducible F) (h₂ : F.BorelBireducible G) : E.BorelBireducible G

theorem Setoid.BorelBireducible.lift_mk_quotient_eq {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {E : Setoid X} {F : Setoid Y} (h : E.BorelBireducible F) : Cardinal.lift.{v, u} (Cardinal.mk (Quotient E)) = Cardinal.lift.{u, v} (Cardinal.mk (Quotient F))

Borel bireducible relations have equally many classes, allowing different universes.

Reductions between equalities

theorem Setoid.borelReducible_bot_bot_iff {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] : ⊥.BorelReducible ⊥ ↔ ∃ (f : X → Y), Measurable f ∧ Function.Injective f

Equality on X reduces to equality on Y iff there is a measurable injection X → Y.

theorem Setoid.borelReducible_bot_bot_iff_lift_mk_le {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] [StandardBorelSpace X] [StandardBorelSpace Y] : ⊥.BorelReducible ⊥ ↔ Cardinal.lift.{v, u} (Cardinal.mk X) ≤ Cardinal.lift.{u, v} (Cardinal.mk Y)

Reductions between equalities on standard Borel spaces. Equality on X reduces to equality on Y iff X has at most as many points as Y. A countable standard Borel space is discrete, so any injection is measurable; uncountable standard Borel spaces are Borel isomorphic.

Smooth equivalence relations

def Setoid.IsSmooth {X : Type u} [MeasurableSpace X] (E : Setoid X) : Prop

E is smooth: it is Borel reducible to equality on Cantor space ℕ → Bool.

theorem Setoid.isSmooth_def {X : Type u} [MeasurableSpace X] {E : Setoid X} : E.IsSmooth ↔ E.BorelReducible ⊥

theorem Setoid.isSmooth_iff {X : Type u} [MeasurableSpace X] {E : Setoid X} : E.IsSmooth ↔ ∃ (f : X → ℕ → Bool), Measurable f ∧ ∀ (x y : X), E x y ↔ f x = f y

E is smooth iff a measurable map into Cantor space has the classes of E as its fibres.

theorem Setoid.BorelReducible.isSmooth {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {E : Setoid X} {F : Setoid Y} (h : E.BorelReducible F) (hF : F.IsSmooth) : E.IsSmooth

A relation Borel reducible to a smooth relation is smooth.

theorem Setoid.IsSmooth.measurableSet_setOf {X : Type u} [MeasurableSpace X] {E : Setoid X} (h : E.IsSmooth) : MeasurableSet {p : X × X | E p.1 p.2}

A smooth equivalence relation is Borel: its graph is the preimage of the diagonal of Cantor space.

theorem Setoid.isSmooth_iff_countablySeparated {X : Type u} [MeasurableSpace X] {E : Setoid X} : E.IsSmooth ↔ MeasurableSpace.CountablySeparated (Quotient E)

Smoothness is countable separation. E is smooth iff the quotient Quotient E, with Mathlib's quotient σ-algebra, is countably separated: countably many E-invariant measurable sets separate the classes of E.

theorem Setoid.isSmooth_bot_iff {X : Type u} [MeasurableSpace X] : ⊥.IsSmooth ↔ MeasurableSpace.CountablySeparated X

Equality on X is smooth iff X is countably separated.

theorem Setoid.isSmooth_iff_borelReducible_bot {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {E : Setoid X} [StandardBorelSpace Y] (hY : ¬Countable Y) : E.IsSmooth ↔ E.BorelReducible ⊥

Smoothness through any uncountable standard Borel space. For an uncountable standard Borel space Y, E is smooth iff it is Borel reducible to equality on Y: equality on Y and equality on Cantor space are Borel isomorphic.

Countably many classes

theorem Setoid.isSmooth_of_countable_quotient {X : Type u} [MeasurableSpace X] {E : Setoid X} [Countable (Quotient E)] (hE : ∀ (x : X), MeasurableSet {y : X | E x y}) : E.IsSmooth

Countably many measurable classes give a smooth relation. If E has countably many classes, each measurable, then E is smooth.

theorem Setoid.borelBireducible_bot_quotient {X : Type u} [MeasurableSpace X] {E : Setoid X} [Countable (Quotient E)] (hE : ∀ (x : X), MeasurableSet {y : X | E x y}) : E.BorelBireducible ⊥

If E has countably many classes, each measurable, then E is Borel bireducible with equality on its quotient: the quotient map is a reduction one way, and a choice of representatives, measurable because the quotient σ-algebra is discrete, is a reduction the other way.

theorem Setoid.borelReducible_iff_lift_mk_quotient_le_of_countable {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {E : Setoid X} {F : Setoid Y} [Countable (Quotient F)] (hE : ∀ (x : X), MeasurableSet {y : X | E x y}) : E.BorelReducible F ↔ Cardinal.lift.{v, u} (Cardinal.mk (Quotient E)) ≤ Cardinal.lift.{u, v} (Cardinal.mk (Quotient F))

Borel reducibility to a relation with countably many classes is exactly comparison of the cardinalities of the quotients, provided all classes of the source relation are measurable.

theorem Setoid.borelBireducible_iff_lift_mk_quotient_eq_of_countable {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {E : Setoid X} {F : Setoid Y} [Countable (Quotient F)] (hE : ∀ (x : X), MeasurableSet {y : X | E x y}) (hF : ∀ (x : Y), MeasurableSet {y : Y | F x y}) : E.BorelBireducible F ↔ Cardinal.lift.{v, u} (Cardinal.mk (Quotient E)) = Cardinal.lift.{u, v} (Cardinal.mk (Quotient F))

Two relations with measurable classes, one with countably many classes, are Borel bireducible exactly when their quotients have the same cardinality.

theorem Setoid.borelBireducible_bot_iff_nonempty_equiv_of_countable {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {E : Setoid X} [Countable Y] [MeasurableSingletonClass Y] (hE : ∀ (x : X), MeasurableSet {y : X | E x y}) : E.BorelBireducible ⊥ ↔ Nonempty (Quotient E ≃ Y)

A relation with measurable classes is Borel bireducible with equality on a countable discrete measurable space precisely when its quotient bijects with that space. No countability hypothesis on the quotient is needed.

theorem Setoid.borelBireducible_bot_nat_iff {X : Type u} [MeasurableSpace X] {E : Setoid X} (hE : ∀ (x : X), MeasurableSet {y : X | E x y}) : E.BorelBireducible ⊥ ↔ Countable (Quotient E) ∧ Infinite (Quotient E)

Equality on the natural numbers is the normal form for a relation with measurable classes exactly when the quotient is countably infinite.

theorem Setoid.exists_borelBireducible_bot_fin_or_nat {X : Type u} [MeasurableSpace X] {E : Setoid X} [Countable (Quotient E)] (hE : ∀ (x : X), MeasurableSet {y : X | E x y}) : (∃ (n : ℕ), E.BorelBireducible ⊥) ∨ E.BorelBireducible ⊥

A relation with countably many measurable classes is Borel bireducible with equality on some Fin n, or with equality on ℕ.

Cantor antichains

theorem Setoid.HasCantorAntichainOn.borelReducible_bot {X : Type u} [MeasurableSpace X] {E : Setoid X} [TopologicalSpace X] [BorelSpace X] {A : Set X} (h : E.HasCantorAntichainOn A) : ⊥.BorelReducible E

A Cantor antichain reduces equality on Cantor space. If E has a Cantor antichain on some set, the antichain itself is a Borel reduction of equality on ℕ → Bool to E.