Miller's ideal of small families of assignments

Fix a relation G : SetRel X X on a measurable space X, read as a directed graph in which loops are allowed. An assignment is a map φ : ι → X, which labels the points of an index type ι (in applications, the vertices of a finite approximation to a graph homomorphism) by points of X. A family Φ : Set (ι → X) of assignments is small (SetRel.IsSmallFamily G Φ) if countably many measurable G-independent sets capture a value of every member of Φ: some B : ℕ → Set X of measurable independent sets has, for each φ ∈ Φ, some i and n with φ i ∈ B n.

The small families form a σ-ideal (SetRel.isSmallFamily_iUnion), so a family that is not small and is covered by countably many pieces has a piece that is not small (SetRel.exists_not_isSmallFamily_inter). For nonempty ι the family of all assignments is small exactly when G has a countable Borel coloring (SetRel.isSmallFamily_univ_iff). This is the ideal through which B. D. Miller proves the Kechris–Solecki–Todorcevic G₀ dichotomy: starting from the family of all assignments, which is not small when G has no countable Borel coloring, one refines and amalgamates families while keeping them analytic and not small, and reads a continuous homomorphism from the graph G₀ into G off the limit of the construction.

The steps of that construction are the following statements.

• Amalgamation. Let comb : (ι → X) → (ι → X) → κ → X take only values of its arguments. If Φ is not small, neither is the family Set.image2 comb Φ Φ of combinations of its members (SetRel.not_isSmallFamily_image2). If moreover ι is countable and X is a Hausdorff space with its Borel σ-algebra, and Φ and G are analytic, then neither is the family of combinations of pairs φ₀, φ₁ ∈ Φ joined by an edge (φ₀ s, φ₁ s) ∈ G at a designated index s (SetRel.not_isSmallFamily_comb_cross). This is where the Kechris–Solecki–Todorcevic lemma SetRel.exists_measurableSet_isIndependent_superset enters. When comb is jointly continuous both combined families are analytic (MeasureTheory.AnalyticSet.image2, SetRel.analyticSet_comb_cross).
• Vertex shrinking. For finite ι, a family that is not small has, for any countable cover of X, a subfamily that is not small whose members take each coordinate in one prescribed piece of the cover (SetRel.exists_not_isSmallFamily_inter_pi). In a separable pseudometric space this gives, for every ε > 0 and if the original family is analytic, an analytic subfamily that is not small and whose members are uniformly within ε of each other at every coordinate (SetRel.exists_subset_not_isSmallFamily_dist_lt).

Main definitions

• SetRel.IsSmallFamily G Φ: countably many measurable G-independent sets capture a value of every member of Φ.

Main results

• SetRel.isSmallFamily_iff_exists_countable: smallness through a countable set of capturing sets.
• SetRel.isSmallFamily_iUnion: small families form a σ-ideal.
• SetRel.isSmallFamily_univ_iff: for nonempty ι, all assignments form a small family iff G has a countable Borel coloring.
• SetRel.IsSmallFamily.of_exists_range_subset: smallness transfers back along families each of whose members takes all the values of some member of the original family.
• SetRel.not_isSmallFamily_image2, SetRel.not_isSmallFamily_comb_cross: amalgamation keeps families from being small.
• SetRel.exists_not_isSmallFamily_inter_pi, SetRel.exists_subset_not_isSmallFamily_dist_lt: vertex shrinking.

References

• 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 this ideal.
• A. S. Kechris, S. Solecki and S. Todorcevic, Borel chromatic numbers, Advances in Mathematics 141 (1999), 1–44: the G₀ dichotomy and the independent-superset lemma.
• SetRel.IsSmallFamily corresponds to SmallFam in InfinitaryLogic/Descriptive/G0Dichotomy.lean and InfinitaryLogic/Descriptive/G0Fusion.lean of cameronfreer/infinitary-logic (Apache-2.0), commit 518a366cba97b1ae8c4dc64a297a396939bc3e0b. Here the ideal is stated for an arbitrary relation on a measurable space, and the amalgamation statements for any combination map whose values are values of its arguments.

def SetRel.IsSmallFamily {X : Type u_1} {ι : Type u_2} [MeasurableSpace X] (G : SetRel X X) (Φ : Set (ι → X)) : Prop

A family Φ of assignments ι → X is small for a relation G if countably many measurable G-independent sets capture a value of every member of Φ.

theorem SetRel.isSmallFamily_iff {X : Type u_1} {ι : Type u_2} [MeasurableSpace X] {G : SetRel X X} {Φ : Set (ι → X)} : G.IsSmallFamily Φ ↔ ∃ (B : ℕ → Set X), (∀ (n : ℕ), MeasurableSet (B n) ∧ G.IsIndependent (B n)) ∧ ∀ φ ∈ Φ, ∃ (i : ι) (n : ℕ), φ i ∈ B n

