The graphs G_S and G₀ on Cantor space

For a set S of finite binary words, orientedGS S joins s ⌢ false ⌢ x to s ⌢ true ⌢ x, for s ∈ S and a common infinite tail x. Its symmetrization is the simple graph gSGraph S. Each word contributes a compact set of edges, so both edge relations are Fσ and Borel. The endpoints differ at coordinate s.length, so symmetrization removes no edges.

DenseWords S means that every word extends to a word of S; SparseWords S means that S has at most one word of each length. Density is the hypothesis in Miller's independence lemma, while sparseness permits a fusion construction to add at most one new edge at each level. The explicit canonicalWords has both properties, and gZero is its graph, the Kechris–Solecki–Todorcevic graph G₀.

Miller's independence lemma exists_mem_orientedGS_of_not_isMeagre says that for dense S every non-meagre subset of Cantor space with the Baire property contains an oriented edge. Consequently, for dense S:

• isMeagre_of_isIndepSet_gSGraph: independent sets with the Baire property are meagre;
• exists_not_baireMeasurableSet_colorClass: a coloring of gSGraph S by countably many colors has a color class without the Baire property, so orientedGS S has no countable Borel coloring (not_hasCountableBorelColoring_orientedGS) and gSGraph S has no measurable coloring by ℕ; and no relation G receiving a measurable map that sends the oriented edges of orientedGS S to pairs of G has a countable Borel coloring (not_hasCountableBorelColoring_of_orientedGS_hom);
• isMeagre_setOf_comp_of_forall_gSGraph_adj: if a measurable map φ sends the edges of gSGraph S to inequivalent pairs of an equivalence relation E with measurable classes, then every section {b | E (φ a) (φ b)} of the pulled-back relation is meagre.

The last statement is what makes pulled-back relations meagre, through the Kuratowski–Ulam theorem, in the category proof of Silver's theorem. For the canonical words, G₀ itself has no measurable coloring by ℕ (not_exists_measurable_coloring_gZero).

Density cannot be dropped. A dense word set has words of infinitely many lengths (DenseWords.infinite_image_length), and when the words of S have only finitely many lengths, the parity of the coordinates at those lengths changes along every edge. So gSGraph S then has a continuous coloring by Bool (exists_continuous_coloring_gSGraph), and orientedGS S has a countable Borel coloring (hasCountableBorelColoring_orientedGS). For S = {[]}, which is sparse, this coloring is the first coordinate.

References

• A. S. Kechris, S. Solecki and S. Todorcevic, Borel chromatic numbers, Advances in Mathematics 141 (1999), 1–44.
• B. D. Miller, The graph-theoretic approach to descriptive set theory, Bulletin of Symbolic Logic 18 (2012), 554–575.

The word-and-common-tail description also appears in InfinitaryLogic/Descriptive/GSGraph.lean of cameronfreer/infinitary-logic (Apache-2.0), checkpoint 518a366cba97b1ae8c4dc64a297a396939bc3e0b. Here the oriented relation and Mathlib simple graph are separate, and the canonical words have every natural number as a length.

def TauCeti.orientedGS (S : Set (List Bool)) : Set ((ℕ → Bool) × (ℕ → Bool))

The oriented graph associated to binary words S: change the bit just after a word of S from false to true, keeping the same tail.

theorem TauCeti.mem_orientedGS_iff {S : Set (List Bool)} {a b : ℕ → Bool} : (a, b) ∈ orientedGS S ↔ ∃ s ∈ S, ∃ (x : ℕ → Bool), a = PiNat.prependWord (s ++ [false]) x ∧ b = PiNat.prependWord (s ++ [true]) x

Membership in the oriented graph is witnessed by a word and a common tail.

theorem TauCeti.prependWord_mem_orientedGS {S : Set (List Bool)} {s : List Bool} (hs : s ∈ S) (x : ℕ → Bool) : (PiNat.prependWord (s ++ [false]) x, PiNat.prependWord (s ++ [true]) x) ∈ orientedGS S

Every word of S and every tail give an oriented edge.

