# Documentation

Mathlib.ModelTheory.ElementaryMaps

# Elementary Maps Between First-Order Structures #

## Main Definitions #

• A FirstOrder.Language.ElementaryEmbedding is an embedding that commutes with the realizations of formulas.
• A FirstOrder.Language.ElementarySubstructure is a substructure where the realization of each formula agrees with the realization in the larger model.
• 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.
• The Tarski-Vaught Test for substructures: FirstOrder.Language.Substructure.isElementary_of_exists gives a simple criterion for a substructure to be elementary.
structure FirstOrder.Language.ElementaryEmbedding (L : FirstOrder.Language) (M : Type u_1) (N : Type u_2) :
Type (max u_1 u_2)
• toFun : MN
• map_formula' : ∀ ⦃n : ⦄ (φ : ) (x : Fin nM),

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

Instances For

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

Instances For
@[simp]
theorem FirstOrder.Language.ElementaryEmbedding.map_boundedFormula {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} (f : ) {α : Type u_5} {n : } (φ : ) (v : αM) (xs : Fin nM) :
@[simp]
theorem FirstOrder.Language.ElementaryEmbedding.map_formula {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} (f : ) {α : Type u_5} (φ : ) (x : αM) :
theorem FirstOrder.Language.ElementaryEmbedding.map_sentence {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} (f : ) (φ : ) :
M φ N φ
@[simp]
@[simp]
theorem FirstOrder.Language.ElementaryEmbedding.map_fun {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} (φ : ) {n : } (f : ) (x : Fin nM) :
=
@[simp]
theorem FirstOrder.Language.ElementaryEmbedding.map_rel {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} (φ : ) {n : } (r : ) (x : Fin nM) :
@[simp]
theorem FirstOrder.Language.ElementaryEmbedding.map_constants {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} (φ : ) :
φ c = c

An elementary embedding is also a first-order embedding.

Instances For

An elementary embedding is also a first-order homomorphism.

Instances For
@[simp]
theorem FirstOrder.Language.ElementaryEmbedding.ext {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} ⦃f : ⦃g : (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} {f : } {g : } :
f = g ∀ (x : M), f x = g x

The identity elementary embedding from a structure to itself

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

Composition of elementary embeddings

Instances For
@[simp]
theorem FirstOrder.Language.ElementaryEmbedding.comp_apply {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} {P : Type u_3} (g : ) (f : ) (x : M) :
= 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} (f : ) (g : ) (h : ) :

Composition of elementary embeddings is associative.

@[inline, reducible]

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

Instances For

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

Instances For
theorem FirstOrder.Language.Embedding.isElementary_of_exists {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} (f : ) (htv : ∀ (n : ) (φ : ) (x : Fin nM) (a : N), FirstOrder.Language.BoundedFormula.Realize φ default (Fin.snoc (f x) a)b, FirstOrder.Language.BoundedFormula.Realize φ default (Fin.snoc (f x) (f b))) {n : } (φ : ) (x : Fin nM) :

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} (f : ) (htv : ∀ (n : ) (φ : ) (x : Fin nM) (a : N), FirstOrder.Language.BoundedFormula.Realize φ default (Fin.snoc (f x) a)b, FirstOrder.Language.BoundedFormula.Realize φ default (Fin.snoc (f x) (f b))) (a : M) :
= f a
def FirstOrder.Language.Embedding.toElementaryEmbedding {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} (f : ) (htv : ∀ (n : ) (φ : ) (x : Fin nM) (a : N), FirstOrder.Language.BoundedFormula.Realize φ default (Fin.snoc (f x) a)b, FirstOrder.Language.BoundedFormula.Realize φ default (Fin.snoc (f x) (f b))) :

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

Instances For

A first-order equivalence is also an elementary embedding.

Instances For
@[simp]
@[simp]
theorem FirstOrder.Language.realize_term_substructure {L : FirstOrder.Language} {M : Type u_1} {α : Type u_5} {S : } (v : α{ x // x S }) (t : ) :
@[simp]
theorem FirstOrder.Language.Substructure.realize_boundedFormula_top {L : FirstOrder.Language} {M : Type u_1} {α : Type u_5} {n : } {φ : } {v : α{ x // x }} {xs : Fin n{ x // x }} :
FirstOrder.Language.BoundedFormula.Realize φ (Subtype.val v) (Subtype.val xs)
@[simp]
theorem FirstOrder.Language.Substructure.realize_formula_top {L : FirstOrder.Language} {M : Type u_1} {α : Type u_5} {φ : } {v : α{ x // x }} :

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

Instances For
• toSubstructure :
• isElementary' :

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
@[simp]

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

Instances For

The substructure M of the structure M is elementary.

@[simp]
instance FirstOrder.Language.ElementarySubstructure.theory_model {L : FirstOrder.Language} {M : Type u_1} {T : } [h : M T] :
{ x // x S } T
theorem FirstOrder.Language.Substructure.isElementary_of_exists {L : FirstOrder.Language} {M : Type u_1} (S : ) (htv : ∀ (n : ) (φ : ) (x : Fin n{ x // x S }) (a : M), FirstOrder.Language.BoundedFormula.Realize φ default (Fin.snoc (Subtype.val x) a)b, FirstOrder.Language.BoundedFormula.Realize φ default (Fin.snoc (Subtype.val x) b)) :

The Tarski-Vaught test for elementarity of a substructure.

@[simp]
theorem FirstOrder.Language.Substructure.toElementarySubstructure_toSubstructure {L : FirstOrder.Language} {M : Type u_1} (S : ) (htv : ∀ (n : ) (φ : ) (x : Fin n{ x // x S }) (a : M), FirstOrder.Language.BoundedFormula.Realize φ default (Fin.snoc (Subtype.val x) a)b, FirstOrder.Language.BoundedFormula.Realize φ default (Fin.snoc (Subtype.val x) b)) :
def FirstOrder.Language.Substructure.toElementarySubstructure {L : FirstOrder.Language} {M : Type u_1} (S : ) (htv : ∀ (n : ) (φ : ) (x : Fin n{ x // x S }) (a : M), FirstOrder.Language.BoundedFormula.Realize φ default (Fin.snoc (Subtype.val x) a)b, FirstOrder.Language.BoundedFormula.Realize φ default (Fin.snoc (Subtype.val x) b)) :

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

Instances For