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
@[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 (L.elementary_embedding M N) M (λ (_x : 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 : 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
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 : L.elementary_embedding M 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 : L.elementary_embedding M N) (T : L.Theory) :
M T N T
@[simp]
@[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] (φ : L.elementary_embedding M 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 : L.elementary_embedding M N) :
L.hom M N

An elementary embedding is also a first-order homomorphism.

Equations
@[simp]
theorem first_order.language.elementary_embedding.coe_to_hom {L : first_order.language} {M : Type u_3} {N : Type u_4} [L.Structure M] [L.Structure N] {f : L.elementary_embedding M N} :
@[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 : 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

The identity elementary embedding from a structure to itself

Equations
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 : L.elementary_embedding N P) (hmn : L.elementary_embedding M N) :

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.

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) :
def first_order.language.equiv.to_elementary_embedding {L : first_order.language} {M : Type u_3} {N : Type u_4} [L.Structure M] [L.Structure N] (f : L.equiv M N) :

A first-order equivalence is also an elementary embedding.

Equations
@[simp]
theorem first_order.language.equiv.coe_to_elementary_embedding {L : first_order.language} {M : Type u_3} {N : Type u_4} [L.Structure M] [L.Structure N] (f : L.equiv M N) :
@[simp]
@[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
structure first_order.language.elementary_substructure (L : first_order.language) (M : Type u_3) [L.Structure M] :
Type u_3

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
@[simp]
@[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 : ) (φ : L.bounded_formula empty (n + 1)) (x : fin nS) (a : M), φ.realize inhabited.default (fin.snoc (coe x) a)(∃ (b : S), φ.realize inhabited.default (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 : ) (φ : L.bounded_formula empty (n + 1)) (x : fin nS) (a : M), φ.realize inhabited.default (fin.snoc (coe x) a)(∃ (b : S), φ.realize inhabited.default (fin.snoc (coe x) b))) :

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

Equations
@[simp]