theorem TauCeti.ne_of_mem_orientedGS {S : Set (List Bool)} {a b : ℕ → Bool} (h : (a, b) ∈ orientedGS S) : a ≠ b

The two endpoints of an oriented edge are distinct.

theorem TauCeti.mem_orientedGS_iff_exists_flipAt {S : Set (List Bool)} {a b : ℕ → Bool} : (a, b) ∈ orientedGS S ↔ ∃ s ∈ S, a ∈ PiNat.wordCylinder (s ++ [false]) ∧ (PiNat.flipAt s.length) a = b

An oriented edge is the graph of a coordinate flip restricted to the false half of a word cylinder.

theorem TauCeti.orientedGS_mono {S T : Set (List Bool)} (h : S ⊆ T) : orientedGS S ⊆ orientedGS T

Enlarging the word set enlarges the oriented graph.

@[simp]

theorem TauCeti.orientedGS_empty : orientedGS ∅ = ∅

def TauCeti.gSGraph (S : Set (List Bool)) : SimpleGraph (ℕ → Bool)

The simple graph obtained by forgetting the orientation of orientedGS S.

@[simp]

theorem TauCeti.gSGraph_adj_iff {S : Set (List Bool)} {a b : ℕ → Bool} : (gSGraph S).Adj a b ↔ (a, b) ∈ orientedGS S ∨ (b, a) ∈ orientedGS S

Adjacency is precisely an oriented edge in one of the two directions; no additional inequality hypothesis is needed.

theorem TauCeti.gSGraph_mono {S T : Set (List Bool)} (h : S ⊆ T) : gSGraph S ≤ gSGraph T

Enlarging the word set enlarges the simple graph.

@[simp]

theorem TauCeti.gSGraph_empty : gSGraph ∅ = ⊥

theorem TauCeti.orientedGS_eq_biUnion (S : Set (List Bool)) : orientedGS S = ⋃ s ∈ S, Set.range fun (x : ℕ → Bool) => (PiNat.prependWord (s ++ [false]) x, PiNat.prependWord (s ++ [true]) x)

The oriented graph is a countable union of compact edge sets, one for each word.

theorem TauCeti.isClosed_orientedGS_singleton (s : List Bool) : IsClosed (orientedGS {s})

The edges contributed by one word form a closed set.

theorem TauCeti.isGδ_compl_orientedGS (S : Set (List Bool)) : IsGδ (orientedGS S)ᶜ

The oriented edge relation is Fσ, expressed as a Gδ complement.

theorem TauCeti.measurableSet_orientedGS (S : Set (List Bool)) : MeasurableSet (orientedGS S)

The oriented edge relation is Borel.

theorem TauCeti.isGδ_compl_gSGraph (S : Set (List Bool)) : IsGδ {p : (ℕ → Bool) × (ℕ → Bool) | (gSGraph S).Adj p.1 p.2}ᶜ

The unoriented edge relation is Fσ, expressed as a Gδ complement.

theorem TauCeti.measurableSet_gSGraph (S : Set (List Bool)) : MeasurableSet {p : (ℕ → Bool) × (ℕ → Bool) | (gSGraph S).Adj p.1 p.2}

The simple graph has a Borel edge relation.

Dense and sparse words

def TauCeti.DenseWords (S : Set (List Bool)) : Prop

A word set is dense if every word is a prefix of some member.

def TauCeti.SparseWords (S : Set (List Bool)) : Prop

A word set is sparse if it has at most one member of each length.

theorem TauCeti.denseWords_iff {S : Set (List Bool)} : DenseWords S ↔ ∀ (r : List Bool), ∃ s ∈ S, r <+: s

Unfolding the density condition.

theorem TauCeti.sparseWords_iff {S : Set (List Bool)} : SparseWords S ↔ ∀ s ∈ S, ∀ t ∈ S, s.length = t.length → s = t

Unfolding the sparseness condition.

theorem TauCeti.DenseWords.mono {S T : Set (List Bool)} (h : DenseWords S) (hST : S ⊆ T) : DenseWords T

Density passes to larger word sets.

theorem TauCeti.SparseWords.mono {S T : Set (List Bool)} (h : SparseWords T) (hST : S ⊆ T) : SparseWords S

