Silver-Burgess Dichotomy for Borel Equivalence Relations

This file proves the Silver-Burgess dichotomy for closed equivalence relations on Polish spaces and derives SilverBurgessDichotomy for standard Borel spaces, modulo one sorry in the Borel-to-closed reduction (borel_to_closed_reduction in GandyHarrington.lean).

Main Results

• Perfect.mk_eq_continuum: Nonempty perfect subset of Polish space has cardinality 2^ℵ₀.
• continuum_classes_of_perfect_transversal: Perfect antichain → continuum classes.
• splitting_lemma_closed: Closed equiv relation with uncountably many classes splits into disjoint closed pieces, each uncountable, cross-inequivalent.
• silver_core_closed: Silver's theorem for closed equivalence relations on Polish spaces.
• silver_core_polish: Silver's theorem for Borel equivalence relations (depends on borel_to_closed_reduction in GandyHarrington.lean, sorry: Gandy-Harrington topology not available in Mathlib).
• silverBurgessDichotomy: The Silver-Burgess dichotomy (depends on silver_core_polish).

Perfect set cardinality

theorem Perfect.mk_eq_continuum {α : Type u} [MetricSpace α] [CompleteSpace α] [SecondCountableTopology α] {C : Set α} (hperf : Perfect C) (hne : C.Nonempty) : Cardinal.mk ↑C = Cardinal.continuum

A nonempty perfect subset of a Polish space has cardinality = continuum. Lower bound via Perfect.exists_nat_bool_injection; upper bound via second-countability of Polish spaces.

Perfect transversal → continuum classes

theorem continuum_classes_of_perfect_transversal {α : Type u} [MetricSpace α] [CompleteSpace α] [SecondCountableTopology α] (r : Setoid α) {C : Set α} (hperf : Perfect C) (hne : C.Nonempty) (hinequiv : ∀ x ∈ C, ∀ y ∈ C, r x y → x = y) : Cardinal.continuum ≤ Cardinal.mk (Quotient r)

If an equivalence relation on a Polish space has a perfect set of pairwise inequivalent elements, it has at least continuum classes.

theorem eq_continuum_classes_of_perfect_transversal {α : Type u} [MetricSpace α] [CompleteSpace α] [SecondCountableTopology α] (r : Setoid α) {C : Set α} (hperf : Perfect C) (hne : C.Nonempty) (hinequiv : ∀ x ∈ C, ∀ y ∈ C, r x y → x = y) (hle : Cardinal.mk α ≤ Cardinal.continuum) : Cardinal.mk (Quotient r) = Cardinal.continuum

If an equivalence relation on a Polish space has a perfect set of pairwise inequivalent elements, it has exactly continuum classes (assuming the ambient space has cardinality ≤ continuum).

Polish space cardinality upper bound

theorem mk_le_continuum_of_polish {α : Type u} [MetricSpace α] [CompleteSpace α] [SecondCountableTopology α] [Nonempty α] : Cardinal.mk α ≤ Cardinal.continuum

A Polish space has cardinality ≤ continuum.

theorem mk_quotient_le_continuum_of_polish {α : Type u} [MetricSpace α] [CompleteSpace α] [SecondCountableTopology α] [Nonempty α] (r : Setoid α) : Cardinal.mk (Quotient r) ≤ Cardinal.continuum

The quotient of a Polish space has cardinality ≤ continuum.

Splitting lemma for closed equivalence relations

def IsClassCondensationPt {α : Type u_1} (r : Setoid α) [TopologicalSpace α] (U : Set α) (x : α) : Prop

A condensation point for E-classes in U: every open neighborhood meets uncountably many E-classes.

Equations

• IsClassCondensationPt r U x = (x ∈ U ∧ ∀ (V : Set α), IsOpen V → x ∈ V → ¬{q : Quotient r | ∃ y ∈ U ∩ V, ⟦y⟧ = q}.Countable)

theorem exists_classCondensationPt_of_uncountable {α : Type u} [TopologicalSpace α] [SecondCountableTopology α] (r : Setoid α) {U : Set α} (hunc : ¬{q : Quotient r | ∃ y ∈ U, ⟦y⟧ = q}.Countable) : ∃ (x : α), IsClassCondensationPt r U x

In a second-countable space, if U meets uncountably many E-classes, there exist condensation points in uncountably many classes.

theorem uncountable_classCondensationPt_classes {α : Type u} [TopologicalSpace α] [SecondCountableTopology α] (r : Setoid α) {U : Set α} (hunc : ¬{q : Quotient r | ∃ y ∈ U, ⟦y⟧ = q}.Countable) : ¬{q : Quotient r | ∃ (x : α), IsClassCondensationPt r U x ∧ ⟦x⟧ = q}.Countable

In a second-countable space, if U meets uncountably many E-classes, then uncountably many classes have a condensation point representative in U.

theorem splitting_lemma_closed {α : Type u} [MetricSpace α] [SecondCountableTopology α] (r : Setoid α) (hclosed_r : IsClosed {p : α × α | r p.1 p.2}) {U : Set α} (hU : IsClosed U) (hunc : ¬{q : Quotient r | ∃ y ∈ U, ⟦y⟧ = q}.Countable) : ∃ (U₀ : Set α) (U₁ : Set α), IsClosed U₀ ∧ IsClosed U₁ ∧ U₀ ⊆ U ∧ U₁ ⊆ U ∧ Disjoint U₀ U₁ ∧ ¬{q : Quotient r | ∃ y ∈ U₀, ⟦y⟧ = q}.Countable ∧ ¬{q : Quotient r | ∃ y ∈ U₁, ⟦y⟧ = q}.Countable ∧ ∀ x ∈ U₀, ∀ y ∈ U₁, ¬r x y

Splitting lemma for closed equivalence relations on metric spaces. If a closed set U meets uncountably many classes of a closed equivalence relation, it contains disjoint closed subsets each meeting uncountably many classes with no cross-equivalence.

Core Silver theorem

theorem silver_core_closed {α : Type u} [MetricSpace α] [CompleteSpace α] [SecondCountableTopology α] (r : Setoid α) (hclosed_r : IsClosed {p : α × α | r p.1 p.2}) : Countable (Quotient r) ∨ ∃ (f : (ℕ → Bool) → α), Continuous f ∧ Function.Injective f ∧ ∀ (a b : ℕ → Bool), a ≠ b → ¬r (f a) (f b)

Silver's theorem (core Polish space version, for closed equivalence relations): A closed equivalence relation on a Polish space has countably many equivalence classes, or admits a continuous injection from Cantor space whose images are pairwise inequivalent.