The Kechris–Solecki–Todorcevic G₀ dichotomy

Let X be a Polish space with its Borel σ-algebra and G : SetRel X X an analytic relation, read as a directed graph in which loops are allowed. The G₀ dichotomy says that exactly one of the following holds:

• G has a countable Borel coloring (SetRel.HasCountableBorelColoring);
• there is a continuous map φ of Cantor space into X sending every oriented edge of orientedGS canonicalWords to a pair of G.

The homomorphism half, exists_continuous_orientedGS_hom, says that the second alternative holds when the first fails, and it does so for every sparse word set S (at most one word of each length) in place of canonicalWords; neither symmetry nor irreflexivity of G is assumed. The two alternatives exclude each other whenever S is dense (not_hasCountableBorelColoring_of_orientedGS_hom, in TauCeti.SetTheory.Descriptive.GSGraph): a coloring of G would pull back to a countable Borel coloring of orientedGS S, which Miller's independence lemma forbids. For a simple graph G on X with analytic edge relation, the dichotomy reads: either G has a measurable coloring by ℕ, or there is a continuous homomorphism gZero →g G (SimpleGraph.g0_dichotomy).

Applied to the inequivalence relation of a Borel equivalence relation E with uncountably many classes, the homomorphism half gives a continuous map sending gZero-adjacent points to E-inequivalent points, and more generally adjacent points of gSGraph S for every sparse S (Setoid.exists_continuous_forall_gSGraph_adj_not). This is the input to the category proof of Silver's theorem.

The fusion construction

The homomorphism half is proved by B. D. Miller's fusion argument through the σ-ideal of small families of assignments (SetRel.IsSmallFamily). Choose a complete metric on X and write G as the range of a continuous g : (ℕ → ℕ) → X × X. The vertices of level n are the binary words of length n, recorded newest letter first as in PiNat.res. A level edge is the level-n trace of an oriented edge of orientedGS S, a pair r ++ false :: s.reverse and r ++ true :: s.reverse with s ∈ S. A stage of level n is an analytic family of maps from the vertices of level n to X that is not small, whose members are uniformly within 2⁻ⁿ of each other at every vertex, together with a word of naturals for every level edge through whose cylinder g witnesses the values of every member at the two ends of that edge.

A stage of level n + 1 is obtained by combining two members of a stage of level n according to the newest letter. When S has a word s of length n, the two combined members are required to form a pair of G at s.reverse, which creates the one fresh level edge (false :: s.reverse, true :: s.reverse) (SetRel.not_isSmallFamily_comb_cross); sparseness is what makes the fresh edge unique. Every witness word is then extended by one letter (SetRel.exists_subset_not_isSmallFamily_witness_extension) and the vertices are shrunk (SetRel.exists_subset_not_isSmallFamily_dist_lt). Picking one member per stage, the values along a branch of Cantor space form a Cauchy sequence whose limit is the continuous map φ. Along an oriented edge the witness words grow and nest, and so define a point of Baire space whose image under g is the pair of limit values.

Main results

• TauCeti.exists_continuous_orientedGS_hom: the homomorphism half, for every sparse S.
• TauCeti.g0_dichotomy_oriented: the G₀ dichotomy for analytic relations.
• SimpleGraph.g0_dichotomy: the G₀ dichotomy for simple graphs.
• Setoid.exists_continuous_forall_gSGraph_adj_not: a Borel equivalence relation with uncountably many classes receives, for every sparse S, a continuous map sending adjacent points of gSGraph S to inequivalent points.

References

• A. S. Kechris, S. Solecki and S. Todorcevic, Borel chromatic numbers, Advances in Mathematics 141 (1999), 1–44, Theorem 6.3.
• B. D. Miller, The graph-theoretic approach to descriptive set theory, Bulletin of Symbolic Logic 18 (2012), 554–575, the classical proof of the G₀ dichotomy through small families.
• The fusion follows FusionStage, exists_fusionStage_succ and exists_gsGraph_hom in InfinitaryLogic/Descriptive/G0Fusion.lean of cameronfreer/infinitary-logic (Apache-2.0), checkpoint 518a366cba97b1ae8c4dc64a297a396939bc3e0b. There the homomorphism half is proved for one fixed word set and symmetric relations; here it is proved for every sparse word set and every analytic relation, with vertices recorded newest letter first, and exclusivity and both forms of the dichotomy are added.

Level edges

Stages of the fusion

The G₀ dichotomy

theorem TauCeti.exists_continuous_orientedGS_hom {X : Type u_1} [TopologicalSpace X] [PolishSpace X] [MeasurableSpace X] [BorelSpace X] {G : SetRel X X} (hG : MeasureTheory.AnalyticSet G) {S : Set (List Bool)} (hS : SparseWords S) (hcol : ¬G.HasCountableBorelColoring) : ∃ (φ : (ℕ → Bool) → X), Continuous φ ∧ ∀ ⦃y z : ℕ → Bool⦄, (y, z) ∈ orientedGS S → (φ y, φ z) ∈ G

The homomorphism half of the G₀ dichotomy. Let G be an analytic relation on a Polish space with no countable Borel coloring. For every set S of words with at most one word of each length, some continuous map of Cantor space into the space sends every oriented edge of orientedGS S to a pair of G.

theorem TauCeti.g0_dichotomy_oriented {X : Type u_1} [TopologicalSpace X] [PolishSpace X] [MeasurableSpace X] [BorelSpace X] {G : SetRel X X} (hG : MeasureTheory.AnalyticSet G) : Xor G.HasCountableBorelColoring (∃ (φ : (ℕ → Bool) → X), Continuous φ ∧ ∀ ⦃y z : ℕ → Bool⦄, (y, z) ∈ orientedGS canonicalWords → (φ y, φ z) ∈ G)

The G₀ dichotomy, oriented form. An analytic relation G on a Polish space has a countable Borel coloring, or there is a continuous map of Cantor space sending every oriented edge of orientedGS canonicalWords to a pair of G, and not both.

theorem SimpleGraph.g0_dichotomy {X : Type u_1} [TopologicalSpace X] [PolishSpace X] [MeasurableSpace X] [BorelSpace X] (G : SimpleGraph X) (hG : MeasureTheory.AnalyticSet {p : X × X | G.Adj p.1 p.2}) : Xor (∃ (c : G.Coloring ℕ), Measurable ⇑c) (∃ (φ : TauCeti.gZero →g G), Continuous ⇑φ)

The Kechris–Solecki–Todorcevic G₀ dichotomy. A simple graph on a Polish space whose edge relation is analytic has a measurable coloring by ℕ, or receives a continuous homomorphism from gZero, and not both.

theorem Setoid.exists_continuous_forall_gSGraph_adj_not {X : Type u_1} [TopologicalSpace X] [PolishSpace X] [MeasurableSpace X] [BorelSpace X] (E : Setoid X) (hE : MeasurableSet {p : X × X | E p.1 p.2}) (hc : ¬Countable (Quotient E)) {S : Set (List Bool)} (hS : TauCeti.SparseWords S) : ∃ (φ : (ℕ → Bool) → X), Continuous φ ∧ ∀ ⦃y z : ℕ → Bool⦄, (TauCeti.gSGraph S).Adj y z → ¬E (φ y) (φ z)

Let E be a Borel equivalence relation on a Polish space with uncountably many classes. For every set S of words with at most one word of each length, some continuous map of Cantor space sends adjacent points of gSGraph S to E-inequivalent points.