Sparseness passes to smaller word sets.

theorem TauCeti.DenseWords.infinite_image_length {S : Set (List Bool)} (h : DenseWords S) : (List.length '' S).Infinite

A dense word set has words of infinitely many lengths.

def TauCeti.canonicalWord (n : ℕ) : List Bool

Decode the first component of Nat.unpair n, then pad the decoded word with false to length n. If decoding fails or the word is too long, use the all-false word.

@[simp]

theorem TauCeti.length_canonicalWord (n : ℕ) : (canonicalWord n).length = n

The canonical word at stage n has length exactly n.

theorem TauCeti.prefix_canonicalWord_pair (r : List Bool) {k : ℕ} (hk : r.length ≤ k) : r <+: canonicalWord (Nat.pair (Encodable.encode r) k)

Coding a word in the first component of a sufficiently large pair produces an extension of that word.

theorem TauCeti.canonicalWord_injective : Function.Injective canonicalWord

Canonical words are distinguished by their lengths.

def TauCeti.canonicalWords : Set (List Bool)

The canonical dense sparse word set defining G₀.

@[simp]

theorem TauCeti.mem_canonicalWords_iff {s : List Bool} : s ∈ canonicalWords ↔ ∃ (n : ℕ), canonicalWord n = s

theorem TauCeti.canonicalWord_mem_canonicalWords (n : ℕ) : canonicalWord n ∈ canonicalWords

The canonical word at every stage belongs to the canonical word set.

theorem TauCeti.denseWords_canonicalWords : DenseWords canonicalWords

Every finite word extends to a canonical word.

theorem TauCeti.sparseWords_canonicalWords : SparseWords canonicalWords

There is only one canonical word of each length.

theorem TauCeti.exists_unique_mem_canonicalWords_length (n : ℕ) : ∃! s : List Bool, s ∈ canonicalWords ∧ s.length = n

There is exactly one canonical word of each length.

theorem TauCeti.mem_canonicalWords_iff_eq_canonicalWord {s : List Bool} : s ∈ canonicalWords ↔ s = canonicalWord s.length

The unique canonical word of length n is canonicalWord n.

def TauCeti.gZero : SimpleGraph (ℕ → Bool)

The Kechris–Solecki–Todorcevic graph G₀ on Cantor space.

@[simp]

theorem TauCeti.gZero_adj_iff {a b : ℕ → Bool} : gZero.Adj a b ↔ (a, b) ∈ orientedGS canonicalWords ∨ (b, a) ∈ orientedGS canonicalWords

G₀ has exactly the two orientations of the canonical word edges.

Miller's independence lemma

theorem TauCeti.exists_mem_orientedGS_of_not_isMeagre {S : Set (List Bool)} {A : Set (ℕ → Bool)} (hS : DenseWords S) (hA : BaireMeasurableSet A) (hn : ¬IsMeagre A) : ∃ a ∈ A, ∃ b ∈ A, (a, b) ∈ orientedGS S

Miller's independence lemma. If every word extends to a word of S, then every non-meagre subset of Cantor space with the Baire property contains both ends of an oriented edge of orientedGS S.

theorem TauCeti.exists_gSGraph_adj_of_not_isMeagre {S : Set (List Bool)} {A : Set (ℕ → Bool)} (hS : DenseWords S) (hA : BaireMeasurableSet A) (hn : ¬IsMeagre A) : ∃ a ∈ A, ∃ b ∈ A, (gSGraph S).Adj a b

Miller's independence lemma, for the simple graph: if S is dense, then every non-meagre subset of Cantor space with the Baire property contains two adjacent points of gSGraph S.

theorem TauCeti.isMeagre_of_isIndepSet_gSGraph {S : Set (List Bool)} {A : Set (ℕ → Bool)} (hS : DenseWords S) (hA : BaireMeasurableSet A) (hind : (gSGraph S).IsIndepSet A) : IsMeagre A

If S is dense, then every independent set of gSGraph S with the Baire property is meagre.

