Extending witnesses in analytic families of assignments

Let g : (ℕ → ℕ) → X × X be continuous. A word w witnesses a tracked pair of coordinates of an assignment φ : ι → X when that pair belongs to g '' PiNat.wordCylinder w. For an analytic family that is not small, finitely many such words can be extended simultaneously while retaining an analytic subfamily that is not small.

SetRel.exists_subset_not_isSmallFamily_witness_append extends every tracked word by one letter. SetRel.exists_subset_not_isSmallFamily_witness_extension extends them by any specified number of letters. These refinements keep witnesses coherent in fusion constructions of continuous graph homomorphisms: repeated extensions determine a point of Baire space, and continuity of g then identifies the limiting edge.

The relation defining smallness need not equal the range of g; in applications g parametrizes that relation. Neither the index type of assignments nor the space of assignments needs to be countable or Polish. Analyticity is retained by taking continuous preimages inside the original analytic family.

References

• B. D. Miller, The graph-theoretic approach to descriptive set theory, Bulletin of Symbolic Logic 18 (2012), 554–575, the witness refinement in the proof of the G₀ dichotomy.

theorem SetRel.exists_subset_not_isSmallFamily_witness_append {X : Type u_1} {ι : Type u_2} {κ : Type u_3} [TopologicalSpace X] [T2Space X] [MeasurableSpace X] {G : SetRel X X} {Φ : Set (ι → X)} [Finite κ] {g : (ℕ → ℕ) → X × X} {e : κ → ι × ι} {w : κ → List ℕ} (hg : Continuous g) (hΦa : MeasureTheory.AnalyticSet Φ) (hΦ : ¬G.IsSmallFamily Φ) (hw : ∀ φ ∈ Φ, ∀ (k : κ), (φ (e k).1, φ (e k).2) ∈ g '' PiNat.wordCylinder (w k)) : ∃ (c : κ → ℕ), ∃ Ψ ⊆ Φ, MeasureTheory.AnalyticSet Ψ ∧ ¬G.IsSmallFamily Ψ ∧ ∀ φ ∈ Ψ, ∀ (k : κ), (φ (e k).1, φ (e k).2) ∈ g '' PiNat.wordCylinder (w k ++ [c k])

Finitely many tracked witness words can each be extended by one letter, on an analytic subfamily that is still not small. The new letter for each pair is uniform over that subfamily.

theorem SetRel.exists_subset_not_isSmallFamily_witness_extension {X : Type u_1} {ι : Type u_2} {κ : Type u_3} [TopologicalSpace X] [T2Space X] [MeasurableSpace X] {G : SetRel X X} {Φ : Set (ι → X)} [Finite κ] {g : (ℕ → ℕ) → X × X} {e : κ → ι × ι} {w : κ → List ℕ} (hg : Continuous g) (hΦa : MeasureTheory.AnalyticSet Φ) (hΦ : ¬G.IsSmallFamily Φ) (hw : ∀ φ ∈ Φ, ∀ (k : κ), (φ (e k).1, φ (e k).2) ∈ g '' PiNat.wordCylinder (w k)) (n : ℕ) : ∃ (v : κ → List ℕ), (∀ (k : κ), w k <+: v k) ∧ (∀ (k : κ), (v k).length = (w k).length + n) ∧ ∃ Ψ ⊆ Φ, MeasureTheory.AnalyticSet Ψ ∧ ¬G.IsSmallFamily Ψ ∧ ∀ φ ∈ Ψ, ∀ (k : κ), (φ (e k).1, φ (e k).2) ∈ g '' PiNat.wordCylinder (v k)

Extend every word witnessing one of finitely many tracked coordinate pairs by exactly n letters, retaining analyticity and non-smallness. The new words extend the old ones, not merely their lengths.