Unfolding lemma for SetRel.IsSmallFamily.

theorem SetRel.isSmallFamily_iff_exists_countable {X : Type u_1} {ι : Type u_2} [MeasurableSpace X] {G : SetRel X X} {Φ : Set (ι → X)} : G.IsSmallFamily Φ ↔ ∃ (𝒞 : Set (Set X)), 𝒞.Countable ∧ (∀ C ∈ 𝒞, MeasurableSet C ∧ G.IsIndependent C) ∧ ∀ φ ∈ Φ, ∃ (i : ι), ∃ C ∈ 𝒞, φ i ∈ C

A family is small iff some countable set of measurable independent sets captures a value of every member.

theorem SetRel.IsSmallFamily.mono_left {X : Type u_1} {ι : Type u_2} [MeasurableSpace X] {G H : SetRel X X} {Φ : Set (ι → X)} (hHG : H ⊆ G) (h : G.IsSmallFamily Φ) : H.IsSmallFamily Φ

Smallness for a relation passes to its subrelations.

theorem SetRel.IsSmallFamily.mono_right {X : Type u_1} {ι : Type u_2} [MeasurableSpace X] {G : SetRel X X} {Φ Ψ : Set (ι → X)} (hΨΦ : Ψ ⊆ Φ) (h : G.IsSmallFamily Φ) : G.IsSmallFamily Ψ

Smallness passes to subfamilies.

@[simp]

theorem SetRel.isSmallFamily_empty {X : Type u_1} {ι : Type u_2} [MeasurableSpace X] {G : SetRel X X} : G.IsSmallFamily ∅

The empty family is small.

@[simp]

theorem SetRel.isSmallFamily_iUnion {X : Type u_1} {ι : Type u_2} {κ : Type u_3} [MeasurableSpace X] {G : SetRel X X} [Countable κ] {Φ : κ → Set (ι → X)} : G.IsSmallFamily (⋃ (k : κ), Φ k) ↔ ∀ (k : κ), G.IsSmallFamily (Φ k)

Small families form a σ-ideal. A countable union of families is small iff each of them is.

@[simp]

theorem SetRel.isSmallFamily_union {X : Type u_1} {ι : Type u_2} [MeasurableSpace X] {G : SetRel X X} {Φ Ψ : Set (ι → X)} : G.IsSmallFamily (Φ ∪ Ψ) ↔ G.IsSmallFamily Φ ∧ G.IsSmallFamily Ψ

A union of two families is small iff both are.

theorem SetRel.exists_not_isSmallFamily_inter {X : Type u_1} {ι : Type u_2} {κ : Type u_3} [MeasurableSpace X] {G : SetRel X X} {Φ : Set (ι → X)} [Countable κ] {Ψ : κ → Set (ι → X)} (hΦ : ¬G.IsSmallFamily Φ) (hcov : Φ ⊆ ⋃ (k : κ), Ψ k) : ∃ (k : κ), ¬G.IsSmallFamily (Φ ∩ Ψ k)

Pigeonhole for small families. If a family that is not small is covered by countably many families, its intersection with one of them is not small.

theorem SetRel.nonempty_of_not_isSmallFamily {X : Type u_1} {ι : Type u_2} [MeasurableSpace X] {G : SetRel X X} {Φ : Set (ι → X)} (hΦ : ¬G.IsSmallFamily Φ) : Φ.Nonempty

A family that is not small is nonempty.

theorem SetRel.isSmallFamily_univ_iff {X : Type u_1} {ι : Type u_2} [MeasurableSpace X] {G : SetRel X X} [Nonempty ι] : G.IsSmallFamily Set.univ ↔ G.HasCountableBorelColoring

The seed of the G₀ construction. For nonempty ι, the family of all assignments is small iff the relation has a countable Borel coloring.

theorem SetRel.IsSmallFamily.of_exists_range_subset {X : Type u_1} {ι : Type u_2} {κ : Type u_3} [MeasurableSpace X] {G : SetRel X X} {Φ : Set (ι → X)} {Ψ : Set (κ → X)} (hΨ : G.IsSmallFamily Ψ) (h : ∀ φ ∈ Φ, ∃ ψ ∈ Ψ, Set.range ψ ⊆ Set.range φ) : G.IsSmallFamily Φ

Smallness transfers back along value inclusion: if Ψ is small and every member of Φ has all values of some member of Ψ among its own values, then Φ is small.

