Elementary Maps Between First-Order Structures #

Main Definitions #

A FirstOrder.Language.ElementaryEmbedding is an embedding that commutes with the realizations of formulas.
The FirstOrder.Language.elementaryDiagram of a structure is the set of all sentences with parameters that the structure satisfies.
FirstOrder.Language.ElementaryEmbedding.ofModelsElementaryDiagram is the canonical elementary embedding of any structure into a model of its elementary diagram.

Main Results #

The Tarski-Vaught Test for embeddings: FirstOrder.Language.Embedding.isElementary_of_exists gives a simple criterion for an embedding to be elementary.

structure FirstOrder.Language.ElementaryEmbedding (L : Language) (M : Type u_1) (N : Type u_2) [L.Structure M] [L.Structure N] :

Type (max u_1 u_2)

An elementary embedding of first-order structures is an embedding that commutes with the realizations of formulas.

toFun : M → N
map_formula' ⦃n : ℕ⦄ (φ : L.Formula (Fin n)) (x : Fin n → M) : φ.Realize (↑self ∘ x) ↔ φ.Realize x

source

def FirstOrder.«term_↪ₑ[_]_» :

Lean.TrailingParserDescr

An elementary embedding of first-order structures is an embedding that commutes with the realizations of formulas.

Equations

One or more equations did not get rendered due to their size.

source

instance FirstOrder.Language.ElementaryEmbedding.instFunLike {L : Language} {M : Type u_1} {N : Type u_2} [L.Structure M] [L.Structure N] :

FunLike (L.ElementaryEmbedding M N) M N

Equations

