Documentation

Mathlib.ModelTheory.ElementaryMaps

Elementary Maps Between First-Order Structures #

Main Definitions #

Main Results #

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 : MN
  • map_formula' : ∀ ⦃n : ⦄ (φ : L.Formula (Fin n)) (x : Fin nM), φ.Realize (self x) φ.Realize x
Instances For

    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.
    Instances For
      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' := }
      @[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 nM) :
      φ.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) :
      theorem 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
      @[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 nM) :
      @[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 nM) :
      theorem 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
      @[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' := }
      Instances For
        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' := }
        Instances For
          @[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 g : L.ElementaryEmbedding M N (h : ∀ (x : M), f x = g x) :
          f = g
          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
          Instances For
            instance FirstOrder.Language.ElementaryEmbedding.instInhabited {L : FirstOrder.Language} {M : Type u_1} [L.Structure M] :
            Inhabited (L.ElementaryEmbedding M M)
            Equations
            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' := }
            Instances For
              @[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
              Instances For
                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
                Instances For
                  @[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✝
                  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 nM) (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 nM) :
                  φ.Realize (f x) φ.Realize x

                  The Tarski-Vaught test for elementarity of an embedding.

                  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 nM) (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' := }
                  Instances For
                    @[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 nM) (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.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' := }
                    Instances For
                      @[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 α) :