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)

to_fun : M → N
map_formula' : (∀ ⦃n : ℕ⦄ (φ : L.formula (fin n)) (x : fin n → M), φ.realize (self.to_fun ∘ x) ↔ φ.realize x) . "obviously"

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

Instances for first_order.language.elementary_embedding

first_order.language.elementary_embedding.has_sizeof_inst
first_order.language.elementary_embedding.fun_like
first_order.language.elementary_embedding.has_coe_to_fun
first_order.language.elementary_embedding.embedding_like
first_order.language.elementary_embedding.strong_hom_class
first_order.language.elementary_embedding.inhabited

source

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

first_order.language.elementary_embedding.fun_like = {coe := λ (f : L.elementary_embedding M N), f.to_fun, coe_injective' := _}

source

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

has_coe_to_fun (L.elementary_embedding M N) (λ (_x : L.elementary_embedding M N), M → N)

Equations

first_order.language.elementary_embedding.has_coe_to_fun = fun_like.has_coe_to_fun

source

@[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 u_5} {n : ℕ} (φ : L.bounded_formula α n) (v : α → M) (xs : fin n → M) :

φ.realize (⇑f ∘ v) (⇑f ∘ xs) ↔ φ.realize v xs

source

@[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 u_5} (φ : L.formula α) (x : α → M) :

φ.realize (⇑f ∘ x) ↔ φ.realize x

source

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 ⊨ φ

source

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

source

theorem first_order.language.elementary_embedding.elementarily_equivalent {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.elementarily_equivalent M N

source

@[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] (φ : L.elementary_embedding M N) :

function.injective ⇑φ

source

@[protected, instance]

def first_order.language.elementary_embedding.embedding_like {L : first_order.language} {M : Type u_3} {N : Type u_4} [L.Structure M] [L.Structure N] :

embedding_like (L.elementary_embedding M N) M N

Equations

first_order.language.elementary_embedding.embedding_like = {coe := fun_like.coe (show fun_like (L.elementary_embedding M N) M (λ (_x : M), N), from infer_instance), coe_injective' := _, injective' := _}

source

@[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] (φ : L.elementary_embedding M N) {n : ℕ} (f : L.functions n) (x : fin n → M) :

⇑φ (first_order.language.Structure.fun_map f x) = first_order.language.Structure.fun_map f (⇑φ ∘ x)

source

@[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] (φ : L.elementary_embedding M N) {n : ℕ} (r : L.relations n) (x : fin n → M) :

first_order.language.Structure.rel_map r (⇑φ ∘ x) ↔ first_order.language.Structure.rel_map r x

source

@[protected, instance]

def first_order.language.elementary_embedding.strong_hom_class {L : first_order.language} {M : Type u_3} {N : Type u_4} [L.Structure M] [L.Structure N] :

first_order.language.strong_hom_class L (L.elementary_embedding M N) M N

Equations

first_order.language.elementary_embedding.strong_hom_class = {map_fun := _, map_rel := _}

source

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

source

def first_order.language.elementary_embedding.to_embedding {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.embedding M N

An elementary embedding is also a first-order embedding.

Equations

f.to_embedding = {to_embedding := {to_fun := ⇑f, inj' := _}, map_fun' := _, map_rel' := _}

source

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

f.to_hom = {to_fun := ⇑f, map_fun' := _, map_rel' := _}

source

@[simp]

theorem first_order.language.elementary_embedding.to_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) :

f.to_embedding.to_hom = f.to_hom

source

@[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} :

⇑(f.to_hom) = ⇑f

source

@[simp]

theorem first_order.language.elementary_embedding.coe_to_embedding {L : first_order.language} {M : Type u_3} {N : Type u_4} [L.Structure M] [L.Structure N] (f : L.elementary_embedding M N) :

⇑(f.to_embedding) = ⇑f

source

theorem first_order.language.elementary_embedding.coe_injective {L : first_order.language} {M : Type u_3} {N : Type u_4} [L.Structure M] [L.Structure N] :

function.injective coe_fn

source

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

source

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

source

@[refl]

def first_order.language.elementary_embedding.refl (L : first_order.language) (M : Type u_3) [L.Structure M] :

L.elementary_embedding M M

The identity elementary embedding from a structure to itself

Equations

first_order.language.elementary_embedding.refl L M = {to_fun := id M, map_formula' := _}

source

@[protected, instance]

def first_order.language.elementary_embedding.inhabited {L : first_order.language} {M : Type u_3} [L.Structure M] :

inhabited (L.elementary_embedding M M)

Equations

first_order.language.elementary_embedding.inhabited = {default := first_order.language.elementary_embedding.refl L M _inst_1}

source

@[simp]

theorem first_order.language.elementary_embedding.refl_apply {L : first_order.language} {M : Type u_3} [L.Structure M] (x : M) :

⇑(first_order.language.elementary_embedding.refl L M) x = x

source

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

L.elementary_embedding M P

Composition of elementary embeddings

Equations

hnp.comp hmn = {to_fun := ⇑hnp ∘ ⇑hmn, map_formula' := _}

source

@[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)

source

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.

source

@[reducible]

def first_order.language.elementary_diagram (L : first_order.language) (M : Type u_3) [L.Structure M] :

(L.with_constants M).Theory

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

source

def first_order.language.elementary_embedding.of_models_elementary_diagram (L : first_order.language) (M : Type u_3) [L.Structure M] (N : Type u_4) [L.Structure N] [(L.with_constants M).Structure N] [(L.Lhom_with_constants M).is_expansion_on N] [N ⊨ L.elementary_diagram M] :

L.elementary_embedding M N

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

Equations

first_order.language.elementary_embedding.of_models_elementary_diagram L M N = {to_fun := coe ∘ sum.inr, map_formula' := _}

source

@[simp]

theorem first_order.language.elementary_embedding.of_models_elementary_diagram_to_fun (L : first_order.language) (M : Type u_3) [L.Structure M] (N : Type u_4) [L.Structure N] [(L.with_constants M).Structure N] [(L.Lhom_with_constants M).is_expansion_on N] [N ⊨ L.elementary_diagram M] (ᾰ : M) :

⇑(first_order.language.elementary_embedding.of_models_elementary_diagram L M N) ᾰ = (coe ∘ sum.inr) ᾰ

source

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.

source

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)))) :

L.elementary_embedding M N

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

Equations

f.to_elementary_embedding htv = {to_fun := ⇑f, map_formula' := _}

source

@[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) :

⇑(f.to_elementary_embedding htv) ᾰ = ⇑f ᾰ

source

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) :

L.elementary_embedding M N

A first-order equivalence is also an elementary embedding.

Equations

f.to_elementary_embedding = {to_fun := ⇑f, map_formula' := _}

source

@[simp]

theorem first_order.language.equiv.to_elementary_embedding_to_embedding {L : first_order.language} {M : Type u_3} {N : Type u_4} [L.Structure M] [L.Structure N] (f : L.equiv M N) :

f.to_elementary_embedding.to_embedding = f.to_embedding

source

@[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) :

⇑(f.to_elementary_embedding) = ⇑f

source

@[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 α) :

first_order.language.term.realize (coe ∘ v) t = ↑(first_order.language.term.realize v t)

source

@[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)

source

@[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)

source

def first_order.language.substructure.is_elementary {L : first_order.language} {M : Type u_3} [L.Structure M] (S : L.substructure M) :

Prop

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

Equations

S.is_elementary = ∀ ⦃n : ℕ⦄ (φ : L.formula (fin n)) (x : fin n → ↥S), φ.realize (coe ∘ x) ↔ φ.realize x

source

structure first_order.language.elementary_substructure (L : first_order.language) (M : Type u_3) [L.Structure M] :

Type u_3

to_substructure : L.substructure M
is_elementary' : self.to_substructure.is_elementary

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

first_order.language.elementary_substructure.has_sizeof_inst
first_order.language.elementary_substructure.first_order.language.substructure.has_coe
first_order.language.elementary_substructure.set_like
first_order.language.elementary_substructure.has_top
first_order.language.elementary_substructure.inhabited

source

@[protected, instance]

def first_order.language.elementary_substructure.first_order.language.substructure.has_coe {L : first_order.language} {M : Type u_3} [L.Structure M] :

has_coe (L.elementary_substructure M) (L.substructure M)

Equations

first_order.language.elementary_substructure.first_order.language.substructure.has_coe = {coe := first_order.language.elementary_substructure.to_substructure _inst_1}

source

@[protected, instance]

def first_order.language.elementary_substructure.set_like {L : first_order.language} {M : Type u_3} [L.Structure M] :

set_like (L.elementary_substructure M) M

Equations

first_order.language.elementary_substructure.set_like = {coe := λ (x : L.elementary_substructure M), x.to_substructure.carrier, coe_injective' := _}

source

@[protected, instance]

def first_order.language.elementary_substructure.induced_Structure {L : first_order.language} {M : Type u_3} [L.Structure M] (S : L.elementary_substructure M) :

L.Structure ↥S

Equations

S.induced_Structure = first_order.language.substructure.induced_Structure

source

@[simp]

theorem first_order.language.elementary_substructure.is_elementary {L : first_order.language} {M : Type u_3} [L.Structure M] (S : L.elementary_substructure M) :

↑S.is_elementary

source

def first_order.language.elementary_substructure.subtype {L : first_order.language} {M : Type u_3} [L.Structure M] (S : L.elementary_substructure M) :

L.elementary_embedding ↥S M

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

Equations

S.subtype = {to_fun := coe coe_to_lift, map_formula' := _}

source

@[simp]

theorem first_order.language.elementary_substructure.coe_subtype {L : first_order.language} {M : Type u_3} [L.Structure M] {S : L.elementary_substructure M} :

⇑(S.subtype) = coe

source

@[protected, instance]

def first_order.language.elementary_substructure.has_top {L : first_order.language} {M : Type u_3} [L.Structure M] :

has_top (L.elementary_substructure M)

The substructure M of the structure M is elementary.

Equations

first_order.language.elementary_substructure.has_top = {top := {to_substructure := ⊤, is_elementary' := _}}

source

@[protected, instance]

def first_order.language.elementary_substructure.inhabited {L : first_order.language} {M : Type u_3} [L.Structure M] :

inhabited (L.elementary_substructure M)

Equations

first_order.language.elementary_substructure.inhabited = {default := ⊤}

source

@[simp]

theorem first_order.language.elementary_substructure.mem_top {L : first_order.language} {M : Type u_3} [L.Structure M] (x : M) :

x ∈ ⊤

source

@[simp]

theorem first_order.language.elementary_substructure.coe_top {L : first_order.language} {M : Type u_3} [L.Structure M] :

↑⊤ = set.univ

source

@[simp]

theorem first_order.language.elementary_substructure.realize_sentence {L : first_order.language} {M : Type u_3} [L.Structure M] (S : L.elementary_substructure M) (φ : L.sentence) :

↥S ⊨ φ ↔ M ⊨ φ

source

@[simp]

theorem first_order.language.elementary_substructure.Theory_model_iff {L : first_order.language} {M : Type u_3} [L.Structure M] (S : L.elementary_substructure M) (T : L.Theory) :

↥S ⊨ T ↔ M ⊨ T

source

@[protected, instance]

def first_order.language.elementary_substructure.Theory_model {L : first_order.language} {M : Type u_3} [L.Structure M] {T : L.Theory} [h : M ⊨ T] {S : L.elementary_substructure M} :

↥S ⊨ T

source

@[protected, instance]

def first_order.language.elementary_substructure.nonempty {L : first_order.language} {M : Type u_3} [L.Structure M] [h : nonempty M] {S : L.elementary_substructure M} :

nonempty ↥S

source

theorem first_order.language.elementary_substructure.elementarily_equivalent {L : first_order.language} {M : Type u_3} [L.Structure M] (S : L.elementary_substructure M) :

L.elementarily_equivalent ↥S M

source

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 n → ↥S) (a : M), φ.realize inhabited.default (fin.snoc (coe ∘ x) a) → (∃ (b : ↥S), φ.realize inhabited.default (fin.snoc (coe ∘ x) ↑b))) :

S.is_elementary

The Tarski-Vaught test for elementarity of a substructure.

source

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 n → ↥S) (a : M), φ.realize inhabited.default (fin.snoc (coe ∘ x) a) → (∃ (b : ↥S), φ.realize inhabited.default (fin.snoc (coe ∘ x) ↑b))) :

L.elementary_substructure M

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

Equations

S.to_elementary_substructure htv = {to_substructure := S, is_elementary' := _}

source

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

(S.to_elementary_substructure htv).to_substructure = S