theorem TauCeti.exists_not_baireMeasurableSet_colorClass {S : Set (List Bool)} (hS : DenseWords S) {ι : Type u_1} [Countable ι] (c : (gSGraph S).Coloring ι) : ∃ (i : ι), ¬BaireMeasurableSet (c.colorClass i)

If S is dense, then every coloring of gSGraph S by countably many colors has a color class without the Baire property.

theorem TauCeti.not_hasCountableBorelColoring_orientedGS {S : Set (List Bool)} (hS : DenseWords S) : ¬SetRel.HasCountableBorelColoring (orientedGS S)

If S is dense, then the oriented graph orientedGS S has no countable Borel coloring.

theorem TauCeti.not_hasCountableBorelColoring_of_orientedGS_hom {S : Set (List Bool)} {X : Type u_1} [MeasurableSpace X] {G : SetRel X X} (hS : DenseWords S) {φ : (ℕ → Bool) → X} (hφ : Measurable φ) (hφG : ∀ ⦃y z : ℕ → Bool⦄, (y, z) ∈ orientedGS S → (φ y, φ z) ∈ G) : ¬G.HasCountableBorelColoring

If every word extends to a word of S and a measurable map of Cantor space sends every oriented edge of orientedGS S to a pair of G, then G has no countable Borel coloring. This is the exclusivity half of the G₀ dichotomy.

theorem TauCeti.not_exists_measurable_coloring_gSGraph {S : Set (List Bool)} (hS : DenseWords S) : ¬∃ (c : (gSGraph S).Coloring ℕ), Measurable ⇑c

If S is dense, then gSGraph S has no measurable coloring by ℕ.

theorem TauCeti.isMeagre_setOf_of_forall_gSGraph_adj {S : Set (List Bool)} (hS : DenseWords S) {E : Setoid (ℕ → Bool)} (hE : ∀ ⦃a b : ℕ → Bool⦄, (gSGraph S).Adj a b → ¬E a b) {a : ℕ → Bool} (ha : BaireMeasurableSet {b : ℕ → Bool | E a b}) : IsMeagre {b : ℕ → Bool | E a b}

If S is dense and no edge of gSGraph S joins two E-equivalent points, then every class of E with the Baire property is meagre.

theorem TauCeti.isMeagre_setOf_comp_of_forall_gSGraph_adj {S : Set (List Bool)} (hS : DenseWords S) {X : Type u_1} [MeasurableSpace X] {E : Setoid X} (hE : ∀ (x : X), MeasurableSet {y : X | E x y}) {φ : (ℕ → Bool) → X} (hφ : Measurable φ) (hφE : ∀ ⦃a b : ℕ → Bool⦄, (gSGraph S).Adj a b → ¬E (φ a) (φ b)) (a : ℕ → Bool) : IsMeagre {b : ℕ → Bool | E (φ a) (φ b)}

Let E be an equivalence relation with measurable classes and φ a measurable map from Cantor space sending the edges of gSGraph S to E-inequivalent pairs. If S is dense, then every section {b | E (φ a) (φ b)} of the pulled-back relation is meagre.

theorem TauCeti.not_exists_measurable_coloring_gZero : ¬∃ (c : gZero.Coloring ℕ), Measurable ⇑c

The Kechris–Solecki–Todorcevic graph G₀ has no measurable coloring by ℕ.

Word sets with finitely many lengths

theorem TauCeti.exists_continuous_coloring_gSGraph {S : Set (List Bool)} (hS : (List.length '' S).Finite) : ∃ (c : (gSGraph S).Coloring Bool), Continuous ⇑c

If the words of S have only finitely many lengths, then gSGraph S has a continuous coloring by Bool: the parity of the coordinates at those lengths. In particular, gSGraph S is two-colorable, although S may be sparse.

theorem TauCeti.hasCountableBorelColoring_orientedGS {S : Set (List Bool)} (hS : (List.length '' S).Finite) : SetRel.HasCountableBorelColoring (orientedGS S)

If the words of S have only finitely many lengths, then the oriented graph orientedGS S has a countable Borel coloring. Since {[]} is such a word set and is sparse, the density hypothesis of not_hasCountableBorelColoring_orientedGS cannot be dropped, even for sparse word sets.