Elementary Maps Between First-Order Structures

Main Definitions

• A FirstOrder.Language.ElementaryEmbedding is an embedding that commutes with the realizations of formulas.
• 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.

structure FirstOrder.Language.ElementaryEmbedding (L : FirstOrder.Language) (M : Type u_1) (N : Type u_2) [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] : Type (max u_1 u_2)

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

• toFun : M → N
• map_formula' : ∀ ⦃n : ℕ⦄ (φ : FirstOrder.Language.Formula L (Fin n)) (x : Fin n → M), FirstOrder.Language.Formula.Realize φ (↑self ∘ x) ↔ FirstOrder.Language.Formula.Realize φ x

def FirstOrder.«term_↪ₑ[_]_» : Lean.TrailingParserDescr

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

Equations

• One or more equations did not get rendered due to their size.

instance FirstOrder.Language.ElementaryEmbedding.instFunLike {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] : FunLike (FirstOrder.Language.ElementaryEmbedding L M N) M N

Equations

• FirstOrder.Language.ElementaryEmbedding.instFunLike = { coe := fun (f : FirstOrder.Language.ElementaryEmbedding L M N) => ↑f, coe_injective' := ⋯ }

instance FirstOrder.Language.ElementaryEmbedding.instCoeFunElementaryEmbeddingForAll {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] : CoeFun (FirstOrder.Language.ElementaryEmbedding L M N) fun (x : FirstOrder.Language.ElementaryEmbedding L M N) => M → N

Equations

• FirstOrder.Language.ElementaryEmbedding.instCoeFunElementaryEmbeddingForAll = DFunLike.hasCoeToFun

@[simp]

theorem FirstOrder.Language.ElementaryEmbedding.map_boundedFormula {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] (f : FirstOrder.Language.ElementaryEmbedding L M N) {α : Type u_5} {n : ℕ} (φ : FirstOrder.Language.BoundedFormula L α n) (v : α → M) (xs : Fin n → M) : FirstOrder.Language.BoundedFormula.Realize φ (⇑f ∘ v) (⇑f ∘ xs) ↔ FirstOrder.Language.BoundedFormula.Realize φ v xs

@[simp]

theorem FirstOrder.Language.ElementaryEmbedding.map_formula {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] (f : FirstOrder.Language.ElementaryEmbedding L M N) {α : Type u_5} (φ : FirstOrder.Language.Formula L α) (x : α → M) : FirstOrder.Language.Formula.Realize φ (⇑f ∘ x) ↔ FirstOrder.Language.Formula.Realize φ x

theorem FirstOrder.Language.ElementaryEmbedding.map_sentence {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] (f : FirstOrder.Language.ElementaryEmbedding L M N) (φ : FirstOrder.Language.Sentence L) : M ⊨ φ ↔ N ⊨ φ

theorem FirstOrder.Language.ElementaryEmbedding.theory_model_iff {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] (f : FirstOrder.Language.ElementaryEmbedding L M N) (T : FirstOrder.Language.Theory L) : M ⊨ T ↔ N ⊨ T

theorem FirstOrder.Language.ElementaryEmbedding.elementarilyEquivalent {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] (f : FirstOrder.Language.ElementaryEmbedding L M N) : FirstOrder.Language.ElementarilyEquivalent L M N

@[simp]

theorem FirstOrder.Language.ElementaryEmbedding.injective {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] (φ : FirstOrder.Language.ElementaryEmbedding L M N) : Function.Injective ⇑φ

instance FirstOrder.Language.ElementaryEmbedding.embeddingLike {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] : EmbeddingLike (FirstOrder.Language.ElementaryEmbedding L M N) M N

Equations

• ⋯ = ⋯

@[simp]

theorem FirstOrder.Language.ElementaryEmbedding.map_fun {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] (φ : FirstOrder.Language.ElementaryEmbedding L M N) {n : ℕ} (f : L.Functions n) (x : Fin n → M) : φ (FirstOrder.Language.Structure.funMap f x) = FirstOrder.Language.Structure.funMap f (⇑φ ∘ x)

@[simp]

theorem FirstOrder.Language.ElementaryEmbedding.map_rel {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] (φ : FirstOrder.Language.ElementaryEmbedding L M N) {n : ℕ} (r : L.Relations n) (x : Fin n → M) : FirstOrder.Language.Structure.RelMap r (⇑φ ∘ x) ↔ FirstOrder.Language.Structure.RelMap r x

instance FirstOrder.Language.ElementaryEmbedding.strongHomClass {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] : FirstOrder.Language.StrongHomClass L (FirstOrder.Language.ElementaryEmbedding L M N) M N

Equations

• ⋯ = ⋯

@[simp]

theorem FirstOrder.Language.ElementaryEmbedding.map_constants {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] (φ : FirstOrder.Language.ElementaryEmbedding L M N) (c : FirstOrder.Language.Constants L) : φ ↑c = ↑c

def FirstOrder.Language.ElementaryEmbedding.toEmbedding {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] (f : FirstOrder.Language.ElementaryEmbedding L M N) : FirstOrder.Language.Embedding L M N

An elementary embedding is also a first-order embedding.

Equations

• FirstOrder.Language.ElementaryEmbedding.toEmbedding f = { toEmbedding := { toFun := ⇑f, inj' := ⋯ }, map_fun' := ⋯, map_rel' := ⋯ }

def FirstOrder.Language.ElementaryEmbedding.toHom {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] (f : FirstOrder.Language.ElementaryEmbedding L M N) : FirstOrder.Language.Hom L M N

An elementary embedding is also a first-order homomorphism.

Equations

• FirstOrder.Language.ElementaryEmbedding.toHom f = { toFun := ⇑f, map_fun' := ⋯, map_rel' := ⋯ }

@[simp]

theorem FirstOrder.Language.ElementaryEmbedding.toEmbedding_toHom {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] (f : FirstOrder.Language.ElementaryEmbedding L M N) : FirstOrder.Language.Embedding.toHom (FirstOrder.Language.ElementaryEmbedding.toEmbedding f) = FirstOrder.Language.ElementaryEmbedding.toHom f

@[simp]

theorem FirstOrder.Language.ElementaryEmbedding.coe_toHom {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] {f : FirstOrder.Language.ElementaryEmbedding L M N} : ⇑(FirstOrder.Language.ElementaryEmbedding.toHom f) = ⇑f

@[simp]

theorem FirstOrder.Language.ElementaryEmbedding.coe_toEmbedding {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] (f : FirstOrder.Language.ElementaryEmbedding L M N) : ⇑(FirstOrder.Language.ElementaryEmbedding.toEmbedding f) = ⇑f

theorem FirstOrder.Language.ElementaryEmbedding.coe_injective {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] : Function.Injective DFunLike.coe

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

def FirstOrder.Language.ElementaryEmbedding.refl (L : FirstOrder.Language) (M : Type u_1) [FirstOrder.Language.Structure L M] : FirstOrder.Language.ElementaryEmbedding L M M

The identity elementary embedding from a structure to itself

Equations

• FirstOrder.Language.ElementaryEmbedding.refl L M = { toFun := id, map_formula' := ⋯ }

instance FirstOrder.Language.ElementaryEmbedding.instInhabitedElementaryEmbedding {L : FirstOrder.Language} {M : Type u_1} [FirstOrder.Language.Structure L M] : Inhabited (FirstOrder.Language.ElementaryEmbedding L M M)

Equations

• FirstOrder.Language.ElementaryEmbedding.instInhabitedElementaryEmbedding = { default := FirstOrder.Language.ElementaryEmbedding.refl L M }

@[simp]

theorem FirstOrder.Language.ElementaryEmbedding.refl_apply {L : FirstOrder.Language} {M : Type u_1} [FirstOrder.Language.Structure L M] (x : M) : (FirstOrder.Language.ElementaryEmbedding.refl L M) x = x

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

Composition of elementary embeddings

Equations

• FirstOrder.Language.ElementaryEmbedding.comp hnp hmn = { toFun := ⇑hnp ∘ ⇑hmn, map_formula' := ⋯ }

@[simp]

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

Composition of elementary embeddings is associative.

@[inline, reducible]

abbrev FirstOrder.Language.elementaryDiagram (L : FirstOrder.Language) (M : Type u_1) [FirstOrder.Language.Structure L M] : FirstOrder.Language.Theory (FirstOrder.Language.withConstants L M)

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

Equations

• FirstOrder.Language.elementaryDiagram L M = FirstOrder.Language.completeTheory (FirstOrder.Language.withConstants L M) M

@[simp]

theorem FirstOrder.Language.ElementaryEmbedding.ofModelsElementaryDiagram_toFun (L : FirstOrder.Language) (M : Type u_1) [FirstOrder.Language.Structure L M] (N : Type u_5) [FirstOrder.Language.Structure L N] [FirstOrder.Language.Structure (FirstOrder.Language.withConstants L M) N] [FirstOrder.Language.LHom.IsExpansionOn (FirstOrder.Language.lhomWithConstants L M) N] [N ⊨ FirstOrder.Language.elementaryDiagram L M] : ∀ (a : M), (FirstOrder.Language.ElementaryEmbedding.ofModelsElementaryDiagram L M N) a = (FirstOrder.Language.constantMap ∘ Sum.inr) a

def FirstOrder.Language.ElementaryEmbedding.ofModelsElementaryDiagram (L : FirstOrder.Language) (M : Type u_1) [FirstOrder.Language.Structure L M] (N : Type u_5) [FirstOrder.Language.Structure L N] [FirstOrder.Language.Structure (FirstOrder.Language.withConstants L M) N] [FirstOrder.Language.LHom.IsExpansionOn (FirstOrder.Language.lhomWithConstants L M) N] [N ⊨ FirstOrder.Language.elementaryDiagram L M] : FirstOrder.Language.ElementaryEmbedding L M N

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

Equations

• FirstOrder.Language.ElementaryEmbedding.ofModelsElementaryDiagram L M N = { toFun := FirstOrder.Language.constantMap ∘ Sum.inr, map_formula' := ⋯ }

theorem FirstOrder.Language.Embedding.isElementary_of_exists {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] (f : FirstOrder.Language.Embedding L M N) (htv : ∀ (n : ℕ) (φ : FirstOrder.Language.BoundedFormula L Empty (n + 1)) (x : Fin n → M) (a : N), FirstOrder.Language.BoundedFormula.Realize φ default (Fin.snoc (⇑f ∘ x) a) → ∃ (b : M), FirstOrder.Language.BoundedFormula.Realize φ default (Fin.snoc (⇑f ∘ x) (f b))) {n : ℕ} (φ : FirstOrder.Language.Formula L (Fin n)) (x : Fin n → M) : FirstOrder.Language.Formula.Realize φ (⇑f ∘ x) ↔ FirstOrder.Language.Formula.Realize φ x

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} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] (f : FirstOrder.Language.Embedding L M N) (htv : ∀ (n : ℕ) (φ : FirstOrder.Language.BoundedFormula L Empty (n + 1)) (x : Fin n → M) (a : N), FirstOrder.Language.BoundedFormula.Realize φ default (Fin.snoc (⇑f ∘ x) a) → ∃ (b : M), FirstOrder.Language.BoundedFormula.Realize φ default (Fin.snoc (⇑f ∘ x) (f b))) (a : M) : (FirstOrder.Language.Embedding.toElementaryEmbedding f htv) a = f a

def FirstOrder.Language.Embedding.toElementaryEmbedding {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] (f : FirstOrder.Language.Embedding L M N) (htv : ∀ (n : ℕ) (φ : FirstOrder.Language.BoundedFormula L Empty (n + 1)) (x : Fin n → M) (a : N), FirstOrder.Language.BoundedFormula.Realize φ default (Fin.snoc (⇑f ∘ x) a) → ∃ (b : M), FirstOrder.Language.BoundedFormula.Realize φ default (Fin.snoc (⇑f ∘ x) (f b))) : FirstOrder.Language.ElementaryEmbedding L M N

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

Equations

• FirstOrder.Language.Embedding.toElementaryEmbedding f htv = { toFun := ⇑f, map_formula' := ⋯ }

def FirstOrder.Language.Equiv.toElementaryEmbedding {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] (f : FirstOrder.Language.Equiv L M N) : FirstOrder.Language.ElementaryEmbedding L M N

A first-order equivalence is also an elementary embedding.

Equations

• FirstOrder.Language.Equiv.toElementaryEmbedding f = { toFun := ⇑f, map_formula' := ⋯ }

@[simp]

theorem FirstOrder.Language.Equiv.toElementaryEmbedding_toEmbedding {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] (f : FirstOrder.Language.Equiv L M N) : FirstOrder.Language.ElementaryEmbedding.toEmbedding (FirstOrder.Language.Equiv.toElementaryEmbedding f) = FirstOrder.Language.Equiv.toEmbedding f

@[simp]

theorem FirstOrder.Language.Equiv.coe_toElementaryEmbedding {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] (f : FirstOrder.Language.Equiv L M N) : ⇑(FirstOrder.Language.Equiv.toElementaryEmbedding f) = ⇑f

@[simp]

theorem FirstOrder.Language.realize_term_substructure {L : FirstOrder.Language} {M : Type u_1} [FirstOrder.Language.Structure L M] {α : Type u_5} {S : FirstOrder.Language.Substructure L M} (v : α → ↥S) (t : FirstOrder.Language.Term L α) : FirstOrder.Language.Term.realize (Subtype.val ∘ v) t = ↑(FirstOrder.Language.Term.realize v t)