Definable Sets

This file defines what it means for a set over a first-order structure to be definable.

Main Definitions

• Set.Definable is defined so that A.Definable L s indicates that the set s of a finite cartesian power of M is definable with parameters in A.
• Set.Definable₁ is defined so that A.Definable₁ L s indicates that (s : Set M) is definable with parameters in A.
• Set.Definable₂ is defined so that A.Definable₂ L s indicates that (s : Set (M × M)) is definable with parameters in A.
• A FirstOrder.Language.DefinableSet is defined so that L.DefinableSet A α is the boolean algebra of subsets of α → M defined by formulas with parameters in A.

Main Results

• L.DefinableSet A α forms a BooleanAlgebra
• Set.Definable.image_comp shows that definability is closed under projections in finite dimensions.

def Set.Definable {M : Type w} (A : Set M) (L : FirstOrder.Language) [FirstOrder.Language.Structure L M] {α : Type u₁} (s : Set (α → M)) : Prop

A subset of a finite Cartesian product of a structure is definable over a set A when membership in the set is given by a first-order formula with parameters from A.

theorem Set.Definable.map_expansion {M : Type w} {A : Set M} {L : FirstOrder.Language} [FirstOrder.Language.Structure L M] {α : Type u₁} {s : Set (α → M)} {L' : FirstOrder.Language} [FirstOrder.Language.Structure L' M] (h : Set.Definable A L s) (φ : L →ᴸ L') [FirstOrder.Language.LHom.IsExpansionOn φ M] : Set.Definable A L' s

theorem Set.definable_iff_exists_formula_sum {M : Type w} {A : Set M} {L : FirstOrder.Language} [FirstOrder.Language.Structure L M] {α : Type u₁} {s : Set (α → M)} : Set.Definable A L s ↔ ∃ φ, s = {v | FirstOrder.Language.Formula.Realize φ (Sum.elim Subtype.val v)}

theorem Set.empty_definable_iff {M : Type w} {L : FirstOrder.Language} [FirstOrder.Language.Structure L M] {α : Type u₁} {s : Set (α → M)} : Set.Definable ∅ L s ↔ ∃ φ, s = setOf (FirstOrder.Language.Formula.Realize φ)

theorem Set.definable_iff_empty_definable_with_params {M : Type w} {A : Set M} {L : FirstOrder.Language} [FirstOrder.Language.Structure L M] {α : Type u₁} {s : Set (α → M)} : Set.Definable A L s ↔ Set.Definable ∅ (FirstOrder.Language.withConstants L ↑A) s

theorem Set.Definable.mono {M : Type w} {A : Set M} {L : FirstOrder.Language} [FirstOrder.Language.Structure L M] {α : Type u₁} {B : Set M} {s : Set (α → M)} (hAs : Set.Definable A L s) (hAB : A ⊆ B) : Set.Definable B L s

@[simp]

theorem Set.definable_empty {M : Type w} {A : Set M} {L : FirstOrder.Language} [FirstOrder.Language.Structure L M] {α : Type u₁} : Set.Definable A L ∅

@[simp]

theorem Set.definable_univ {M : Type w} {A : Set M} {L : FirstOrder.Language} [FirstOrder.Language.Structure L M] {α : Type u₁} : Set.Definable A L Set.univ

@[simp]

theorem Set.Definable.inter {M : Type w} {A : Set M} {L : FirstOrder.Language} [FirstOrder.Language.Structure L M] {α : Type u₁} {f : Set (α → M)} {g : Set (α → M)} (hf : Set.Definable A L f) (hg : Set.Definable A L g) : Set.Definable A L (f ∩ g)

@[simp]

theorem Set.Definable.union {M : Type w} {A : Set M} {L : FirstOrder.Language} [FirstOrder.Language.Structure L M] {α : Type u₁} {f : Set (α → M)} {g : Set (α → M)} (hf : Set.Definable A L f) (hg : Set.Definable A L g) : Set.Definable A L (f ∪ g)

theorem Set.definable_finset_inf {M : Type w} {A : Set M} {L : FirstOrder.Language} [FirstOrder.Language.Structure L M] {α : Type u₁} {ι : Type u_2} {f : ι → Set (α → M)} (hf : ∀ (i : ι), Set.Definable A L (f i)) (s : Finset ι) : Set.Definable A L (Finset.inf s f)

theorem Set.definable_finset_sup {M : Type w} {A : Set M} {L : FirstOrder.Language} [FirstOrder.Language.Structure L M] {α : Type u₁} {ι : Type u_2} {f : ι → Set (α → M)} (hf : ∀ (i : ι), Set.Definable A L (f i)) (s : Finset ι) : Set.Definable A L (Finset.sup s f)

theorem Set.definable_finset_biInter {M : Type w} {A : Set M} {L : FirstOrder.Language} [FirstOrder.Language.Structure L M] {α : Type u₁} {ι : Type u_2} {f : ι → Set (α → M)} (hf : ∀ (i : ι), Set.Definable A L (f i)) (s : Finset ι) : Set.Definable A L (⋂ (i : ι) (_ : i ∈ s), f i)

theorem Set.definable_finset_biUnion {M : Type w} {A : Set M} {L : FirstOrder.Language} [FirstOrder.Language.Structure L M] {α : Type u₁} {ι : Type u_2} {f : ι → Set (α → M)} (hf : ∀ (i : ι), Set.Definable A L (f i)) (s : Finset ι) : Set.Definable A L (⋃ (i : ι) (_ : i ∈ s), f i)

@[simp]

theorem Set.Definable.compl {M : Type w} {A : Set M} {L : FirstOrder.Language} [FirstOrder.Language.Structure L M] {α : Type u₁} {s : Set (α → M)} (hf : Set.Definable A L s) : Set.Definable A L sᶜ

@[simp]

theorem Set.Definable.sdiff {M : Type w} {A : Set M} {L : FirstOrder.Language} [FirstOrder.Language.Structure L M] {α : Type u₁} {s : Set (α → M)} {t : Set (α → M)} (hs : Set.Definable A L s) (ht : Set.Definable A L t) : Set.Definable A L (s \ t)

theorem Set.Definable.preimage_comp {M : Type w} {A : Set M} {L : FirstOrder.Language} [FirstOrder.Language.Structure L M] {α : Type u₁} {β : Type u_1} (f : α → β) {s : Set (α → M)} (h : Set.Definable A L s) : Set.Definable A L ((fun g => g ∘ f) ⁻¹' s)

theorem Set.Definable.image_comp_equiv {M : Type w} {A : Set M} {L : FirstOrder.Language} [FirstOrder.Language.Structure L M] {α : Type u₁} {β : Type u_1} {s : Set (β → M)} (h : Set.Definable A L s) (f : α ≃ β) : Set.Definable A L ((fun g => g ∘ ↑f) '' s)

theorem Set.definable_iff_finitely_definable {M : Type w} {A : Set M} {L : FirstOrder.Language} [FirstOrder.Language.Structure L M] {α : Type u₁} {s : Set (α → M)} : Set.Definable A L s ↔ ∃ A0, ↑A0 ⊆ A ∧ Set.Definable (↑A0) L s

theorem Set.Definable.image_comp_sum_inl_fin {M : Type w} {A : Set M} {L : FirstOrder.Language} [FirstOrder.Language.Structure L M] {α : Type u₁} (m : ℕ) {s : Set (α ⊕ Fin m → M)} (h : Set.Definable A L s) : Set.Definable A L ((fun g => g ∘ Sum.inl) '' s)

This lemma is only intended as a helper for Definable.image_comp.

theorem Set.Definable.image_comp_embedding {M : Type w} {A : Set M} {L : FirstOrder.Language} [FirstOrder.Language.Structure L M] {α : Type u₁} {β : Type u_1} {s : Set (β → M)} (h : Set.Definable A L s) (f : α ↪ β) [Finite β] : Set.Definable A L ((fun g => g ∘ ↑f) '' s)

Shows that definability is closed under finite projections.

theorem Set.Definable.image_comp {M : Type w} {A : Set M} {L : FirstOrder.Language} [FirstOrder.Language.Structure L M] {α : Type u₁} {β : Type u_1} {s : Set (β → M)} (h : Set.Definable A L s) (f : α → β) [Finite α] [Finite β] : Set.Definable A L ((fun g => g ∘ f) '' s)

Shows that definability is closed under finite projections.

def Set.Definable₁ {M : Type w} (A : Set M) (L : FirstOrder.Language) [FirstOrder.Language.Structure L M] (s : Set M) : Prop

A 1-dimensional version of Definable, for Set M.

def Set.Definable₂ {M : Type w} (A : Set M) (L : FirstOrder.Language) [FirstOrder.Language.Structure L M] (s : Set (M × M)) : Prop

A 2-dimensional version of Definable, for Set (M × M).

def FirstOrder.Language.DefinableSet (L : FirstOrder.Language) {M : Type w} [FirstOrder.Language.Structure L M] (A : Set M) (α : Type u₁) : Type (max 0 u₁ w)

Definable sets are subsets of finite Cartesian products of a structure such that membership is given by a first-order formula.

instance FirstOrder.Language.DefinableSet.instSetLike {L : FirstOrder.Language} {M : Type w} [FirstOrder.Language.Structure L M] {A : Set M} {α : Type u₁} : SetLike (FirstOrder.Language.DefinableSet L A α) (α → M)

instance FirstOrder.Language.DefinableSet.instTop {L : FirstOrder.Language} {M : Type w} [FirstOrder.Language.Structure L M] {A : Set M} {α : Type u₁} : Top (FirstOrder.Language.DefinableSet L A α)

instance FirstOrder.Language.DefinableSet.instBot {L : FirstOrder.Language} {M : Type w} [FirstOrder.Language.Structure L M] {A : Set M} {α : Type u₁} : Bot (FirstOrder.Language.DefinableSet L A α)

instance FirstOrder.Language.DefinableSet.instSup {L : FirstOrder.Language} {M : Type w} [FirstOrder.Language.Structure L M] {A : Set M} {α : Type u₁} : Sup (FirstOrder.Language.DefinableSet L A α)

instance FirstOrder.Language.DefinableSet.instInf {L : FirstOrder.Language} {M : Type w} [FirstOrder.Language.Structure L M] {A : Set M} {α : Type u₁} : Inf (FirstOrder.Language.DefinableSet L A α)

instance FirstOrder.Language.DefinableSet.instHasCompl {L : FirstOrder.Language} {M : Type w} [FirstOrder.Language.Structure L M] {A : Set M} {α : Type u₁} : HasCompl (FirstOrder.Language.DefinableSet L A α)

instance FirstOrder.Language.DefinableSet.instSDiff {L : FirstOrder.Language} {M : Type w} [FirstOrder.Language.Structure L M] {A : Set M} {α : Type u₁} : SDiff (FirstOrder.Language.DefinableSet L A α)

instance FirstOrder.Language.DefinableSet.instInhabited {L : FirstOrder.Language} {M : Type w} [FirstOrder.Language.Structure L M] {A : Set M} {α : Type u₁} : Inhabited (FirstOrder.Language.DefinableSet L A α)

theorem FirstOrder.Language.DefinableSet.le_iff {L : FirstOrder.Language} {M : Type w} [FirstOrder.Language.Structure L M] {A : Set M} {α : Type u₁} {s : FirstOrder.Language.DefinableSet L A α} {t : FirstOrder.Language.DefinableSet L A α} : s ≤ t ↔ ↑s ≤ ↑t

@[simp]

theorem FirstOrder.Language.DefinableSet.mem_top {L : FirstOrder.Language} {M : Type w} [FirstOrder.Language.Structure L M] {A : Set M} {α : Type u₁} {x : α → M} : x ∈ ⊤

@[simp]

theorem FirstOrder.Language.DefinableSet.not_mem_bot {L : FirstOrder.Language} {M : Type w} [FirstOrder.Language.Structure L M] {A : Set M} {α : Type u₁} {x : α → M} : ¬x ∈ ⊥

@[simp]

theorem FirstOrder.Language.DefinableSet.mem_sup {L : FirstOrder.Language} {M : Type w} [FirstOrder.Language.Structure L M] {A : Set M} {α : Type u₁} {s : FirstOrder.Language.DefinableSet L A α} {t : FirstOrder.Language.DefinableSet L A α} {x : α → M} : x ∈ s ⊔ t ↔ x ∈ s ∨ x ∈ t

@[simp]

theorem FirstOrder.Language.DefinableSet.mem_inf {L : FirstOrder.Language} {M : Type w} [FirstOrder.Language.Structure L M] {A : Set M} {α : Type u₁} {s : FirstOrder.Language.DefinableSet L A α} {t : FirstOrder.Language.DefinableSet L A α} {x : α → M} : x ∈ s ⊓ t ↔ x ∈ s ∧ x ∈ t

@[simp]

theorem FirstOrder.Language.DefinableSet.mem_compl {L : FirstOrder.Language} {M : Type w} [FirstOrder.Language.Structure L M] {A : Set M} {α : Type u₁} {s : FirstOrder.Language.DefinableSet L A α} {x : α → M} : x ∈ sᶜ ↔ ¬x ∈ s

@[simp]

theorem FirstOrder.Language.DefinableSet.mem_sdiff {L : FirstOrder.Language} {M : Type w} [FirstOrder.Language.Structure L M] {A : Set M} {α : Type u₁} {s : FirstOrder.Language.DefinableSet L A α} {t : FirstOrder.Language.DefinableSet L A α} {x : α → M} : x ∈ s \ t ↔ x ∈ s ∧ ¬x ∈ t

@[simp]

theorem FirstOrder.Language.DefinableSet.coe_top {L : FirstOrder.Language} {M : Type w} [FirstOrder.Language.Structure L M] {A : Set M} {α : Type u₁} : ↑⊤ = Set.univ

@[simp]

theorem FirstOrder.Language.DefinableSet.coe_bot {L : FirstOrder.Language} {M : Type w} [FirstOrder.Language.Structure L M] {A : Set M} {α : Type u₁} : ↑⊥ = ∅

@[simp]

theorem FirstOrder.Language.DefinableSet.coe_sup {L : FirstOrder.Language} {M : Type w} [FirstOrder.Language.Structure L M] {A : Set M} {α : Type u₁} (s : FirstOrder.Language.DefinableSet L A α) (t : FirstOrder.Language.DefinableSet L A α) : ↑(s ⊔ t) = ↑s ∪ ↑t

@[simp]

theorem FirstOrder.Language.DefinableSet.coe_inf {L : FirstOrder.Language} {M : Type w} [FirstOrder.Language.Structure L M] {A : Set M} {α : Type u₁} (s : FirstOrder.Language.DefinableSet L A α) (t : FirstOrder.Language.DefinableSet L A α) : ↑(s ⊓ t) = ↑s ∩ ↑t

@[simp]

theorem FirstOrder.Language.DefinableSet.coe_compl {L : FirstOrder.Language} {M : Type w} [FirstOrder.Language.Structure L M] {A : Set M} {α : Type u₁} (s : FirstOrder.Language.DefinableSet L A α) : ↑sᶜ = (↑s)ᶜ

@[simp]

theorem FirstOrder.Language.DefinableSet.coe_sdiff {L : FirstOrder.Language} {M : Type w} [FirstOrder.Language.Structure L M] {A : Set M} {α : Type u₁} (s : FirstOrder.Language.DefinableSet L A α) (t : FirstOrder.Language.DefinableSet L A α) : ↑(s \ t) = ↑s \ ↑t

instance FirstOrder.Language.DefinableSet.instBooleanAlgebra {L : FirstOrder.Language} {M : Type w} [FirstOrder.Language.Structure L M] {A : Set M} {α : Type u₁} : BooleanAlgebra (FirstOrder.Language.DefinableSet L A α)