theorem SetRel.not_isSmallFamily_image2 {X : Type u_1} {ι : Type u_2} {κ : Type u_3} [MeasurableSpace X] {G : SetRel X X} {Φ : Set (ι → X)} (hΦ : ¬G.IsSmallFamily Φ) {comb : (ι → X) → (ι → X) → κ → X} (hcomb : ∀ (φ : ι → X), Set.range (comb φ φ) ⊆ Set.range φ) : ¬G.IsSmallFamily (Set.image2 comb Φ Φ)

Amalgamation keeps families from being small. If Φ is not small and comb φ φ takes only values of φ, then the family of combinations comb φ₀ φ₁ of members of Φ is not small.

theorem SetRel.not_isSmallFamily_comb_cross {X : Type u_1} {ι : Type u_2} {κ : Type u_3} [MeasurableSpace X] {G : SetRel X X} {Φ : Set (ι → X)} [TopologicalSpace X] [T2Space X] [BorelSpace X] [Countable ι] (hG : MeasureTheory.AnalyticSet G) (hΦa : MeasureTheory.AnalyticSet Φ) (hΦ : ¬G.IsSmallFamily Φ) (s : ι) {comb : (ι → X) → (ι → X) → κ → X} (hcomb : ∀ (φ₀ φ₁ : ι → X), Set.range (comb φ₀ φ₁) ⊆ Set.range φ₀ ∪ Set.range φ₁) : ¬G.IsSmallFamily {ψ : κ → X | ∃ φ₀ ∈ Φ, ∃ φ₁ ∈ Φ, (φ₀ s, φ₁ s) ∈ G ∧ comb φ₀ φ₁ = ψ}

Amalgamation across a fresh edge keeps analytic families from being small. Let X be a Hausdorff space with its Borel σ-algebra, G an analytic relation, ι countable, and Φ an analytic family that is not small. If comb φ₀ φ₁ takes only values of φ₀ and φ₁, then for every index s the family of combinations comb φ₀ φ₁ of members φ₀, φ₁ ∈ Φ with (φ₀ s, φ₁ s) ∈ G is not small.

theorem SetRel.analyticSet_comb_cross {X : Type u_1} {ι : Type u_2} {κ : Type u_3} {G : SetRel X X} {Φ : Set (ι → X)} [TopologicalSpace X] [T2Space X] (hG : MeasureTheory.AnalyticSet G) (hΦ : MeasureTheory.AnalyticSet Φ) (s : ι) {comb : (ι → X) → (ι → X) → κ → X} (hcomb : Continuous (Function.uncurry comb)) : MeasureTheory.AnalyticSet {ψ : κ → X | ∃ φ₀ ∈ Φ, ∃ φ₁ ∈ Φ, (φ₀ s, φ₁ s) ∈ G ∧ comb φ₀ φ₁ = ψ}

For a jointly continuous combination map and an analytic relation on a Hausdorff space, the combinations of pairs of members of an analytic family joined by an edge at a designated index form an analytic family.

theorem SetRel.exists_not_isSmallFamily_inter_pi {X : Type u_1} {ι : Type u_2} {κ : Type u_3} [MeasurableSpace X] {G : SetRel X X} {Φ : Set (ι → X)} [Finite ι] [Countable κ] {U : κ → Set X} (hU : ⋃ (k : κ), U k = Set.univ) (hΦ : ¬G.IsSmallFamily Φ) : ∃ (c : ι → κ), ¬G.IsSmallFamily (Φ ∩ Set.univ.pi fun (i : ι) => U (c i))

Vertex shrinking. For finite ι and a countable cover U of X, a family that is not small has a subfamily that is not small whose members take each coordinate i in one piece U (c i).

theorem SetRel.exists_subset_not_isSmallFamily_dist_lt {X : Type u_1} {ι : Type u_2} [MeasurableSpace X] {G : SetRel X X} {Φ : Set (ι → X)} [PseudoMetricSpace X] [TopologicalSpace.SeparableSpace X] [Finite ι] (hΦa : MeasureTheory.AnalyticSet Φ) (hΦ : ¬G.IsSmallFamily Φ) {ε : ℝ} (hε : 0 < ε) : ∃ Ψ ⊆ Φ, MeasureTheory.AnalyticSet Ψ ∧ ¬G.IsSmallFamily Ψ ∧ ∀ φ ∈ Ψ, ∀ ψ ∈ Ψ, ∀ (i : ι), dist (φ i) (ψ i) < ε

Vertex shrinking in a metric. In a separable pseudometric space, for finite ι and ε > 0, an analytic family that is not small has an analytic subfamily that is not small and whose members are within ε of each other at every coordinate.