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) [L.Structure M] [L.Structure 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 : ℕ⦄ (φ : L.Formula (Fin n)) (x : Fin n → M), φ.Realize (↑self ∘ x) ↔ φ.Realize x

theorem FirstOrder.Language.ElementaryEmbedding.map_formula' {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [L.Structure M] [L.Structure N] (self : L.ElementaryEmbedding M N) ⦃n : ℕ⦄ (φ : L.Formula (Fin n)) (x : Fin n → M) : φ.Realize (↑self ∘ x) ↔ φ.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} [L.Structure M] [L.Structure N] : FunLike (L.ElementaryEmbedding M N) M N

Equations

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

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

Equations

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

@[simp]

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

@[simp]

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

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

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

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

@[simp]

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

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

Equations

• ⋯ = ⋯

@[simp]

theorem FirstOrder.Language.ElementaryEmbedding.map_fun {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [L.Structure M] [L.Structure N] (φ : L.ElementaryEmbedding 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} [L.Structure M] [L.Structure N] (φ : L.ElementaryEmbedding 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} [L.Structure M] [L.Structure N] : L.StrongHomClass (L.ElementaryEmbedding M N) M N

Equations

• ⋯ = ⋯

@[simp]

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

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

An elementary embedding is also a first-order embedding.

Equations

• 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} [L.Structure M] [L.Structure N] (f : L.ElementaryEmbedding M N) : L.Hom M N

An elementary embedding is also a first-order homomorphism.

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

def FirstOrder.Language.ElementaryEmbedding.refl (L : FirstOrder.Language) (M : Type u_1) [L.Structure M] : L.ElementaryEmbedding 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.instInhabited {L : FirstOrder.Language} {M : Type u_1} [L.Structure M] : Inhabited (L.ElementaryEmbedding M M)

Equations

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

@[simp]

theorem FirstOrder.Language.ElementaryEmbedding.refl_apply {L : FirstOrder.Language} {M : Type u_1} [L.Structure 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} [L.Structure M] [L.Structure N] [L.Structure P] (hnp : L.ElementaryEmbedding N P) (hmn : L.ElementaryEmbedding M N) : L.ElementaryEmbedding M P

Composition of elementary embeddings

Equations

• hnp.comp 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} [L.Structure M] [L.Structure N] [L.Structure P] (g : L.ElementaryEmbedding N P) (f : L.ElementaryEmbedding M N) (x : M) : (g.comp 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} [L.Structure M] [L.Structure N] [L.Structure P] [L.Structure Q] (f : L.ElementaryEmbedding M N) (g : L.ElementaryEmbedding N P) (h : L.ElementaryEmbedding P Q) : (h.comp g).comp f = h.comp (g.comp f)

Composition of elementary embeddings is associative.

@[reducible, inline]

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

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

Equations

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

@[simp]

theorem FirstOrder.Language.ElementaryEmbedding.ofModelsElementaryDiagram_toFun (L : FirstOrder.Language) (M : Type u_1) [L.Structure M] (N : Type u_5) [L.Structure N] [(L.withConstants M).Structure N] [(L.lhomWithConstants M).IsExpansionOn N] [N ⊨ L.elementaryDiagram 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) [L.Structure M] (N : Type u_5) [L.Structure N] [(L.withConstants M).Structure N] [(L.lhomWithConstants M).IsExpansionOn N] [N ⊨ L.elementaryDiagram M] : L.ElementaryEmbedding 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} [L.Structure M] [L.Structure N] (f : L.Embedding M N) (htv : ∀ (n : ℕ) (φ : L.BoundedFormula Empty (n + 1)) (x : Fin n → M) (a : N), φ.Realize default (Fin.snoc (⇑f ∘ x) a) → ∃ (b : M), φ.Realize 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.

@[simp]

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

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

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

Equations

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

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

A first-order equivalence is also an elementary embedding.

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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