Perfect and Cantor antichains of an equivalence relation

Let E be an equivalence relation on a topological space X and A ⊆ X. Dichotomy theorems for equivalence relations, such as Silver's theorem, conclude that E either has few classes on A or has a large family of pairwise inequivalent points there:

• E.HasCantorAntichainOn A: a continuous map of Cantor space ℕ → Bool into A sending distinct points to E-inequivalent points. It is automatically injective, by reflexivity of E.
• E.HasPerfectAntichainOn A: a nonempty perfect subset of A of pairwise E-inequivalent points.
• E.IsThinOn A: there is no perfect antichain.

Builders produce the Cantor form; ambient statements use the perfect form. In a Hausdorff space a Cantor antichain gives a perfect antichain, its range; in a completely metrizable space a perfect antichain gives a Cantor antichain, through Perfect.exists_nat_bool_injection. In particular the two agree on Polish spaces.

A Cantor antichain on A gives at least continuum many classes, both of E and of its restriction E.comap ((↑) : A → X) to A. The restriction is reached through Setoid.hasCantorAntichainOn_subtype_iff, which passes Cantor antichains between A and the whole subtype ↥A. A second-countable T₀ space, in particular a Polish space, has at most continuum many points, so there the number of classes is exactly 𝔠.

On a Polish space, Cantor antichains are the same as uncountable Borel sets of pairwise inequivalent points: the range of a Cantor antichain is compact, and the perfect set theorem for Borel sets extracts a Cantor antichain from such a set. Since a measurable embedding moves Borel sets to Borel sets, Cantor antichains and thinness transport along a measurable embedding g : X → Y of Polish spaces that pulls an equivalence relation F on Y back to E, with no Borel hypothesis on A, E or F. This is how antichains built in one Polish space, for example a space of codes, are carried to another. Perfect antichains transport along any homeomorphism pulling F back to E, with no hypothesis on the spaces.

Main definitions

• Setoid.HasCantorAntichainOn, Setoid.HasPerfectAntichainOn, Setoid.IsThinOn.

Main results

• Setoid.HasCantorAntichainOn.mono, Setoid.HasCantorAntichainOn.mono_relation and their perfect and thin counterparts: monotonicity in the ambient set and in the relation.
• Setoid.HasCantorAntichainOn.mono_topology: a Cantor antichain for a finer topology is one for a coarser topology.
• Setoid.hasCantorAntichainOn_subtype_iff: Cantor antichains on A and on ↥A.
• Setoid.HasCantorAntichainOn.continuum_le_mk_quotient and Setoid.HasCantorAntichainOn.continuum_le_mk_quotient_comap: at least continuum many classes, of E and of its restriction to A.
• Setoid.HasCantorAntichainOn.mk_quotient_eq_continuum and Setoid.HasCantorAntichainOn.mk_quotient_comap_eq_continuum: exactly continuum many classes in a second-countable T₀ space, such as a Polish space.
• Setoid.HasCantorAntichainOn.hasPerfectAntichainOn (Hausdorff spaces), Setoid.HasPerfectAntichainOn.hasCantorAntichainOn (completely metrizable spaces) and Setoid.hasCantorAntichainOn_iff_hasPerfectAntichainOn.
• Setoid.HasCantorAntichainOn.exists_measurableSet and Setoid.hasCantorAntichainOn_iff_exists_measurableSet: Cantor antichains and uncountable Borel antichains.
• Setoid.hasCantorAntichainOn_image_iff, Setoid.isThinOn_image_iff: transport along measurable embeddings of Polish spaces.
• Setoid.hasPerfectAntichainOn_image_homeomorph_iff: transport of perfect antichains along homeomorphisms of arbitrary topological spaces.

References

• Ported from cameronfreer/infinitary-logic at commit 518a366cba97b1ae8c4dc64a297a396939bc3e0b, InfinitaryLogic/Descriptive/PerfectAntichain.lean.
• Divergences from that source: the predicates are in the Setoid namespace; relation monotonicity uses Mathlib's order on setoids; the subtype bridge is an equivalence, with the continuum bound for the quotient of the subtype; the perfect-to-Cantor direction assumes a completely metrizable topology rather than a complete metric.
• Setoid.hasCantorAntichainOn_image_iff and Setoid.isThinOn_image_iff are stated as in InfinitaryLogic/Descriptive/AntichainTransport.lean of cameronfreer/infinitary-logic at the same commit, which moves the witness as an uncountable Borel set and re-extracts a Cantor copy. Here that argument is factored through Setoid.hasCantorAntichainOn_iff_exists_measurableSet.
• A. S. Kechris, Classical Descriptive Set Theory, Graduate Texts in Mathematics 156, Springer, 1995, Theorem 13.6 (the perfect set theorem for Borel sets, used to extract Cantor antichains from Borel antichains).

