Independent sets and countable Borel colorings of relations

A relation G : SetRel X X is read as a directed graph in which loops are allowed.

• SetRel.IsIndependent G A: the set A contains no pair of G, loops included. This differs from Mathlib's SetRel.IsSeparated, which only constrains pairs of distinct points; for the edge relation of a SimpleGraph it agrees with SimpleGraph.IsIndepSet.
• SetRel.HasCountableBorelColoring G: there is a measurable c : X → ℕ with c x ≠ c y for every pair (x, y) of G; equivalently, X is covered by countably many measurable G-independent sets. For the edge relation of a SimpleGraph it is the existence of a measurable G.Coloring ℕ.

Countable Borel colorings are the dividing line of the Kechris–Solecki–Todorcevic G₀ dichotomy. A coloring does not see the direction of a pair, so the dichotomy concerns the symmetrization G ∪ G.inv: an analytic relation G on a Polish space either has a countable Borel coloring, or the graph G₀ on Cantor space admits a continuous homomorphism into G ∪ G.inv.

For an equivalence relation E, the inequivalence relation {p | ¬ E p.1 p.2} has a countable Borel coloring exactly when E has Borel classes and countably many of them, which turns counting the classes of E into a coloring problem.

The Kechris–Solecki–Todorcevic lemma SetRel.exists_measurableSet_isIndependent_superset says that, in a Hausdorff space with its Borel σ-algebra, every analytic independent set of an analytic relation lies in a Borel independent set. It is what lets families of analytic sets be captured by countably many Borel independent sets.

Main definitions

• SetRel.IsIndependent, SetRel.HasCountableBorelColoring.

Main results

• SetRel.hasCountableBorelColoring_iff_exists_cover: colorings are countable covers by measurable independent sets.
• SetRel.HasCountableBorelColoring.mono, SetRel.HasCountableBorelColoring.preimage: colorings restrict to subrelations and pull back along measurable maps.
• SetRel.not_hasCountableBorelColoring_of_mem: a relation with a loop has no coloring.
• SimpleGraph.isIndependent_adj_iff_isIndepSet, SimpleGraph.hasCountableBorelColoring_adj_iff: agreement with Mathlib's independent sets and colorings of simple graphs.
• Setoid.hasCountableBorelColoring_not_iff: the inequivalence relation of E has a countable Borel coloring iff E has countably many classes, all of them Borel. The forward direction Setoid.countable_quotient_of_hasCountableBorelColoring_not alone needs no measurability.
• SetRel.exists_measurableSet_isIndependent_superset: the Kechris–Solecki–Todorcevic lemma.

References

• A. S. Kechris, S. Solecki and S. Todorcevic, Borel chromatic numbers, Advances in Mathematics 141 (1999), 1–44, Proposition 3.1 (independent analytic sets lie in independent Borel sets).
• B. D. Miller, The graph-theoretic approach to descriptive set theory, Bulletin of Symbolic Logic 18 (2012), 554–575.
• SetRel.IsIndependent and SetRel.exists_measurableSet_isIndependent_superset are adapted from RelIndependent and exists_measurableSet_relIndependent_superset in InfinitaryLogic/Descriptive/G0Dichotomy.lean of cameronfreer/infinitary-logic (Apache-2.0), commit 518a366cba97b1ae8c4dc64a297a396939bc3e0b.
• Divergences from that source: independence is in the SetRel namespace, next to Mathlib's SetRel.IsSeparated; the Kechris–Solecki–Todorcevic lemma is proved by two Lusin separations, against the image and then the preimage of the relation, rather than by an ω-recursion against symmetric neighbourhoods, and so holds in every Hausdorff space with its Borel σ-algebra rather than only in Polish spaces.

def SetRel.IsIndependent {X : Type u_1} (G : SetRel X X) (A : Set X) : Prop

A set is independent for a relation G if it contains no pair of G, loops included.

theorem SetRel.isIndependent_iff {X : Type u_1} {G : SetRel X X} {A : Set X} : G.IsIndependent A ↔ ∀ ⦃x : X⦄, x ∈ A → ∀ ⦃y : X⦄, y ∈ A → (x, y) ∉ G

Unfolding lemma for SetRel.IsIndependent.

theorem SetRel.isIndependent_iff_disjoint_prod {X : Type u_1} {G : SetRel X X} {A : Set X} : G.IsIndependent A ↔ Disjoint (A ×ˢ A) G

A set is independent iff its square misses the relation.

theorem SetRel.isIndependent_iff_disjoint_image {X : Type u_1} {G : SetRel X X} {A : Set X} : G.IsIndependent A ↔ Disjoint A (G.image A)

A set is independent iff it misses its own image under the relation.

theorem SetRel.isIndependent_iff_disjoint_preimage {X : Type u_1} {G : SetRel X X} {A : Set X} : G.IsIndependent A ↔ Disjoint A (G.preimage A)

A set is independent iff it misses its own preimage under the relation.

theorem SetRel.isIndependent_iff_isSeparated {X : Type u_1} {G : SetRel X X} {A : Set X} : G.IsIndependent A ↔ G.IsSeparated A ∧ ∀ x ∈ A, (x, x) ∉ G

Independence is separation together with the absence of loops.

theorem SetRel.IsIndependent.mono_left {X : Type u_1} {G H : SetRel X X} {A : Set X} (hHG : H ⊆ G) (h : G.IsIndependent A) : H.IsIndependent A

Independence passes to subrelations.

theorem SetRel.IsIndependent.mono_right {X : Type u_1} {G : SetRel X X} {A B : Set X} (hBA : B ⊆ A) (h : G.IsIndependent A) : G.IsIndependent B

Independence passes to subsets.

@[simp]

