Definable Sets #
This file defines what it means for a set over a first-order structure to be definable.
Main Definitions #
Set.Definableis defined so thatA.Definable L sindicates that the setsof a finite Cartesian power ofMis definable with parameters inA.Set.Definable₁is defined so thatA.Definable₁ L sindicates that(s : Set M)is definable with parameters inA.Set.Definable₂is defined so thatA.Definable₂ L sindicates that(s : Set (M × M))is definable with parameters inA.- A
FirstOrder.Language.DefinableSetis defined so thatL.DefinableSet A αis the Boolean algebra of subsets ofα → Mdefined by formulas with parameters inA. Set.TermDefinablefunctions are those equivalent to some term expressible in the language.Set.TermDefinable₁specialize this to case of unary functions.
Main Results #
L.DefinableSet A αforms aBooleanAlgebraSet.Definable.image_compshows that definability is closed under projections in finite dimensions.- The
Set.TermDefinableproperty is transitive, andTermDefinablefunctions are closed under composition.
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.
Instances For
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
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)}
:
@[simp]
theorem
Set.definable_empty
{M : Type w}
{A : Set M}
{L : FirstOrder.Language}
[L.Structure M]
{α : Type u₁}
:
@[simp]
theorem
Set.definable_univ
{M : Type w}
{A : Set M}
{L : FirstOrder.Language}
[L.Structure M]
{α : Type u₁}
:
theorem
Set.Definable.image_comp_sumInl_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)
:
This lemma is only intended as a helper for Definable.image_comp.
theorem
Set.Definable.singleton
{M : Type w}
(L : FirstOrder.Language)
[L.Structure M]
(a : M)
:
{a}.Definable₁ L {a}
A singleton is definable by parameter as itself.
theorem
Set.Definable.singleton_of_mem
{M : Type w}
(L : FirstOrder.Language)
[L.Structure M]
{a : M}
{A : Set M}
(ha : a ∈ A)
:
A.Definable₁ L {a}
A singleton {a} is definable over any set A that contains a.
theorem
Set.Definable.diagonal
{M : Type w}
(L : FirstOrder.Language)
[L.Structure M]
(A : Set M)
:
A.Definable₂ L (Set.diagonal M)
The 2-dimensional diagonal is definable independent from parameters.
@[implicit_reducible]
instance
FirstOrder.Language.DefinableSet.instSetLike
{L : 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' := ⋯ }
@[implicit_reducible]
instance
FirstOrder.Language.DefinableSet.instPartialOrder
{L : Language}
{M : Type w}
[L.Structure M]
{A : Set M}
{α : Type u₁}
:
PartialOrder (L.DefinableSet A α)
Equations
@[implicit_reducible]
instance
FirstOrder.Language.DefinableSet.instSup
{L : 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, ⋯⟩ }
@[implicit_reducible]
instance
FirstOrder.Language.DefinableSet.instInf
{L : 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, ⋯⟩ }
@[implicit_reducible]
instance
FirstOrder.Language.DefinableSet.instCompl
{L : Language}
{M : Type w}
[L.Structure M]
{A : Set M}
{α : Type u₁}
:
Compl (L.DefinableSet A α)
Equations
- FirstOrder.Language.DefinableSet.instCompl = { compl := fun (s : L.DefinableSet A α) => ⟨(↑s)ᶜ, ⋯⟩ }
@[implicit_reducible]
instance
FirstOrder.Language.DefinableSet.instSDiff
{L : 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, ⋯⟩ }
@[implicit_reducible]
noncomputable instance
FirstOrder.Language.DefinableSet.instHImp
{L : 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, ⋯⟩ }
@[implicit_reducible]
instance
FirstOrder.Language.DefinableSet.instInhabited
{L : Language}
{M : Type w}
[L.Structure M]
{A : Set M}
{α : Type u₁}
:
Inhabited (L.DefinableSet A α)
Equations
- FirstOrder.Language.DefinableSet.instInhabited = { default := ⊥ }
@[simp]
theorem
FirstOrder.Language.DefinableSet.coe_sup
{L : Language}
{M : Type w}
[L.Structure M]
{A : Set M}
{α : Type u₁}
(s t : L.DefinableSet A α)
:
@[simp]
theorem
FirstOrder.Language.DefinableSet.coe_inf
{L : Language}
{M : Type w}
[L.Structure M]
{A : Set M}
{α : Type u₁}
(s t : L.DefinableSet A α)
:
@[implicit_reducible]
noncomputable instance
FirstOrder.Language.DefinableSet.instBooleanAlgebra
{L : 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) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
def
Set.DefinableFun
{M : Type u_1}
(L : FirstOrder.Language)
[L.Structure M]
{α : Type u_2}
(A : Set M)
(f : (α → M) → M)
:
A function from tuples of elements of M to M is definable if its graph is definable.
Equations
- Set.DefinableFun L A f = A.Definable L (Function.tupleGraph f)
Instances For
def
Set.DefinableMap
{M : Type u_1}
(L : FirstOrder.Language)
[L.Structure M]
{α : Type u_2}
{β : Type u_3}
(A : Set M)
(F : (α → M) → β → M)
:
A family of functions is definable when each coordinate is definable.
Equations
- Set.DefinableMap L A F = ∀ (i : β), Set.DefinableFun L A fun (x : α → M) => F x i
Instances For
theorem
Set.DefinableFun.mono
{M : Type u_1}
{L : FirstOrder.Language}
[L.Structure M]
{α : Type u_2}
{A : Set M}
{f : (α → M) → M}
{B : Set M}
(hAs : DefinableFun L A f)
(hAB : A ⊆ B)
:
DefinableFun L B f
theorem
Set.DefinableFun.of_empty
{M : Type u_1}
{L : FirstOrder.Language}
[L.Structure M]
{α : Type u_2}
{A : Set M}
{f : (α → M) → M}
(hAs : DefinableFun L ∅ f)
:
DefinableFun L A f
theorem
Set.empty_definableFun_iff
{M : Type u_1}
{L : FirstOrder.Language}
[L.Structure M]
{α : Type u_2}
{f : (α → M) → M}
:
theorem
Set.definableFun_iff_empty_definableFun_with_params
{M : Type u_1}
{L : FirstOrder.Language}
[L.Structure M]
{α : Type u_2}
{A : Set M}
{f : (α → M) → M}
:
theorem
FirstOrder.Language.Term.definableFun_realize
{M : Type u_1}
{L : Language}
[L.Structure M]
{α : Type u_2}
(t : L.Term α)
:
Set.DefinableFun L ∅ fun (v : α → M) => realize v t
A term is a definable function.
theorem
Set.DefinableFun.fun_symbol
{M : Type u_1}
{L : FirstOrder.Language}
[L.Structure M]
{n : ℕ}
(f : L.Functions n)
:
A function symbol is a definable function.
theorem
FirstOrder.Language.definableFun_var
{M : Type u_1}
(L : Language)
[L.Structure M]
{α : Type u_2}
(i : α)
:
Set.DefinableFun L ∅ fun (v : α → M) => v i
A coordinate projection is a definable function.
theorem
Set.DefinableFun.proj
{M : Type u_1}
(L : FirstOrder.Language)
[L.Structure M]
{α : Type u_2}
{A : Set M}
{i : α}
:
DefinableFun L A fun (v : α → M) => v i
theorem
FirstOrder.Language.definableFun_const
{M : Type u_1}
(L : Language)
[L.Structure M]
{A : Set M}
{a : M}
(γ : Type u_4)
(ha : a ∈ A)
:
Set.DefinableFun L A fun (x : γ → M) => a
A constant function is a definable function.
theorem
Set.Definable.preimage_map
{M : Type u_1}
{L : FirstOrder.Language}
[L.Structure M]
{A : Set M}
{α : Type u_4}
{β : Type u_5}
[Finite β]
{F : (α → M) → β → M}
(hF : DefinableMap L A F)
{S : Set (β → M)}
(hS : A.Definable L S)
:
The preimage of a definable set under a definable map is definable.
theorem
Set.DefinableFun.comp
{M : Type u_1}
{L : FirstOrder.Language}
[L.Structure M]
{α : Type u_2}
{β : Type u_3}
{A : Set M}
{f : (α → M) → M}
[Finite α]
{g : (β → M) → α → M}
(hg : DefinableMap L A g)
(hf : DefinableFun L A f)
:
DefinableFun L A fun (v : β → M) => f (g v)
theorem
Set.DefinableFun.ite
{M : Type u_1}
{L : FirstOrder.Language}
[L.Structure M]
{α : Type u_2}
{A : Set M}
{f : (α → M) → M}
{p : (α → M) → Prop}
{g : (α → M) → M}
[DecidablePred p]
(hp : A.Definable L (setOf p))
(hf : DefinableFun L A f)
(hg : DefinableFun L A g)
:
DefinableFun L A fun (v : α → M) => if p v then f v else g v
theorem
Set.DefinableFun.setOf_eq
{M : Type u_1}
{L : FirstOrder.Language}
[L.Structure M]
{α : Type u_2}
{A : Set M}
{f g : (α → M) → M}
(hf : DefinableFun L A f)
(hg : DefinableFun L A g)
:
The set where two definable functions agree is definable.
theorem
Set.DefinableFun.setOf_eq_const
{M : Type u_1}
{L : FirstOrder.Language}
[L.Structure M]
{α : Type u_2}
{A : Set M}
{f : (α → M) → M}
(hf : DefinableFun L A f)
{a : M}
(ha : a ∈ A)
:
The preimage of a constant under a definable function is definable.
def
Set.TermDefinable
{M : Type w}
(A : Set M)
(L : FirstOrder.Language)
[L.Structure M]
{α : Type u₁}
(f : (α → M) → M)
:
A function from a Cartesian power of a structure to that structure is term-definable over
a set A when the value of the function is given by a term with constants A.
Equations
- A.TermDefinable L f = ∃ (φ : (L.withConstants ↑A).Term α), f = fun (v : α → M) => FirstOrder.Language.Term.realize v φ
Instances For
theorem
Set.TermDefinable.definable_tupleGraph
{M : Type w}
(A : Set M)
(L : FirstOrder.Language)
[L.Structure M]
{α : Type u₁}
{f : (α → M) → M}
(h : A.TermDefinable L f)
:
A.Definable L (Function.tupleGraph f)
Every TermDefinable function has a tupleGraph that is definable.
theorem
Set.TermDefinable.map_expansion
{M : Type w}
{A : Set M}
{L : FirstOrder.Language}
{L' : FirstOrder.Language}
[L.Structure M]
[L'.Structure M]
{α : Type u₁}
{f : (α → M) → M}
(h : A.TermDefinable L f)
(φ : L →ᴸ L')
[φ.IsExpansionOn M]
:
A.TermDefinable L' f
theorem
Set.termDefinable_empty_iff
{M : Type w}
{L : FirstOrder.Language}
[L.Structure M]
{α : Type u₁}
{f : (α → M) → M}
:
theorem
Set.termDefinable_empty_withConstants_iff
{M : Type w}
{A : Set M}
{L : FirstOrder.Language}
[L.Structure M]
{α : Type u₁}
{f : (α → M) → M}
:
theorem
Set.TermDefinable.mono
{M : Type w}
{A : Set M}
{L : FirstOrder.Language}
[L.Structure M]
{α : Type u₁}
{B : Set M}
{f : (α → M) → M}
(h : A.TermDefinable L f)
(hAB : A ⊆ B)
:
B.TermDefinable L f
theorem
Set.TermDefinable.trans
{M : Type w}
{A : Set M}
{L : FirstOrder.Language}
{L' : FirstOrder.Language}
[L.Structure M]
[L'.Structure M]
{β : Type u_1}
{f : (β → M) → M}
(h₁ : A.TermDefinable L f)
(h₂ :
∀ {n : ℕ} (g : (L.withConstants ↑A).Functions n),
A.TermDefinable L' fun (v : Fin n → M) => FirstOrder.Language.Term.realize v g.term)
:
A.TermDefinable L' f
TermDefinable is transitive. If f is TermDefinable in a structure S on L, and all of the functions' realizations on S are TermDefinable on a structure T on L', then f is TermDefinable on T in L'.
def
Set.TermDefinable₁
{M : Type w}
{A : Set M}
(L : FirstOrder.Language)
[L.Structure M]
(f : M → M)
:
A function from a structure to itself is term-definable over a set A when the
value of the function is given by a term with constants A. Like TermDefinable
but specialized for unary functions in order to write M → M instead of (Unit → M) → M.
Equations
- Set.TermDefinable₁ L f = A.TermDefinable L fun (x : Unit → M) => f (x ())
Instances For
theorem
Set.termDefinable₁_iff_termDefinable
{M : Type w}
{A : Set M}
{L : FirstOrder.Language}
[L.Structure M]
(f : M → M)
:
TermDefinable₁ is defined as TermDefinable on the Unit index type.
theorem
Set.TermDefinable.termDefinable₁
{M : Type w}
{A : Set M}
{L : FirstOrder.Language}
[L.Structure M]
(f : M → M)
:
(A.TermDefinable L fun (v : Unit → M) => f (v ())) → TermDefinable₁ L f
Alias of the reverse direction of Set.termDefinable₁_iff_termDefinable.
TermDefinable₁ is defined as TermDefinable on the Unit index type.
theorem
Set.TermDefinable₁.termDefinable
{M : Type w}
{A : Set M}
{L : FirstOrder.Language}
[L.Structure M]
(f : M → M)
:
TermDefinable₁ L f → A.TermDefinable L fun (v : Unit → M) => f (v ())
Alias of the forward direction of Set.termDefinable₁_iff_termDefinable.
TermDefinable₁ is defined as TermDefinable on the Unit index type.
theorem
Set.termDefinable₁_iff_exists_term
{M : Type w}
{A : Set M}
{L : FirstOrder.Language}
[L.Structure M]
{f : M → M}
:
TermDefinable₁ L f ↔ ∃ (φ : (L.withConstants ↑A).Term Unit),
f = (fun (v : Unit → M) => FirstOrder.Language.Term.realize v φ) ∘ Function.const Unit
theorem
Set.TermDefinable₁.definable₂_graph
{M : Type w}
{A : Set M}
{L : FirstOrder.Language}
[L.Structure M]
{f : M → M}
(h : TermDefinable₁ L f)
:
A.Definable₂ L (Function.graph f)
A TermDefinable₁ function has a graph that's Definable₂.
The identity function is TermDefinable₁
theorem
Set.TermDefinable.const
{M : Type w}
{A : Set M}
{L : FirstOrder.Language}
[L.Structure M]
{α : Type u₁}
(C : (L.withConstants ↑A).Constants)
:
A.TermDefinable L (Function.const (α → M) ↑C)
Constant functions are TermDefinable, assuming the constant value is a language constant.
theorem
Set.TermDefinable₁.const
{M : Type w}
{A : Set M}
{L : FirstOrder.Language}
[L.Structure M]
(C : (L.withConstants ↑A).Constants)
:
TermDefinable₁ L (Function.const M ↑C)
Constant functions are TermDefinable₁, assuming the constant value is a language constant.
theorem
Set.TermDefinable.comp
{M : Type w}
{A : Set M}
{L : FirstOrder.Language}
[L.Structure M]
{α : Type u₁}
{β : Type u_1}
{f : (α → M) → M}
{g : α → (β → M) → M}
(hf : A.TermDefinable L f)
(hg : ∀ (i : α), A.TermDefinable L (g i))
:
A.TermDefinable L fun (b : β → M) => f fun (x : α) => g x b
A k-ary TermDefinable function composed with k TermDefinable others is TermDefinable.
theorem
Set.TermDefinable₁.comp
{M : Type w}
{A : Set M}
{L : FirstOrder.Language}
[L.Structure M]
{f g : M → M}
(hf : TermDefinable₁ L f)
(hg : TermDefinable₁ L g)
:
TermDefinable₁ L (f ∘ g)
TermDefinable₁ functions are closed under composition.
theorem
Set.TermDefinable₁.comp_termDefinable
{M : Type w}
{A : Set M}
{L : FirstOrder.Language}
[L.Structure M]
{α : Type u₁}
{f : M → M}
{g : (α → M) → M}
(hf : TermDefinable₁ L f)
(hg : A.TermDefinable L g)
:
A.TermDefinable L (f ∘ g)
A TermDefinable function postcomposed with TermDefinable₁ is TermDefinable.