# mathlib3documentation

model_theory.elementary_maps

# Elementary Maps Between First-Order Structures #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

## Main Definitions #

• A first_order.language.elementary_embedding is an embedding that commutes with the realizations of formulas.
• A first_order.language.elementary_substructure is a substructure where the realization of each formula agrees with the realization in the larger model.
• The first_order.language.elementary_diagram of a structure is the set of all sentences with parameters that the structure satisfies.
• first_order.language.elementary_embedding.of_models_elementary_diagram is the canonical elementary embedding of any structure into a model of its elementary diagram.

## Main Results #

• The Tarski-Vaught Test for embeddings: first_order.language.embedding.is_elementary_of_exists gives a simple criterion for an embedding to be elementary.
• The Tarski-Vaught Test for substructures: first_order.language.embedding.is_elementary_of_exists gives a simple criterion for a substructure to be elementary.
structure first_order.language.elementary_embedding (L : first_order.language) (M : Type u_3) (N : Type u_4) [L.Structure M] [L.Structure N] :
Type (max u_3 u_4)

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

Instances for first_order.language.elementary_embedding
@[protected, instance]
def first_order.language.elementary_embedding.fun_like {L : first_order.language} {M : Type u_3} {N : Type u_4} [L.Structure M] [L.Structure N] :
fun_like N) M (λ (_x : M), N)
Equations
@[protected, instance]
def first_order.language.elementary_embedding.has_coe_to_fun {L : first_order.language} {M : Type u_3} {N : Type u_4} [L.Structure M] [L.Structure N] :
(λ (_x : N), M N)
Equations
@[simp]
theorem first_order.language.elementary_embedding.map_bounded_formula {L : first_order.language} {M : Type u_3} {N : Type u_4} [L.Structure M] [L.Structure N] (f : N) {α : Type u_5} {n : } (φ : n) (v : α M) (xs : fin n M) :
φ.realize (f v) (f xs) φ.realize v xs
@[simp]
theorem first_order.language.elementary_embedding.map_formula {L : first_order.language} {M : Type u_3} {N : Type u_4} [L.Structure M] [L.Structure N] (f : N) {α : Type u_5} (φ : L.formula α) (x : α M) :
φ.realize (f x) φ.realize x
theorem first_order.language.elementary_embedding.map_sentence {L : first_order.language} {M : Type u_3} {N : Type u_4} [L.Structure M] [L.Structure N] (f : N) (φ : L.sentence) :
M φ N φ
theorem first_order.language.elementary_embedding.Theory_model_iff {L : first_order.language} {M : Type u_3} {N : Type u_4} [L.Structure M] [L.Structure N] (f : N) (T : L.Theory) :
M T N T
@[simp]
theorem first_order.language.elementary_embedding.injective {L : first_order.language} {M : Type u_3} {N : Type u_4} [L.Structure M] [L.Structure N] (φ : N) :
@[simp]
theorem first_order.language.elementary_embedding.map_fun {L : first_order.language} {M : Type u_3} {N : Type u_4} [L.Structure M] [L.Structure N] (φ : N) {n : } (f : L.functions n) (x : fin n M) :
@[simp]
theorem first_order.language.elementary_embedding.map_rel {L : first_order.language} {M : Type u_3} {N : Type u_4} [L.Structure M] [L.Structure N] (φ : N) {n : } (r : L.relations n) (x : fin n M) :
@[protected, instance]
Equations
@[simp]
theorem first_order.language.elementary_embedding.map_constants {L : first_order.language} {M : Type u_3} {N : Type u_4} [L.Structure M] [L.Structure N] (φ : N) (c : L.constants) :
φ c = c

An elementary embedding is also a first-order embedding.

Equations
def first_order.language.elementary_embedding.to_hom {L : first_order.language} {M : Type u_3} {N : Type u_4} [L.Structure M] [L.Structure N] (f : N) :
L.hom M N

An elementary embedding is also a first-order homomorphism.

Equations
@[simp]
@[ext]
theorem first_order.language.elementary_embedding.ext {L : first_order.language} {M : Type u_3} {N : Type u_4} [L.Structure M] [L.Structure N] ⦃f g : N⦄ (h : (x : M), f x = g x) :
f = g
theorem first_order.language.elementary_embedding.ext_iff {L : first_order.language} {M : Type u_3} {N : Type u_4} [L.Structure M] [L.Structure N] {f g : N} :
f = g (x : M), f x = g x
@[refl]

The identity elementary embedding from a structure to itself