def Setoid.HasCantorAntichainOn {X : Type u} [TopologicalSpace X] (E : Setoid X) (A : Set X) : Prop

A carries a Cantor antichain for E: a continuous map of Cantor space into A whose distinct points have E-inequivalent images.

def Setoid.HasPerfectAntichainOn {X : Type u} [TopologicalSpace X] (E : Setoid X) (A : Set X) : Prop

A carries a perfect antichain for E: a nonempty perfect subset of A whose points are pairwise E-inequivalent.

def Setoid.IsThinOn {X : Type u} [TopologicalSpace X] (E : Setoid X) (A : Set X) : Prop

A is thin for E: it carries no perfect antichain.

theorem Setoid.hasCantorAntichainOn_iff {X : Type u} [TopologicalSpace X] {E : Setoid X} {A : Set X} : E.HasCantorAntichainOn A ↔ ∃ (f : (ℕ → Bool) → X), Continuous f ∧ (∀ (a : ℕ → Bool), f a ∈ A) ∧ ∀ (a b : ℕ → Bool), a ≠ b → ¬E (f a) (f b)

Unfolding lemma for Setoid.HasCantorAntichainOn.

theorem Setoid.hasPerfectAntichainOn_iff {X : Type u} [TopologicalSpace X] {E : Setoid X} {A : Set X} : E.HasPerfectAntichainOn A ↔ ∃ (P : Set X), Perfect P ∧ P.Nonempty ∧ P ⊆ A ∧ ∀ x ∈ P, ∀ y ∈ P, E x y → x = y

Unfolding lemma for Setoid.HasPerfectAntichainOn.

theorem Setoid.isThinOn_iff {X : Type u} [TopologicalSpace X] {E : Setoid X} {A : Set X} : E.IsThinOn A ↔ ¬E.HasPerfectAntichainOn A

Unfolding lemma for Setoid.IsThinOn.

Monotonicity

theorem Setoid.HasCantorAntichainOn.mono {X : Type u} [TopologicalSpace X] {E : Setoid X} {A B : Set X} (h : E.HasCantorAntichainOn A) (hAB : A ⊆ B) : E.HasCantorAntichainOn B

A Cantor antichain on A is one on every superset of A.

theorem Setoid.HasPerfectAntichainOn.mono {X : Type u} [TopologicalSpace X] {E : Setoid X} {A B : Set X} (h : E.HasPerfectAntichainOn A) (hAB : A ⊆ B) : E.HasPerfectAntichainOn B

A perfect antichain on A is one on every superset of A.

theorem Setoid.IsThinOn.anti {X : Type u} [TopologicalSpace X] {E : Setoid X} {A B : Set X} (h : E.IsThinOn B) (hAB : A ⊆ B) : E.IsThinOn A

A subset of a thin set is thin.

theorem Setoid.HasCantorAntichainOn.mono_relation {X : Type u} [TopologicalSpace X] {E F : Setoid X} {A : Set X} (hEF : E ≤ F) (h : F.HasCantorAntichainOn A) : E.HasCantorAntichainOn A

A Cantor antichain for a coarser relation F is one for the finer relation E.

theorem Setoid.HasPerfectAntichainOn.mono_relation {X : Type u} [TopologicalSpace X] {E F : Setoid X} {A : Set X} (hEF : E ≤ F) (h : F.HasPerfectAntichainOn A) : E.HasPerfectAntichainOn A

A perfect antichain for a coarser relation F is one for the finer relation E.

theorem Setoid.IsThinOn.mono_relation {X : Type u} [TopologicalSpace X] {E F : Setoid X} {A : Set X} (hEF : E ≤ F) (h : E.IsThinOn A) : F.IsThinOn A

A set thin for a finer relation E is thin for every coarser relation F.

