Invariant analytic separation

An analytic set disjoint from an invariant analytic set can be separated from it by an invariant Borel set (invariant_analytic_separation). The proof iterates ordinary Lusin separation (AnalyticSet.measurablySeparable) with the saturation of the separator under the permutation action: each saturation is analytic (the action is continuous) and still disjoint from the invariant excluded set, so it can be separated again; the union of the ω stages is Borel and invariant. No Borelness of the isomorphism relation is used.

Composed with López–Escobar (lopez_escobar), the invariant separator is the model class of one L_{ω₁ω}-sentence: sentence_separates_analytic_classes.

Classical background

The separation argument is the same iterative separation-and-saturation construction as Gao, Invariant Descriptive Set Theory (CRC Press, 2009), Lemma 5.4.6, specialized to the isomorphism action. Marker, Lectures on Infinitary Model Theory (Cambridge, 2016), Corollary 4.3.6 and Theorem 4.3.7, gives the invariant-separation and López–Escobar background through interpolation (Corollary 4.24 and Theorem 4.25 in the Fall 2013 lecture notes).

def FirstOrder.Language.saturation {L : Language} (A : Set L.StructureSpace) : Set L.StructureSpace

The saturation of a set of structures under the permutation action.

Equations

• FirstOrder.Language.saturation A = (fun (p : Equiv.Perm ℕ × L.StructureSpace) => p.1 • p.2) '' Set.univ ×ˢ A

theorem FirstOrder.Language.mem_saturation {L : Language} {A : Set L.StructureSpace} {y : L.StructureSpace} : y ∈ saturation A ↔ ∃ (σ : Equiv.Perm ℕ), ∃ x ∈ A, σ • x = y

theorem FirstOrder.Language.subset_saturation {L : Language} (A : Set L.StructureSpace) : A ⊆ saturation A

theorem FirstOrder.Language.analyticSet_saturation {L : Language} [Countable ((n : ℕ) × L.Relations n)] {A : Set L.StructureSpace} (hA : MeasureTheory.AnalyticSet A) : MeasureTheory.AnalyticSet (saturation A)

The saturation of an analytic set is analytic: the action is continuous.

theorem FirstOrder.Language.saturation_invariant {L : Language} (A : Set L.StructureSpace) : ActionInvariant (saturation A)

theorem FirstOrder.Language.disjoint_saturation {L : Language} {A B : Set L.StructureSpace} (hB : ActionInvariant B) (hd : Disjoint B A) : Disjoint B (saturation A)

theorem FirstOrder.Language.invariant_analytic_separation {L : Language} [Countable ((n : ℕ) × L.Relations n)] {A B : Set L.StructureSpace} (hA : MeasureTheory.AnalyticSet A) (hB : MeasureTheory.AnalyticSet B) (hinv : ActionInvariant B) (hd : Disjoint A B) : ∃ (C : Set L.StructureSpace), A ⊆ C ∧ Disjoint B C ∧ MeasurableSet C ∧ ActionInvariant C

Invariant analytic separation. An analytic set disjoint from an invariant analytic set is contained in an invariant Borel set disjoint from it. Iterated saturation; no Borel isomorphism relation is used.

theorem FirstOrder.Language.sentence_separates_analytic_classes {L : Language} [L.IsRelational] [Countable ((n : ℕ) × L.Relations n)] {A B : Set L.StructureSpace} (hA : MeasureTheory.AnalyticSet A) (hB : MeasureTheory.AnalyticSet B) (hinv : ActionInvariant B) (hd : Disjoint A B) : ∃ (θ : L.Sentenceω), A ⊆ ModelsOf θ ∧ Disjoint B (ModelsOf θ)

A sentence separates an analytic class from a disjoint invariant analytic class, by López–Escobar applied to the invariant separator.