mathlib documentation

model_theory.elementary_maps

Elementary Maps Between First-Order Structures #

Main Definitions #

Main Results #

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
@[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 : L.elementary_embedding M N) {α : Type} {n : } (φ : L.bounded_formula α 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 : L.elementary_embedding M N) {α : Type} (φ : L.formula α) (x : α M) :
φ.realize (f x) φ.realize x

An elementary embedding is also a first-order embedding.

Equations

An elementary embedding is also a first-order homomorphism.

Equations
@[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 : L.elementary_embedding M 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 : L.elementary_embedding M N} :
f = g (x : M), f x = g x
@[refl]

The identity elementary embedding from a structure to itself

Equations
@[trans]

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 : L.elementary_embedding N P) (f : L.elementary_embedding M 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 : L.elementary_embedding M N) (g : L.elementary_embedding N P) (h : L.elementary_embedding P 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 : ) (φ : L.bounded_formula empty (n + 1)) (x : fin n M) (a : N), φ.realize inhabited.default (fin.snoc (f x) a) ( (b : M), φ.realize inhabited.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.

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 : ) (φ : L.bounded_formula empty (n + 1)) (x : fin n M) (a : N), φ.realize inhabited.default (fin.snoc (f x) a) ( (b : M), φ.realize inhabited.default (fin.snoc (f x) (f b)))) :

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 : ) (φ : L.bounded_formula empty (n + 1)) (x : fin n M) (a : N), φ.realize inhabited.default (fin.snoc (f x) a) ( (b : M), φ.realize inhabited.default (fin.snoc (f x) (f b)))) (ᾰ : M) :

A first-order equivalence is also an elementary embedding.

Equations
@[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 : } {φ : L.bounded_formula α 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

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]

The Tarski-Vaught test for elementarity of a substructure.

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

Equations