theorem SetRel.IsIndependent.empty {X : Type u_1} {G : SetRel X X} : G.IsIndependent ∅

The empty set is independent.

@[simp]

theorem SetRel.isIndependent_singleton {X : Type u_1} {G : SetRel X X} {x : X} : G.IsIndependent {x} ↔ (x, x) ∉ G

A singleton is independent iff its point carries no loop.

def SetRel.HasCountableBorelColoring {X : Type u_1} [MeasurableSpace X] (G : SetRel X X) : Prop

A relation G has a countable Borel coloring if some measurable c : X → ℕ gives the two ends of every pair of G different colors.

theorem SetRel.hasCountableBorelColoring_iff {X : Type u_1} {G : SetRel X X} [MeasurableSpace X] : G.HasCountableBorelColoring ↔ ∃ (c : X → ℕ), Measurable c ∧ ∀ ⦃x y : X⦄, (x, y) ∈ G → c x ≠ c y

Unfolding lemma for SetRel.HasCountableBorelColoring.

theorem SetRel.hasCountableBorelColoring_iff_exists_cover {X : Type u_1} {G : SetRel X X} [MeasurableSpace X] : G.HasCountableBorelColoring ↔ ∃ (B : ℕ → Set X), (∀ (n : ℕ), MeasurableSet (B n) ∧ G.IsIndependent (B n)) ∧ ⋃ (n : ℕ), B n = Set.univ

A relation has a countable Borel coloring iff the space is covered by countably many measurable independent sets.

theorem SetRel.HasCountableBorelColoring.mono {X : Type u_1} {G H : SetRel X X} [MeasurableSpace X] (hHG : H ⊆ G) (h : G.HasCountableBorelColoring) : H.HasCountableBorelColoring

A coloring of a relation colors every subrelation.

theorem SetRel.HasCountableBorelColoring.preimage {X : Type u_1} {Y : Type u_2} {G : SetRel X X} [MeasurableSpace X] [MeasurableSpace Y] (h : G.HasCountableBorelColoring) {f : Y → X} (hf : Measurable f) : HasCountableBorelColoring (Prod.map f f ⁻¹' G)

A coloring of a relation pulls back along a measurable map. Combined with SetRel.HasCountableBorelColoring.mono, a relation H with a measurable map f sending H-pairs to G-pairs inherits a coloring from one of G.

theorem SetRel.not_hasCountableBorelColoring_of_mem {X : Type u_1} {G : SetRel X X} [MeasurableSpace X] {x : X} (hx : (x, x) ∈ G) : ¬G.HasCountableBorelColoring

A relation with a loop has no coloring at all.

theorem SetRel.exists_measurableSet_isIndependent_superset {X : Type u_1} {G : SetRel X X} {A : Set X} [TopologicalSpace X] [T2Space X] [MeasurableSpace X] [BorelSpace X] (hG : MeasureTheory.AnalyticSet G) (hA : MeasureTheory.AnalyticSet A) (hind : G.IsIndependent A) : ∃ (B : Set X), MeasurableSet B ∧ A ⊆ B ∧ G.IsIndependent B

The Kechris–Solecki–Todorcevic lemma. In a Hausdorff space with its Borel σ-algebra, an analytic independent set of an analytic relation is contained in a Borel independent set.

@[simp]

theorem SimpleGraph.isIndependent_adj_iff_isIndepSet {V : Type u_1} (G : SimpleGraph V) {s : Set V} : SetRel.IsIndependent {p : V × V | G.Adj p.1 p.2} s ↔ G.IsIndepSet s

Independence for the edge relation of a simple graph is Mathlib's SimpleGraph.IsIndepSet.

theorem SimpleGraph.hasCountableBorelColoring_adj_iff {V : Type u_1} (G : SimpleGraph V) [MeasurableSpace V] : SetRel.HasCountableBorelColoring {p : V × V | G.Adj p.1 p.2} ↔ ∃ (c : G.Coloring ℕ), Measurable ⇑c

The edge relation of a simple graph has a countable Borel coloring iff the graph has a measurable coloring by ℕ.

theorem Setoid.countable_quotient_of_hasCountableBorelColoring_not {X : Type u_1} [MeasurableSpace X] (E : Setoid X) (h : SetRel.HasCountableBorelColoring {p : X × X | ¬E p.1 p.2}) : Countable (Quotient E)

If the inequivalence relation of E has a countable Borel coloring, then E has countably many classes: two points of the same color are equivalent.

theorem Setoid.measurableSet_setOf_of_hasCountableBorelColoring_not {X : Type u_1} [MeasurableSpace X] (E : Setoid X) (h : SetRel.HasCountableBorelColoring {p : X × X | ¬E p.1 p.2}) (x : X) : MeasurableSet {y : X | E x y}

If the inequivalence relation of E has a countable Borel coloring, then every class of E is measurable: it is the union of the color classes of its points.

theorem Setoid.hasCountableBorelColoring_not_of_countable {X : Type u_1} [MeasurableSpace X] {E : Setoid X} [Countable (Quotient E)] (hE : ∀ (x : X), MeasurableSet {y : X | E x y}) : SetRel.HasCountableBorelColoring {p : X × X | ¬E p.1 p.2}

For an equivalence relation E with measurable classes and countably many of them, the inequivalence relation of E has a countable Borel coloring: color each point by an index of its class.

theorem Setoid.hasCountableBorelColoring_not_iff {X : Type u_1} [MeasurableSpace X] {E : Setoid X} : SetRel.HasCountableBorelColoring {p : X × X | ¬E p.1 p.2} ↔ Countable (Quotient E) ∧ ∀ (x : X), MeasurableSet {y : X | E x y}

Countable colorings count classes. The inequivalence relation of an equivalence relation E has a countable Borel coloring iff E has countably many classes, all of them measurable.