mathlib documentation

model_theory.elementary_maps

Elementary Maps Between First-Order Structures #

Main Definitions #

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.

@[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} [fintype α] (φ : L.formula α) (x : α → M) :
@[simp]
theorem first_order.language.elementary_embedding.map_const {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.const) :
φ c = c
@[simp]

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.

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]

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.

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]