# 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 : FirstOrder.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 : MN
• map_formula' : ∀ ⦃n : ⦄ (φ : L.Formula (Fin n)) (x : Fin nM), φ.Realize (self x) φ.Realize x
Instances For
theorem FirstOrder.Language.ElementaryEmbedding.map_formula' {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [L.Structure M] [L.Structure N] (self : L.ElementaryEmbedding M N) ⦃n : (φ : L.Formula (Fin n)) (x : Fin nM) :
φ.Realize (self x) φ.Realize x

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.
Instances For
instance FirstOrder.Language.ElementaryEmbedding.instFunLike {L : FirstOrder.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' := }
instance FirstOrder.Language.ElementaryEmbedding.instCoeFunForall {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [L.Structure M] [L.Structure N] :
CoeFun (L.ElementaryEmbedding M N) fun (x : L.ElementaryEmbedding M N) => MN
Equations
• FirstOrder.Language.ElementaryEmbedding.instCoeFunForall = DFunLike.hasCoeToFun
@[simp]
theorem FirstOrder.Language.ElementaryEmbedding.map_boundedFormula {L : FirstOrder.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 nM) :
φ.Realize (f v) (f xs) φ.Realize v xs
@[simp]
theorem FirstOrder.Language.ElementaryEmbedding.map_formula {L : FirstOrder.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
theorem FirstOrder.Language.ElementaryEmbedding.map_sentence {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [L.Structure M] [L.Structure N] (f : L.ElementaryEmbedding M N) (φ : L.Sentence) :
M φ N φ
theorem FirstOrder.Language.ElementaryEmbedding.theory_model_iff {L : FirstOrder.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
theorem FirstOrder.Language.ElementaryEmbedding.elementarilyEquivalent {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [L.Structure M] [L.Structure N] (f : L.ElementaryEmbedding M N) :
L.ElementarilyEquivalent M N
@[simp]
theorem FirstOrder.Language.ElementaryEmbedding.injective {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [L.Structure M] [L.Structure N] (φ : L.ElementaryEmbedding M N) :
instance FirstOrder.Language.ElementaryEmbedding.embeddingLike {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [L.Structure M] [L.Structure N] :
EmbeddingLike (L.ElementaryEmbedding M N) M N
Equations
• =
@[simp]
theorem FirstOrder.Language.ElementaryEmbedding.map_fun {L : FirstOrder.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 nM) :
@[simp]
theorem FirstOrder.Language.ElementaryEmbedding.map_rel {L : FirstOrder.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 nM) :
instance FirstOrder.Language.ElementaryEmbedding.strongHomClass {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [L.Structure M] [L.Structure N] :
L.StrongHomClass (L.ElementaryEmbedding M N) M N
Equations
• =
@[simp]
theorem FirstOrder.Language.ElementaryEmbedding.map_constants {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [L.Structure M] [L.Structure N] (φ : L.ElementaryEmbedding M N) (c : L.Constants) :
φ c = c
def FirstOrder.Language.ElementaryEmbedding.toEmbedding {L : FirstOrder.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' := }
Instances For
def FirstOrder.Language.ElementaryEmbedding.toHom {L : FirstOrder.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' := }
Instances For
@[simp]
theorem FirstOrder.Language.ElementaryEmbedding.toEmbedding_toHom {L : FirstOrder.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
@[simp]
theorem FirstOrder.Language.ElementaryEmbedding.coe_toHom {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [L.Structure M] [L.Structure N] {f : L.ElementaryEmbedding M N} :
f.toHom = f
@[simp]
theorem FirstOrder.Language.ElementaryEmbedding.coe_toEmbedding {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [L.Structure M] [L.Structure N] (f : L.ElementaryEmbedding M N) :
f.toEmbedding = f
theorem FirstOrder.Language.ElementaryEmbedding.coe_injective {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [L.Structure M] [L.Structure N] :
Function.Injective DFunLike.coe
theorem FirstOrder.Language.ElementaryEmbedding.ext {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [L.Structure M] [L.Structure N] ⦃f : L.ElementaryEmbedding M N ⦃g : L.ElementaryEmbedding M N (h : ∀ (x : M), f x = g x) :
f = g
theorem FirstOrder.Language.ElementaryEmbedding.ext_iff {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [L.Structure M] [L.Structure N] {f : L.ElementaryEmbedding M N} {g : L.ElementaryEmbedding M N} :
f = g ∀ (x : M), f x = g x
def FirstOrder.Language.ElementaryEmbedding.refl (L : FirstOrder.Language) (M : Type u_1) [L.Structure M] :
L.ElementaryEmbedding M M

The identity elementary embedding from a structure to itself

Equations
• = { toFun := id, map_formula' := }
Instances For
instance FirstOrder.Language.ElementaryEmbedding.instInhabited {L : FirstOrder.Language} {M : Type u_1} [L.Structure M] :
Inhabited (L.ElementaryEmbedding M M)
Equations
• FirstOrder.Language.ElementaryEmbedding.instInhabited = { default := }
@[simp]
theorem FirstOrder.Language.ElementaryEmbedding.refl_apply {L : FirstOrder.Language} {M : Type u_1} [L.Structure M] (x : M) :
def FirstOrder.Language.ElementaryEmbedding.comp {L : FirstOrder.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' := }
Instances For
@[simp]
theorem FirstOrder.Language.ElementaryEmbedding.comp_apply {L : FirstOrder.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)
theorem FirstOrder.Language.ElementaryEmbedding.comp_assoc {L : FirstOrder.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.

@[reducible, inline]
abbrev FirstOrder.Language.elementaryDiagram (L : FirstOrder.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
Instances For
@[simp]
theorem FirstOrder.Language.ElementaryEmbedding.ofModelsElementaryDiagram_toFun (L : FirstOrder.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), = (FirstOrder.Language.constantMap Sum.inr) a
def FirstOrder.Language.ElementaryEmbedding.ofModelsElementaryDiagram (L : FirstOrder.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
• = { toFun := FirstOrder.Language.constantMap Sum.inr, map_formula' := }
Instances For
theorem FirstOrder.Language.Embedding.isElementary_of_exists {L : FirstOrder.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 nM) (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 nM) :
φ.Realize (f x) φ.Realize x

The Tarski-Vaught test for elementarity of an embedding.

@[simp]
theorem FirstOrder.Language.Embedding.toElementaryEmbedding_toFun {L : FirstOrder.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 nM) (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
def FirstOrder.Language.Embedding.toElementaryEmbedding {L : FirstOrder.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 nM) (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' := }
Instances For
def FirstOrder.Language.Equiv.toElementaryEmbedding {L : FirstOrder.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' := }
Instances For
@[simp]
theorem FirstOrder.Language.Equiv.toElementaryEmbedding_toEmbedding {L : FirstOrder.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
@[simp]
theorem FirstOrder.Language.Equiv.coe_toElementaryEmbedding {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [L.Structure M] [L.Structure N] (f : L.Equiv M N) :
f.toElementaryEmbedding = f
@[simp]
theorem FirstOrder.Language.realize_term_substructure {L : FirstOrder.Language} {M : Type u_1} [L.Structure M] {α : Type u_5} {S : L.Substructure M} (v : αS) (t : L.Term α) :