Equations
@[protected, instance]
Equations
@[trans]
def first_order.language.elementary_embedding.comp {L : first_order.language} {M : Type u_3} {N : Type u_4} {P : Type u_5} [L.Structure M] [L.Structure N] [L.Structure P] (hnp : P) (hmn : N) :
P

Composition of elementary embeddings

Equations
@[simp]
theorem first_order.language.elementary_embedding.comp_apply {L : first_order.language} {M : Type u_3} {N : Type u_4} {P : Type u_5} [L.Structure M] [L.Structure N] [L.Structure P] (g : P) (f : N) (x : M) :
(g.comp f) x = g (f x)
theorem first_order.language.elementary_embedding.comp_assoc {L : first_order.language} {M : Type u_3} {N : Type u_4} {P : Type u_5} {Q : Type u_6} [L.Structure M] [L.Structure N] [L.Structure P] [L.Structure Q] (f : N) (g : P) (h : Q) :
(h.comp g).comp f = h.comp (g.comp f)

Composition of elementary embeddings is associative.

@[reducible]

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

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

Equations
theorem first_order.language.embedding.is_elementary_of_exists {L : first_order.language} {M : Type u_3} {N : Type u_4} [L.Structure M] [L.Structure N] (f : L.embedding M N) (htv : (n : ) (φ : (n + 1)) (x : fin n M) (a : N), (fin.snoc (f x) a) ( (b : M), (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.

def first_order.language.embedding.to_elementary_embedding {L : first_order.language} {M : Type u_3} {N : Type u_4} [L.Structure M] [L.Structure N] (f : L.embedding M N) (htv : (n : ) (φ : (n + 1)) (x : fin n M) (a : N), (fin.snoc (f x) a) ( (b : M), (fin.snoc (f x) (f b)))) :
N

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

Equations
@[simp]
theorem first_order.language.embedding.to_elementary_embedding_to_fun {L : first_order.language} {M : Type u_3} {N : Type u_4} [L.Structure M] [L.Structure N] (f : L.embedding M N) (htv : (n : ) (φ : (n + 1)) (x : fin n M) (a : N), (fin.snoc (f x) a) ( (b : M), (fin.snoc (f x) (f b)))) (ᾰ : M) :

A first-order equivalence is also an elementary embedding.

Equations
@[simp]
@[simp]
theorem first_order.language.realize_term_substructure {L : first_order.language} {M : Type u_3} [L.Structure M] {α : Type u_4} {S : L.substructure M} (v : α S) (t : L.term α) :
@[simp]
theorem first_order.language.substructure.realize_bounded_formula_top {L : first_order.language} {M : Type u_3} [L.Structure M] {α : Type u_4} {n : } {φ : n} {v : α } {xs : fin n } :
φ.realize v xs φ.realize (coe v) (coe xs)
@[simp]
theorem first_order.language.substructure.realize_formula_top {L : first_order.language} {M : Type u_3} [L.Structure M] {α : Type u_4} {φ : L.formula α} {v : α } :
φ.realize v φ.realize (coe v)

A substructure is elementary when every formula applied to a tuple in the subtructure agrees with its value in the overall structure.

Equations

An elementary substructure is one in which every formula applied to a tuple in the subtructure agrees with its value in the overall structure.

Instances for first_order.language.elementary_substructure
@[protected, instance]
Equations
@[protected, instance]
Equations

The natural embedding of an L.substructure of M into M.

Equations
@[protected, instance]

The substructure M of the structure M is elementary.

Equations
@[protected, instance]
Equations
@[protected, instance]
theorem first_order.language.substructure.is_elementary_of_exists {L : first_order.language} {M : Type u_3} [L.Structure M] (S : L.substructure M) (htv : (n : ) (φ : (n + 1)) (x : fin n S) (a : M), (fin.snoc (coe x) a) ( (b : S), (fin.snoc (coe x) b))) :

The Tarski-Vaught test for elementarity of a substructure.

def first_order.language.substructure.to_elementary_substructure {L : first_order.language} {M : Type u_3} [L.Structure M] (S : L.substructure M) (htv : (n : ) (φ : (n + 1)) (x : fin n S) (a : M), (fin.snoc (coe x) a) ( (b : S), (fin.snoc (coe x) b))) :

Bundles a substructure satisfying the Tarski-Vaught test as an elementary substructure.

Equations
@[simp]
theorem first_order.language.substructure.to_elementary_substructure_to_substructure {L : first_order.language} {M : Type u_3} [L.Structure M] (S : L.substructure M) (htv : (n : ) (φ : (n + 1)) (x : fin n S) (a : M), (fin.snoc (coe x) a) ( (b : S), (fin.snoc (coe x) b))) :