theorem Setoid.HasCantorAntichainOn.mono_topology {X : Type u} {E : Setoid X} {A : Set X} {t t' : TopologicalSpace X} (htt' : t ≤ t') (h : E.HasCantorAntichainOn A) : E.HasCantorAntichainOn A

A Cantor antichain for a finer topology t is one for every coarser topology t': a witness continuous into t remains continuous into t'. This carries witnesses built in a finer, for example Polish, topology back to the original one.

Injectivity, subtypes and the number of classes

theorem Setoid.HasCantorAntichainOn.exists_injective {X : Type u} [TopologicalSpace X] {E : Setoid X} {A : Set X} (h : E.HasCantorAntichainOn A) : ∃ (f : (ℕ → Bool) → X), Continuous f ∧ Set.range f ⊆ A ∧ Function.Injective f ∧ ∀ (a b : ℕ → Bool), a ≠ b → ¬E (f a) (f b)

A Cantor antichain is injective: equal images are equivalent, by reflexivity. The witness keeps its antichain property.

theorem Setoid.hasCantorAntichainOn_subtype_iff {X : Type u} [TopologicalSpace X] {E : Setoid X} {A : Set X} : (comap Subtype.val E).HasCantorAntichainOn Set.univ ↔ E.HasCantorAntichainOn A

The subtype bridge. A carries a Cantor antichain for E exactly when the whole subtype ↥A carries one for the restriction of E to A.

theorem Setoid.HasCantorAntichainOn.continuum_le_mk_quotient {X : Type u} [TopologicalSpace X] {E : Setoid X} {A : Set X} (h : E.HasCantorAntichainOn A) : Cardinal.continuum ≤ Cardinal.mk (Quotient E)

At least continuum many classes. If A carries a Cantor antichain for E, then E has at least continuum many classes.

theorem Setoid.HasCantorAntichainOn.continuum_le_mk_quotient_comap {X : Type u} [TopologicalSpace X] {E : Setoid X} {A : Set X} (h : E.HasCantorAntichainOn A) : Cardinal.continuum ≤ Cardinal.mk (Quotient (comap Subtype.val E))

At least continuum many classes on A. If A carries a Cantor antichain for E, then the restriction of E to A has at least continuum many classes.

theorem Setoid.HasCantorAntichainOn.mk_quotient_eq_continuum {X : Type u} [TopologicalSpace X] {E : Setoid X} {A : Set X} [SecondCountableTopology X] [T0Space X] (h : E.HasCantorAntichainOn A) : Cardinal.mk (Quotient E) = Cardinal.continuum

Exactly continuum many classes. In a second-countable T₀ space, in particular a Polish space, a Cantor antichain on A for E gives E exactly continuum many classes.

theorem Setoid.HasCantorAntichainOn.mk_quotient_comap_eq_continuum {X : Type u} [TopologicalSpace X] {E : Setoid X} {A : Set X} [SecondCountableTopology X] [T0Space X] (h : E.HasCantorAntichainOn A) : Cardinal.mk (Quotient (comap Subtype.val E)) = Cardinal.continuum

Exactly continuum many classes on A. In a second-countable T₀ space, in particular a Polish space, a Cantor antichain on A for E gives the restriction of E to A exactly continuum many classes.

Cantor antichains and perfect antichains

theorem Setoid.HasCantorAntichainOn.hasPerfectAntichainOn {X : Type u} [TopologicalSpace X] {E : Setoid X} {A : Set X} [T2Space X] (h : E.HasCantorAntichainOn A) : E.HasPerfectAntichainOn A

A Cantor antichain is a perfect antichain in a Hausdorff space: its range is closed, as the continuous injective image of a compact space, and has no isolated points.

theorem Setoid.HasPerfectAntichainOn.hasCantorAntichainOn {X : Type u} [TopologicalSpace X] {E : Setoid X} {A : Set X} [TopologicalSpace.IsCompletelyMetrizableSpace X] (h : E.HasPerfectAntichainOn A) : E.HasCantorAntichainOn A

A perfect antichain gives a Cantor antichain in a completely metrizable space, through the Cantor injection of a nonempty perfect set.

theorem Setoid.hasCantorAntichainOn_iff_hasPerfectAntichainOn {X : Type u} [TopologicalSpace X] {E : Setoid X} {A : Set X} [TopologicalSpace.IsCompletelyMetrizableSpace X] : E.HasCantorAntichainOn A ↔ E.HasPerfectAntichainOn A

In a completely metrizable space, in particular a Polish space, Cantor antichains and perfect antichains exist together.

theorem Setoid.isThinOn_iff_not_hasCantorAntichainOn {X : Type u} [TopologicalSpace X] {E : Setoid X} {A : Set X} [TopologicalSpace.IsCompletelyMetrizableSpace X] : E.IsThinOn A ↔ ¬E.HasCantorAntichainOn A

In a completely metrizable space, a set is thin exactly when it carries no Cantor antichain.

Borel antichains and transport along measurable embeddings

theorem Setoid.HasCantorAntichainOn.exists_measurableSet {X : Type u} [TopologicalSpace X] {E : Setoid X} {A : Set X} [T2Space X] [MeasurableSpace X] [OpensMeasurableSpace X] (h : E.HasCantorAntichainOn A) : ∃ s ⊆ A, MeasurableSet s ∧ ¬s.Countable ∧ ∀ x ∈ s, ∀ y ∈ s, E x y → x = y

The range of a Cantor antichain is a Borel antichain. In a Hausdorff space whose open sets are measurable, a Cantor antichain on A has as its range an uncountable measurable subset of A whose points are pairwise E-inequivalent.

theorem Setoid.hasCantorAntichainOn_iff_exists_measurableSet {X : Type u} [TopologicalSpace X] {E : Setoid X} {A : Set X} [PolishSpace X] [MeasurableSpace X] [BorelSpace X] : E.HasCantorAntichainOn A ↔ ∃ s ⊆ A, MeasurableSet s ∧ ¬s.Countable ∧ ∀ x ∈ s, ∀ y ∈ s, E x y → x = y

Cantor antichains are uncountable Borel antichains. On a Polish space, A carries a Cantor antichain for E exactly when it contains an uncountable Borel set of pairwise E-inequivalent points. No Borel hypothesis is made on A or E.

theorem Setoid.hasCantorAntichainOn_image_iff {X : Type u} [TopologicalSpace X] {E : Setoid X} {Y : Type u_1} [TopologicalSpace Y] [PolishSpace X] [MeasurableSpace X] [BorelSpace X] [PolishSpace Y] [MeasurableSpace Y] [BorelSpace Y] {F : Setoid Y} {g : X → Y} (hg : MeasurableEmbedding g) (hrel : ∀ (x y : X), F (g x) (g y) ↔ E x y) (A : Set X) : F.HasCantorAntichainOn (g '' A) ↔ E.HasCantorAntichainOn A

Transport of Cantor antichains. Let g : X → Y be a measurable embedding of Polish spaces that pulls F back to E. Then g '' A carries a Cantor antichain for F exactly when A carries one for E. No Borel hypothesis is made on A, E or F.

theorem Setoid.isThinOn_image_iff {X : Type u} [TopologicalSpace X] {E : Setoid X} {Y : Type u_1} [TopologicalSpace Y] [PolishSpace X] [MeasurableSpace X] [BorelSpace X] [PolishSpace Y] [MeasurableSpace Y] [BorelSpace Y] {F : Setoid Y} {g : X → Y} (hg : MeasurableEmbedding g) (hrel : ∀ (x y : X), F (g x) (g y) ↔ E x y) (A : Set X) : F.IsThinOn (g '' A) ↔ E.IsThinOn A

Transport of thinness. Let g : X → Y be a measurable embedding of Polish spaces that pulls F back to E. Then g '' A is thin for F exactly when A is thin for E.

theorem Setoid.hasPerfectAntichainOn_image_homeomorph_iff {X : Type u} [TopologicalSpace X] {E : Setoid X} {Y : Type u_1} [TopologicalSpace Y] {F : Setoid Y} (g : X ≃ₜ Y) (hrel : ∀ (x y : X), F (g x) (g y) ↔ E x y) (A : Set X) : F.HasPerfectAntichainOn (⇑g '' A) ↔ E.HasPerfectAntichainOn A

Transport of perfect antichains along a homeomorphism. If a homeomorphism g : X ≃ₜ Y pulls F back to E, then g '' A carries a perfect antichain for F exactly when A carries one for E. No Polish or Borel hypothesis is made.