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) [L.Structure M] {α : Type u₁} (s : Set (α → M)) :

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.

Equations

A.Definable L s = ∃ (φ : (L.withConstants ↑A).Formula α), s = setOf φ.Realize

Instances For

source

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

A.Definable L' s

source

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

A.Definable L s ↔ ∃ (φ : L.Formula (↑A ⊕ α)), s = {v : α → M | φ.Realize (Sum.elim Subtype.val v)}

source

theorem Set.empty_definable_iff {M : Type w} {L : FirstOrder.Language} [L.Structure M] {α : Type u₁} {s : Set (α → M)} :

∅.Definable L s ↔ ∃ (φ : L.Formula α), s = setOf φ.Realize

source

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

A.Definable L s ↔ ∅.Definable (L.withConstants ↑A) s

source

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

B.Definable L s

source

@[simp]

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

A.Definable L ∅

source

@[simp]

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

A.Definable L Set.univ

source

@[simp]

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

A.Definable L (f ∩ g)

source

@[simp]

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

A.Definable L (f ∪ g)

source

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

A.Definable L (s.inf f)

source

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

A.Definable L (s.sup f)

source

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

A.Definable L (⋂ i ∈ s, f i)

source

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

A.Definable L (⋃ i ∈ s, f i)

source

@[simp]

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

A.Definable L sᶜ

source

@[simp]

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

A.Definable L (s \ t)

source

@[simp]

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

A.Definable L (s ⇨ t)

source

theorem Set.Definable.preimage_comp {M : Type w} {A : Set M} {L : FirstOrder.Language} [L.Structure M] {α : Type u₁} {β : Type u_1} (f : α → β) {s : Set (α → M)} (h : A.Definable L s) :

A.Definable L ((fun (g : β → M) => g ∘ f) ⁻¹' s)

source

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

A.Definable L ((fun (g : β → M) => g ∘ ⇑f) '' s)

source

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

A.Definable L s ↔ ∃ (A0 : Finset M), ↑A0 ⊆ A ∧ (↑A0).Definable L s

source

theorem Set.Definable.image_comp_sum_inl_fin {M : Type w} {A : Set M} {L : FirstOrder.Language} [L.Structure M] {α : Type u₁} (m : ℕ) {s : Set (α ⊕ Fin m → M)} (h : A.Definable L s) :

A.Definable L ((fun (g : α ⊕ Fin m → M) => g ∘ Sum.inl) '' s)

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

source

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

A.Definable L ((fun (g : β → M) => g ∘ ⇑f) '' s)

Shows that definability is closed under finite projections.

source

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

A.Definable L ((fun (g : β → M) => g ∘ f) '' s)

Shows that definability is closed under finite projections.

source

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

Prop

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

Equations

A.Definable₁ L s = A.Definable L {x : Fin 1 → M | x 0 ∈ s}

Instances For

source

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

Prop

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

Equations

A.Definable₂ L s = A.Definable L {x : Fin 2 → M | (x 0, x 1) ∈ s}

Instances For

source

def FirstOrder.Language.DefinableSet (L : FirstOrder.Language) {M : Type w} [L.Structure 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.

Equations

L.DefinableSet A α = { s : Set (α → M) // A.Definable L s }

Instances For

source

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

SetLike (L.DefinableSet A α) (α → M)

Equations

FirstOrder.Language.DefinableSet.instSetLike = { coe := Subtype.val, coe_injective' := ⋯ }

source

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

Top (L.DefinableSet A α)

Equations

FirstOrder.Language.DefinableSet.instTop = { top := ⟨⊤, ⋯⟩ }

source

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

Bot (L.DefinableSet A α)

Equations

FirstOrder.Language.DefinableSet.instBot = { bot := ⟨⊥, ⋯⟩ }

source

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

Max (L.DefinableSet A α)

Equations

FirstOrder.Language.DefinableSet.instSup = { max := fun (s t : L.DefinableSet A α) => ⟨↑s ∪ ↑t, ⋯⟩ }

source

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

Min (L.DefinableSet A α)

Equations

FirstOrder.Language.DefinableSet.instInf = { min := fun (s t : L.DefinableSet A α) => ⟨↑s ∩ ↑t, ⋯⟩ }

source

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

HasCompl (L.DefinableSet A α)

Equations

FirstOrder.Language.DefinableSet.instHasCompl = { compl := fun (s : L.DefinableSet A α) => ⟨(↑s)ᶜ, ⋯⟩ }

source

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

SDiff (L.DefinableSet A α)

Equations

FirstOrder.Language.DefinableSet.instSDiff = { sdiff := fun (s t : L.DefinableSet A α) => ⟨↑s \ ↑t, ⋯⟩ }

source

noncomputable instance FirstOrder.Language.DefinableSet.instHImp {L : FirstOrder.Language} {M : Type w} [L.Structure M] {A : Set M} {α : Type u₁} :

HImp (L.DefinableSet A α)

Equations

FirstOrder.Language.DefinableSet.instHImp = { himp := fun (s t : L.DefinableSet A α) => ⟨↑s ⇨ ↑t, ⋯⟩ }

source

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

Inhabited (L.DefinableSet A α)

Equations

FirstOrder.Language.DefinableSet.instInhabited = { default := ⊥ }

source

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

s ≤ t ↔ ↑s ≤ ↑t

source

@[simp]

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

x ∈ ⊤

source

@[simp]

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

x ∉ ⊥

source

@[simp]

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

x ∈ s ⊔ t ↔ x ∈ s ∨ x ∈ t

source

@[simp]

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

x ∈ s ⊓ t ↔ x ∈ s ∧ x ∈ t

source

@[simp]

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

x ∈ sᶜ ↔ x ∉ s

source

@[simp]

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

x ∈ s \ t ↔ x ∈ s ∧ x ∉ t

source

@[simp]

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

↑⊤ = Set.univ

source

@[simp]

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

↑⊥ = ∅

source

@[simp]

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

↑(s ⊔ t) = ↑s ∪ ↑t

source

@[simp]

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

↑(s ⊓ t) = ↑s ∩ ↑t

source

@[simp]

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

↑sᶜ = (↑s)ᶜ

source

@[simp]

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

↑(s \ t) = ↑s \ ↑t

source

@[simp]

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

↑(s ⇨ t) = ↑s ⇨ ↑t

source

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

BooleanAlgebra (L.DefinableSet A α)

Equations

FirstOrder.Language.DefinableSet.instBooleanAlgebra = Function.Injective.booleanAlgebra (fun (a : { s : Set (α → M) // A.Definable L s }) => ↑a) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

Documentation

Mathlib.ModelTheory.Definability

Definable Sets #

Main Definitions #

Main Results #