FirstOrder.Language.ElementaryEmbedding.instFunLike = { coe := fun (f : L.ElementaryEmbedding M N) => ↑f, coe_injective' := ⋯ }

source

@[simp]

theorem FirstOrder.Language.ElementaryEmbedding.map_boundedFormula {L : Language} {M : Type u_1} {N : Type u_2} [L.Structure M] [L.Structure N] (f : L.ElementaryEmbedding M N) {α : Type u_5} {n : ℕ} (φ : L.BoundedFormula α n) (v : α → M) (xs : Fin n → M) :

φ.Realize (⇑f ∘ v) (⇑f ∘ xs) ↔ φ.Realize v xs

source

@[simp]

theorem FirstOrder.Language.ElementaryEmbedding.map_formula {L : Language} {M : Type u_1} {N : Type u_2} [L.Structure M] [L.Structure N] (f : L.ElementaryEmbedding M N) {α : Type u_5} (φ : L.Formula α) (x : α → M) :

φ.Realize (⇑f ∘ x) ↔ φ.Realize x

source

theorem FirstOrder.Language.ElementaryEmbedding.map_sentence {L : Language} {M : Type u_1} {N : Type u_2} [L.Structure M] [L.Structure N] (f : L.ElementaryEmbedding M N) (φ : L.Sentence) :

M ⊨ φ ↔ N ⊨ φ

source

theorem FirstOrder.Language.ElementaryEmbedding.theory_model_iff {L : Language} {M : Type u_1} {N : Type u_2} [L.Structure M] [L.Structure N] (f : L.ElementaryEmbedding M N) (T : L.Theory) :

M ⊨ T ↔ N ⊨ T

source

theorem FirstOrder.Language.ElementaryEmbedding.elementarilyEquivalent {L : Language} {M : Type u_1} {N : Type u_2} [L.Structure M] [L.Structure N] (f : L.ElementaryEmbedding M N) :

L.ElementarilyEquivalent M N

source

@[simp]

theorem FirstOrder.Language.ElementaryEmbedding.injective {L : Language} {M : Type u_1} {N : Type u_2} [L.Structure M] [L.Structure N] (φ : L.ElementaryEmbedding M N) :

Function.Injective ⇑φ

source

instance FirstOrder.Language.ElementaryEmbedding.embeddingLike {L : Language} {M : Type u_1} {N : Type u_2} [L.Structure M] [L.Structure N] :

EmbeddingLike (L.ElementaryEmbedding M N) M N

source

@[simp]

theorem FirstOrder.Language.ElementaryEmbedding.map_fun {L : Language} {M : Type u_1} {N : Type u_2} [L.Structure M] [L.Structure N] (φ : L.ElementaryEmbedding M N) {n : ℕ} (f : L.Functions n) (x : Fin n → M) :

φ (Structure.funMap f x) = Structure.funMap f (⇑φ ∘ x)

source

@[simp]

theorem FirstOrder.Language.ElementaryEmbedding.map_rel {L : Language} {M : Type u_1} {N : Type u_2} [L.Structure M] [L.Structure N] (φ : L.ElementaryEmbedding M N) {n : ℕ} (r : L.Relations n) (x : Fin n → M) :

Structure.RelMap r (⇑φ ∘ x) ↔ Structure.RelMap r x

source

instance FirstOrder.Language.ElementaryEmbedding.strongHomClass {L : Language} {M : Type u_1} {N : Type u_2} [L.Structure M] [L.Structure N] :

L.StrongHomClass (L.ElementaryEmbedding M N) M N

source

@[simp]

theorem FirstOrder.Language.ElementaryEmbedding.map_constants {L : Language} {M : Type u_1} {N : Type u_2} [L.Structure M] [L.Structure N] (φ : L.ElementaryEmbedding M N) (c : L.Constants) :

φ ↑c = ↑c

source

def FirstOrder.Language.ElementaryEmbedding.toEmbedding {L : Language} {M : Type u_1} {N : Type u_2} [L.Structure M] [L.Structure N] (f : L.ElementaryEmbedding M N) :

L.Embedding M N

An elementary embedding is also a first-order embedding.

Equations

f.toEmbedding = { toFun := ⇑f, inj' := ⋯, map_fun' := ⋯, map_rel' := ⋯ }

source

def FirstOrder.Language.ElementaryEmbedding.toHom {L : Language} {M : Type u_1} {N : Type u_2} [L.Structure M] [L.Structure N] (f : L.ElementaryEmbedding M N) :

L.Hom M N

An elementary embedding is also a first-order homomorphism.

Equations

f.toHom = { toFun := ⇑f, map_fun' := ⋯, map_rel' := ⋯ }

source

@[simp]

theorem FirstOrder.Language.ElementaryEmbedding.toEmbedding_toHom {L : Language} {M : Type u_1} {N : Type u_2} [L.Structure M] [L.Structure N] (f : L.ElementaryEmbedding M N) :

f.toEmbedding.toHom = f.toHom

source

@[simp]

theorem FirstOrder.Language.ElementaryEmbedding.coe_toHom {L : Language} {M : Type u_1} {N : Type u_2} [L.Structure M] [L.Structure N] {f : L.ElementaryEmbedding M N} :

⇑f.toHom = ⇑f

source

@[simp]

theorem FirstOrder.Language.ElementaryEmbedding.coe_toEmbedding {L : Language} {M : Type u_1} {N : Type u_2} [L.Structure M] [L.Structure N] (f : L.ElementaryEmbedding M N) :

⇑f.toEmbedding = ⇑f

source

theorem FirstOrder.Language.ElementaryEmbedding.coe_injective {L : Language} {M : Type u_1} {N : Type u_2} [L.Structure M] [L.Structure N] :

Function.Injective DFunLike.coe

source

theorem FirstOrder.Language.ElementaryEmbedding.ext {L : Language} {M : Type u_1} {N : Type u_2} [L.Structure M] [L.Structure N] ⦃f g : L.ElementaryEmbedding M N⦄ (h : ∀ (x : M), f x = g x) :

f = g

source

def FirstOrder.Language.ElementaryEmbedding.refl (L : Language) (M : Type u_1) [L.Structure M] :

L.ElementaryEmbedding M M

The identity elementary embedding from a structure to itself

Equations

FirstOrder.Language.ElementaryEmbedding.refl L M = { toFun := id, map_formula' := ⋯ }

source

instance FirstOrder.Language.ElementaryEmbedding.instInhabited {L : Language} {M : Type u_1} [L.Structure M] :

Inhabited (L.ElementaryEmbedding M M)

Equations

FirstOrder.Language.ElementaryEmbedding.instInhabited = { default := FirstOrder.Language.ElementaryEmbedding.refl L M }

source

@[simp]

theorem FirstOrder.Language.ElementaryEmbedding.refl_apply {L : Language} {M : Type u_1} [L.Structure M] (x : M) :

(refl L M) x = x

source

def FirstOrder.Language.ElementaryEmbedding.comp {L : Language} {M : Type u_1} {N : Type u_2} {P : Type u_3} [L.Structure M] [L.Structure N] [L.Structure P] (hnp : L.ElementaryEmbedding N P) (hmn : L.ElementaryEmbedding M N) :

L.ElementaryEmbedding M P

Composition of elementary embeddings

Equations

hnp.comp hmn = { toFun := ⇑hnp ∘ ⇑hmn, map_formula' := ⋯ }

source

@[simp]

theorem FirstOrder.Language.ElementaryEmbedding.comp_apply {L : Language} {M : Type u_1} {N : Type u_2} {P : Type u_3} [L.Structure M] [L.Structure N] [L.Structure P] (g : L.ElementaryEmbedding N P) (f : L.ElementaryEmbedding M N) (x : M) :

(g.comp f) x = g (f x)

source

theorem FirstOrder.Language.ElementaryEmbedding.comp_assoc {L : Language} {M : Type u_1} {N : Type u_2} {P : Type u_3} {Q : Type u_4} [L.Structure M] [L.Structure N] [L.Structure P] [L.Structure Q] (f : L.ElementaryEmbedding M N) (g : L.ElementaryEmbedding N P) (h : L.ElementaryEmbedding P Q) :

(h.comp g).comp f = h.comp (g.comp f)

Composition of elementary embeddings is associative.

source

@[reducible, inline]

abbrev FirstOrder.Language.elementaryDiagram (L : Language) (M : Type u_1) [L.Structure M] :

(L.withConstants M).Theory

The elementary diagram of an L-structure is the set of all sentences with parameters it satisfies.

Equations

L.elementaryDiagram M = (L.withConstants M).completeTheory M

source

def FirstOrder.Language.ElementaryEmbedding.ofModelsElementaryDiagram (L : Language) (M : Type u_1) [L.Structure M] (N : Type u_5) [L.Structure N] [(L.withConstants M).Structure N] [(L.lhomWithConstants M).IsExpansionOn N] [N ⊨ L.elementaryDiagram M] :

L.ElementaryEmbedding M N

The canonical elementary embedding of an L-structure into any model of its elementary diagram

Equations

FirstOrder.Language.ElementaryEmbedding.ofModelsElementaryDiagram L M N = { toFun := FirstOrder.Language.constantMap ∘ Sum.inr, map_formula' := ⋯ }

source

@[simp]

theorem FirstOrder.Language.ElementaryEmbedding.ofModelsElementaryDiagram_toFun (L : Language) (M : Type u_1) [L.Structure M] (N : Type u_5) [L.Structure N] [(L.withConstants M).Structure N] [(L.lhomWithConstants M).IsExpansionOn N] [N ⊨ L.elementaryDiagram M] (a✝ : M) :

(ofModelsElementaryDiagram L M N) a✝ = (constantMap ∘ Sum.inr) a✝

source

theorem FirstOrder.Language.Embedding.isElementary_of_exists {L : Language} {M : Type u_1} {N : Type u_2} [L.Structure M] [L.Structure N] (f : L.Embedding M N) (htv : ∀ (n : ℕ) (φ : L.BoundedFormula Empty (n + 1)) (x : Fin n → M) (a : N), φ.Realize default (Fin.snoc (⇑f ∘ x) a) → ∃ (b : M), φ.Realize default (Fin.snoc (⇑f ∘ x) (f b))) {n : ℕ} (φ : L.Formula (Fin n)) (x : Fin n → M) :

φ.Realize (⇑f ∘ x) ↔ φ.Realize x

The Tarski-Vaught test for elementarity of an embedding.

source

def FirstOrder.Language.Embedding.toElementaryEmbedding {L : Language} {M : Type u_1} {N : Type u_2} [L.Structure M] [L.Structure N] (f : L.Embedding M N) (htv : ∀ (n : ℕ) (φ : L.BoundedFormula Empty (n + 1)) (x : Fin n → M) (a : N), φ.Realize default (Fin.snoc (⇑f ∘ x) a) → ∃ (b : M), φ.Realize default (Fin.snoc (⇑f ∘ x) (f b))) :

L.ElementaryEmbedding M N

Bundles an embedding satisfying the Tarski-Vaught test as an elementary embedding.

Equations

f.toElementaryEmbedding htv = { toFun := ⇑f, map_formula' := ⋯ }

source

@[simp]

theorem FirstOrder.Language.Embedding.toElementaryEmbedding_toFun {L : Language} {M : Type u_1} {N : Type u_2} [L.Structure M] [L.Structure N] (f : L.Embedding M N) (htv : ∀ (n : ℕ) (φ : L.BoundedFormula Empty (n + 1)) (x : Fin n → M) (a : N), φ.Realize default (Fin.snoc (⇑f ∘ x) a) → ∃ (b : M), φ.Realize default (Fin.snoc (⇑f ∘ x) (f b))) (a : M) :

(f.toElementaryEmbedding htv) a = f a

source

def FirstOrder.Language.Equiv.toElementaryEmbedding {L : Language} {M : Type u_1} {N : Type u_2} [L.Structure M] [L.Structure N] (f : L.Equiv M N) :

L.ElementaryEmbedding M N

A first-order equivalence is also an elementary embedding.

Equations

f.toElementaryEmbedding = { toFun := ⇑f, map_formula' := ⋯ }

source

@[simp]

theorem FirstOrder.Language.Equiv.toElementaryEmbedding_toEmbedding {L : Language} {M : Type u_1} {N : Type u_2} [L.Structure M] [L.Structure N] (f : L.Equiv M N) :

f.toElementaryEmbedding.toEmbedding = f.toEmbedding

source

@[simp]

theorem FirstOrder.Language.Equiv.coe_toElementaryEmbedding {L : Language} {M : Type u_1} {N : Type u_2} [L.Structure M] [L.Structure N] (f : L.Equiv M N) :

⇑f.toElementaryEmbedding = ⇑f

source

@[simp]

theorem FirstOrder.Language.realize_term_substructure {L : Language} {M : Type u_1} [L.Structure M] {α : Type u_5} {S : L.Substructure M} (v : α → ↥S) (t : L.Term α) :

Term.realize (Subtype.val ∘ v) t = ↑(Term.realize v t)

Documentation

Mathlib.ModelTheory.ElementaryMaps

Elementary Maps Between First-Order Structures #

Main Definitions #

Main Results #