Documentation

Mathlib.ModelTheory.Basic

Basics on First-Order Structures #

This file defines first-order languages and structures in the style of the Flypitch project, as well as several important maps between structures.

Main Definitions #

References #

For the Flypitch project:

Languages and Structures #

structure FirstOrder.Language :
Type (max (u + 1) (v + 1))

A first-order language consists of a type of functions of every natural-number arity and a type of relations of every natural-number arity.

  • Functions : Type u

    For every arity, a Type* of functions of that arity

  • Relations : Type v

    For every arity, a Type* of relations of that arity

Instances For
    def FirstOrder.Sequence₂ (a₀ : Type u) (a₁ : Type u) (a₂ : Type u) :
    Type u

    Used to define FirstOrder.Language₂.

    Equations
    Instances For
      instance FirstOrder.Sequence₂.inhabited₀ (a₀ : Type u) (a₁ : Type u) (a₂ : Type u) [h : Inhabited a₀] :
      Equations
      instance FirstOrder.Sequence₂.inhabited₁ (a₀ : Type u) (a₁ : Type u) (a₂ : Type u) [h : Inhabited a₁] :
      Equations
      instance FirstOrder.Sequence₂.inhabited₂ (a₀ : Type u) (a₁ : Type u) (a₂ : Type u) [h : Inhabited a₂] :
      Equations
      instance FirstOrder.Sequence₂.instIsEmptyHAddNatOfNat (a₀ : Type u) (a₁ : Type u) (a₂ : Type u) {n : } :
      IsEmpty (FirstOrder.Sequence₂ a₀ a₁ a₂ (n + 3))
      Equations
      • =
      @[simp]
      theorem FirstOrder.Sequence₂.sum_card (a₀ : Type u) (a₁ : Type u) (a₂ : Type u) :
      (Cardinal.sum fun (i : ) => Cardinal.mk (FirstOrder.Sequence₂ a₀ a₁ a₂ i)) = Cardinal.mk a₀ + Cardinal.mk a₁ + Cardinal.mk a₂
      @[simp]
      theorem FirstOrder.Language.mk₂_Functions (c : Type u) (f₁ : Type u) (f₂ : Type u) (r₁ : Type v) (r₂ : Type v) :
      ∀ (a : ), (FirstOrder.Language.mk₂ c f₁ f₂ r₁ r₂).Functions a = FirstOrder.Sequence₂ c f₁ f₂ a
      @[simp]
      theorem FirstOrder.Language.mk₂_Relations (c : Type u) (f₁ : Type u) (f₂ : Type u) (r₁ : Type v) (r₂ : Type v) :
      ∀ (a : ), (FirstOrder.Language.mk₂ c f₁ f₂ r₁ r₂).Relations a = FirstOrder.Sequence₂ PEmpty.{v + 1} r₁ r₂ a
      def FirstOrder.Language.mk₂ (c : Type u) (f₁ : Type u) (f₂ : Type u) (r₁ : Type v) (r₂ : Type v) :

      A constructor for languages with only constants, unary and binary functions, and unary and binary relations.

      Equations
      Instances For

        The empty language has no symbols.

        Equations
        Instances For

          The sum of two languages consists of the disjoint union of their symbols.

          Equations
          • L.sum L' = { Functions := fun (n : ) => L.Functions n L'.Functions n, Relations := fun (n : ) => L.Relations n L'.Relations n }
          Instances For

            The type of constants in a given language.

            Equations
            • L.Constants = L.Functions 0
            Instances For
              @[simp]
              theorem FirstOrder.Language.constants_mk₂ (c : Type u) (f₁ : Type u) (f₂ : Type u) (r₁ : Type v) (r₂ : Type v) :
              (FirstOrder.Language.mk₂ c f₁ f₂ r₁ r₂).Constants = c

              The type of symbols in a given language.

              Equations
              • L.Symbols = ((l : ) × L.Functions l (l : ) × L.Relations l)
              Instances For

                The cardinality of a language is the cardinality of its type of symbols.

                Equations
                Instances For

                  A language is relational when it has no function symbols.

                  • empty_functions : ∀ (n : ), IsEmpty (L.Functions n)

                    There are no function symbols in the language.

                  Instances
                    theorem FirstOrder.Language.IsRelational.empty_functions {L : FirstOrder.Language} [self : L.IsRelational] (n : ) :
                    IsEmpty (L.Functions n)

                    There are no function symbols in the language.

                    A language is algebraic when it has no relation symbols.

                    • empty_relations : ∀ (n : ), IsEmpty (L.Relations n)

                      There are no relation symbols in the language.

                    Instances
                      theorem FirstOrder.Language.IsAlgebraic.empty_relations {L : FirstOrder.Language} [self : L.IsAlgebraic] (n : ) :
                      IsEmpty (L.Relations n)

                      There are no relation symbols in the language.

                      instance FirstOrder.Language.instIsEmptyFunctionsOfIsRelational {L : FirstOrder.Language} [L.IsRelational] {n : } :
                      IsEmpty (L.Functions n)
                      Equations
                      • =
                      instance FirstOrder.Language.instIsEmptyRelationsOfIsAlgebraic {L : FirstOrder.Language} [L.IsAlgebraic] {n : } :
                      IsEmpty (L.Relations n)
                      Equations
                      • =
                      instance FirstOrder.Language.isRelational_of_empty_functions {symb : Type u_1} :
                      { Functions := fun (x : ) => Empty, Relations := symb }.IsRelational
                      Equations
                      • =
                      instance FirstOrder.Language.isAlgebraic_of_empty_relations {symb : Type u_1} :
                      { Functions := symb, Relations := fun (x : ) => Empty }.IsAlgebraic
                      Equations
                      • =
                      instance FirstOrder.Language.isRelational_sum {L : FirstOrder.Language} {L' : FirstOrder.Language} [L.IsRelational] [L'.IsRelational] :
                      (L.sum L').IsRelational
                      Equations
                      • =
                      instance FirstOrder.Language.isAlgebraic_sum {L : FirstOrder.Language} {L' : FirstOrder.Language} [L.IsAlgebraic] [L'.IsAlgebraic] :
                      (L.sum L').IsAlgebraic
                      Equations
                      • =
                      instance FirstOrder.Language.isRelational_mk₂ {c : Type u} {f₁ : Type u} {f₂ : Type u} {r₁ : Type v} {r₂ : Type v} [h0 : IsEmpty c] [h1 : IsEmpty f₁] [h2 : IsEmpty f₂] :
                      (FirstOrder.Language.mk₂ c f₁ f₂ r₁ r₂).IsRelational
                      Equations
                      • =
                      instance FirstOrder.Language.isAlgebraic_mk₂ {c : Type u} {f₁ : Type u} {f₂ : Type u} {r₁ : Type v} {r₂ : Type v} [h1 : IsEmpty r₁] [h2 : IsEmpty r₂] :
                      (FirstOrder.Language.mk₂ c f₁ f₂ r₁ r₂).IsAlgebraic
                      Equations
                      • =
                      instance FirstOrder.Language.subsingleton_mk₂_functions {c : Type u} {f₁ : Type u} {f₂ : Type u} {r₁ : Type v} {r₂ : Type v} [h0 : Subsingleton c] [h1 : Subsingleton f₁] [h2 : Subsingleton f₂] {n : } :
                      Subsingleton ((FirstOrder.Language.mk₂ c f₁ f₂ r₁ r₂).Functions n)
                      Equations
                      • =
                      instance FirstOrder.Language.subsingleton_mk₂_relations {c : Type u} {f₁ : Type u} {f₂ : Type u} {r₁ : Type v} {r₂ : Type v} [h1 : Subsingleton r₁] [h2 : Subsingleton r₂] {n : } :
                      Subsingleton ((FirstOrder.Language.mk₂ c f₁ f₂ r₁ r₂).Relations n)
                      Equations
                      • =
                      instance FirstOrder.Language.Countable.countable_functions {L : FirstOrder.Language} [h : Countable L.Symbols] :
                      Countable ((l : ) × L.Functions l)
                      Equations
                      • =
                      @[simp]
                      @[simp]
                      class FirstOrder.Language.Structure (L : FirstOrder.Language) (M : Type w) :
                      Type (max (max u v) w)

                      A first-order structure on a type M consists of interpretations of all the symbols in a given language. Each function of arity n is interpreted as a function sending tuples of length n (modeled as (Fin n → M)) to M, and a relation of arity n is a function from tuples of length n to Prop.

                      • funMap : {n : } → L.Functions n(Fin nM)M

                        Interpretation of the function symbols

                      • RelMap : {n : } → L.Relations n(Fin nM)Prop

                        Interpretation of the relation symbols

                      Instances

                        Used for defining FirstOrder.Language.Theory.ModelType.instInhabited.

                        Equations
                        Instances For

                          Maps #

                          structure FirstOrder.Language.Hom (L : FirstOrder.Language) (M : Type w) (N : Type w') [L.Structure M] [L.Structure N] :
                          Type (max w w')

                          A homomorphism between first-order structures is a function that commutes with the interpretations of functions and maps tuples in one structure where a given relation is true to tuples in the second structure where that relation is still true.

                          Instances For
                            theorem FirstOrder.Language.Hom.map_fun' {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (self : L.Hom M N) {n : } (f : L.Functions n) (x : Fin nM) :

                            The homomorphism commutes with the interpretations of the function symbols

                            theorem FirstOrder.Language.Hom.map_rel' {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (self : L.Hom M N) {n : } (r : L.Relations n) (x : Fin nM) :

                            The homomorphism sends related elements to related elements

                            A homomorphism between first-order structures is a function that commutes with the interpretations of functions and maps tuples in one structure where a given relation is true to tuples in the second structure where that relation is still true.

                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              structure FirstOrder.Language.Embedding (L : FirstOrder.Language) (M : Type w) (N : Type w') [L.Structure M] [L.Structure N] extends Function.Embedding :
                              Type (max w w')

                              An embedding of first-order structures is an embedding that commutes with the interpretations of functions and relations.

                              Instances For
                                theorem FirstOrder.Language.Embedding.map_fun' {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (self : L.Embedding M N) {n : } (f : L.Functions n) (x : Fin nM) :

                                The homomorphism commutes with the interpretations of the function symbols

                                theorem FirstOrder.Language.Embedding.map_rel' {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (self : L.Embedding M N) {n : } (r : L.Relations n) (x : Fin nM) :

                                The homomorphism sends related elements to related elements

                                An embedding of first-order structures is an embedding that commutes with the interpretations of functions and relations.

                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  structure FirstOrder.Language.Equiv (L : FirstOrder.Language) (M : Type w) (N : Type w') [L.Structure M] [L.Structure N] extends Equiv :
                                  Type (max w w')

                                  An equivalence of first-order structures is an equivalence that commutes with the interpretations of functions and relations.

                                  Instances For
                                    theorem FirstOrder.Language.Equiv.map_fun' {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (self : L.Equiv M N) {n : } (f : L.Functions n) (x : Fin nM) :

                                    The homomorphism commutes with the interpretations of the function symbols

                                    theorem FirstOrder.Language.Equiv.map_rel' {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (self : L.Equiv M N) {n : } (r : L.Relations n) (x : Fin nM) :

                                    The homomorphism sends related elements to related elements

                                    An equivalence of first-order structures is an equivalence that commutes with the interpretations of functions and relations.

                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For
                                      def FirstOrder.Language.constantMap {L : FirstOrder.Language} {M : Type w} [L.Structure M] (c : L.Constants) :
                                      M

                                      Interpretation of a constant symbol

                                      Equations
                                      Instances For
                                        instance FirstOrder.Language.instCoeTCConstants {L : FirstOrder.Language} {M : Type w} [L.Structure M] :
                                        CoeTC L.Constants M
                                        Equations
                                        • FirstOrder.Language.instCoeTCConstants = { coe := FirstOrder.Language.constantMap }
                                        theorem FirstOrder.Language.funMap_eq_coe_constants {L : FirstOrder.Language} {M : Type w} [L.Structure M] {c : L.Constants} {x : Fin 0M} :
                                        theorem FirstOrder.Language.nonempty_of_nonempty_constants {L : FirstOrder.Language} {M : Type w} [L.Structure M] [h : Nonempty L.Constants] :

                                        Given a language with a nonempty type of constants, any structure will be nonempty. This cannot be a global instance, because L becomes a metavariable.

                                        def FirstOrder.Language.funMap₂ {M : Type w} {c : Type u} {f₁ : Type u} {f₂ : Type u} {r₁ : Type v} {r₂ : Type v} (c' : cM) (f₁' : f₁MM) (f₂' : f₂MMM) {n : } :
                                        (FirstOrder.Language.mk₂ c f₁ f₂ r₁ r₂).Functions n(Fin nM)M

                                        The function map for FirstOrder.Language.Structure₂.

                                        Equations
                                        Instances For
                                          def FirstOrder.Language.RelMap₂ {M : Type w} {c : Type u} {f₁ : Type u} {f₂ : Type u} {r₁ : Type v} {r₂ : Type v} (r₁' : r₁Set M) (r₂' : r₂MMProp) {n : } :
                                          (FirstOrder.Language.mk₂ c f₁ f₂ r₁ r₂).Relations n(Fin nM)Prop

                                          The relation map for FirstOrder.Language.Structure₂.

                                          Equations
                                          Instances For
                                            def FirstOrder.Language.Structure.mk₂ {M : Type w} {c : Type u} {f₁ : Type u} {f₂ : Type u} {r₁ : Type v} {r₂ : Type v} (c' : cM) (f₁' : f₁MM) (f₂' : f₂MMM) (r₁' : r₁Set M) (r₂' : r₂MMProp) :
                                            (FirstOrder.Language.mk₂ c f₁ f₂ r₁ r₂).Structure M

                                            A structure constructor to match FirstOrder.Language₂.

                                            Equations
                                            Instances For
                                              @[simp]
                                              theorem FirstOrder.Language.Structure.funMap_apply₀ {M : Type w} {c : Type u} {f₁ : Type u} {f₂ : Type u} {r₁ : Type v} {r₂ : Type v} {c' : cM} {f₁' : f₁MM} {f₂' : f₂MMM} {r₁' : r₁Set M} {r₂' : r₂MMProp} (c₀ : c) {x : Fin 0M} :
                                              @[simp]
                                              theorem FirstOrder.Language.Structure.funMap_apply₁ {M : Type w} {c : Type u} {f₁ : Type u} {f₂ : Type u} {r₁ : Type v} {r₂ : Type v} {c' : cM} {f₁' : f₁MM} {f₂' : f₂MMM} {r₁' : r₁Set M} {r₂' : r₂MMProp} (f : f₁) (x : M) :
                                              @[simp]
                                              theorem FirstOrder.Language.Structure.funMap_apply₂ {M : Type w} {c : Type u} {f₁ : Type u} {f₂ : Type u} {r₁ : Type v} {r₂ : Type v} {c' : cM} {f₁' : f₁MM} {f₂' : f₂MMM} {r₁' : r₁Set M} {r₂' : r₂MMProp} (f : f₂) (x : M) (y : M) :
                                              @[simp]
                                              theorem FirstOrder.Language.Structure.relMap_apply₁ {M : Type w} {c : Type u} {f₁ : Type u} {f₂ : Type u} {r₁ : Type v} {r₂ : Type v} {c' : cM} {f₁' : f₁MM} {f₂' : f₂MMM} {r₁' : r₁Set M} {r₂' : r₂MMProp} (r : r₁) (x : M) :
                                              @[simp]
                                              theorem FirstOrder.Language.Structure.relMap_apply₂ {M : Type w} {c : Type u} {f₁ : Type u} {f₂ : Type u} {r₁ : Type v} {r₂ : Type v} {c' : cM} {f₁' : f₁MM} {f₂' : f₂MMM} {r₁' : r₁Set M} {r₂' : r₂MMProp} (r : r₂) (x : M) (y : M) :

                                              HomClass L F M N states that F is a type of L-homomorphisms. You should extend this typeclass when you extend FirstOrder.Language.Hom.

                                              Instances
                                                theorem FirstOrder.Language.HomClass.map_fun {L : outParam FirstOrder.Language} {F : Type u_3} {M : Type u_4} {N : Type u_5} [FunLike F M N] [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] [self : FirstOrder.Language.HomClass L F M N] (φ : F) {n : } (f : L.Functions n) (x : Fin nM) :

                                                The homomorphism commutes with the interpretations of the function symbols

                                                The homomorphism sends related elements to related elements

                                                StrongHomClass L F M N states that F is a type of L-homomorphisms which preserve relations in both directions.

                                                Instances

                                                  The homomorphism commutes with the interpretations of the function symbols

                                                  The homomorphism sends related elements to related elements

                                                  @[instance 100]
                                                  instance FirstOrder.Language.StrongHomClass.homClass {L : FirstOrder.Language} {M : Type w} {N : Type w'} {F : Type u_3} [L.Structure M] [L.Structure N] [FunLike F M N] [L.StrongHomClass F M N] :
                                                  L.HomClass F M N
                                                  Equations
                                                  • =
                                                  theorem FirstOrder.Language.HomClass.strongHomClassOfIsAlgebraic {L : FirstOrder.Language} [L.IsAlgebraic] {F : Type u_3} {M : Type u_4} {N : Type u_5} [L.Structure M] [L.Structure N] [FunLike F M N] [L.HomClass F M N] :
                                                  L.StrongHomClass F M N

                                                  Not an instance to avoid a loop.

                                                  theorem FirstOrder.Language.HomClass.map_constants {L : FirstOrder.Language} {F : Type u_3} {M : Type u_4} {N : Type u_5} [L.Structure M] [L.Structure N] [FunLike F M N] [L.HomClass F M N] (φ : F) (c : L.Constants) :
                                                  φ c = c
                                                  instance FirstOrder.Language.Hom.instFunLike {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] :
                                                  FunLike (L.Hom M N) M N
                                                  Equations
                                                  • FirstOrder.Language.Hom.instFunLike = { coe := FirstOrder.Language.Hom.toFun, coe_injective' := }
                                                  instance FirstOrder.Language.Hom.homClass {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] :
                                                  L.HomClass (L.Hom M N) M N
                                                  Equations
                                                  • =
                                                  instance FirstOrder.Language.Hom.instStrongHomClassOfIsAlgebraic {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] [L.IsAlgebraic] :
                                                  L.StrongHomClass (L.Hom M N) M N
                                                  Equations
                                                  • =
                                                  instance FirstOrder.Language.Hom.hasCoeToFun {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] :
                                                  CoeFun (L.Hom M N) fun (x : L.Hom M N) => MN
                                                  Equations
                                                  • FirstOrder.Language.Hom.hasCoeToFun = DFunLike.hasCoeToFun
                                                  @[simp]
                                                  theorem FirstOrder.Language.Hom.toFun_eq_coe {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {f : L.Hom M N} :
                                                  f.toFun = f
                                                  theorem FirstOrder.Language.Hom.ext {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] ⦃f : L.Hom M N ⦃g : L.Hom M N (h : ∀ (x : M), f x = g x) :
                                                  f = g
                                                  theorem FirstOrder.Language.Hom.ext_iff {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {f : L.Hom M N} {g : L.Hom M N} :
                                                  f = g ∀ (x : M), f x = g x
                                                  @[simp]
                                                  theorem FirstOrder.Language.Hom.map_fun {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (φ : L.Hom M N) {n : } (f : L.Functions n) (x : Fin nM) :
                                                  @[simp]
                                                  theorem FirstOrder.Language.Hom.map_constants {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (φ : L.Hom M N) (c : L.Constants) :
                                                  φ c = c
                                                  @[simp]
                                                  theorem FirstOrder.Language.Hom.map_rel {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (φ : L.Hom M N) {n : } (r : L.Relations n) (x : Fin nM) :
                                                  def FirstOrder.Language.Hom.id (L : FirstOrder.Language) (M : Type w) [L.Structure M] :
                                                  L.Hom M M

                                                  The identity map from a structure to itself.

                                                  Equations
                                                  Instances For
                                                    instance FirstOrder.Language.Hom.instInhabited {L : FirstOrder.Language} {M : Type w} [L.Structure M] :
                                                    Inhabited (L.Hom M M)
                                                    Equations
                                                    @[simp]
                                                    theorem FirstOrder.Language.Hom.id_apply {L : FirstOrder.Language} {M : Type w} [L.Structure M] (x : M) :
                                                    def FirstOrder.Language.Hom.comp {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {P : Type u_1} [L.Structure P] (hnp : L.Hom N P) (hmn : L.Hom M N) :
                                                    L.Hom M P

                                                    Composition of first-order homomorphisms.

                                                    Equations
                                                    • hnp.comp hmn = { toFun := hnp hmn, map_fun' := , map_rel' := }
                                                    Instances For
                                                      @[simp]
                                                      theorem FirstOrder.Language.Hom.comp_apply {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {P : Type u_1} [L.Structure P] (g : L.Hom N P) (f : L.Hom M N) (x : M) :
                                                      (g.comp f) x = g (f x)
                                                      theorem FirstOrder.Language.Hom.comp_assoc {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {P : Type u_1} [L.Structure P] {Q : Type u_2} [L.Structure Q] (f : L.Hom M N) (g : L.Hom N P) (h : L.Hom P Q) :
                                                      (h.comp g).comp f = h.comp (g.comp f)

                                                      Composition of first-order homomorphisms is associative.

                                                      @[simp]
                                                      theorem FirstOrder.Language.Hom.comp_id {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (f : L.Hom M N) :
                                                      @[simp]
                                                      theorem FirstOrder.Language.Hom.id_comp {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (f : L.Hom M N) :
                                                      def FirstOrder.Language.HomClass.toHom {L : FirstOrder.Language} {F : Type u_3} {M : Type u_4} {N : Type u_5} [L.Structure M] [L.Structure N] [FunLike F M N] [L.HomClass F M N] :
                                                      FL.Hom M N

                                                      Any element of a HomClass can be realized as a first_order homomorphism.

                                                      Equations
                                                      Instances For
                                                        instance FirstOrder.Language.Embedding.funLike {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] :
                                                        FunLike (L.Embedding M N) M N
                                                        Equations
                                                        • FirstOrder.Language.Embedding.funLike = { coe := fun (f : L.Embedding M N) => f.toFun, coe_injective' := }
                                                        instance FirstOrder.Language.Embedding.embeddingLike {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] :
                                                        EmbeddingLike (L.Embedding M N) M N
                                                        Equations
                                                        • =
                                                        instance FirstOrder.Language.Embedding.strongHomClass {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] :
                                                        L.StrongHomClass (L.Embedding M N) M N
                                                        Equations
                                                        • =
                                                        @[simp]
                                                        theorem FirstOrder.Language.Embedding.map_fun {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (φ : L.Embedding M N) {n : } (f : L.Functions n) (x : Fin nM) :
                                                        @[simp]
                                                        theorem FirstOrder.Language.Embedding.map_constants {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (φ : L.Embedding M N) (c : L.Constants) :
                                                        φ c = c
                                                        @[simp]
                                                        theorem FirstOrder.Language.Embedding.map_rel {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (φ : L.Embedding M N) {n : } (r : L.Relations n) (x : Fin nM) :
                                                        def FirstOrder.Language.Embedding.toHom {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] :
                                                        L.Embedding M NL.Hom M N

                                                        A first-order embedding is also a first-order homomorphism.

                                                        Equations
                                                        • FirstOrder.Language.Embedding.toHom = FirstOrder.Language.HomClass.toHom
                                                        Instances For
                                                          @[simp]
                                                          theorem FirstOrder.Language.Embedding.coe_toHom {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {f : L.Embedding M N} :
                                                          f.toHom = f
                                                          theorem FirstOrder.Language.Embedding.coe_injective {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] :
                                                          Function.Injective DFunLike.coe
                                                          theorem FirstOrder.Language.Embedding.ext {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] ⦃f : L.Embedding M N ⦃g : L.Embedding M N (h : ∀ (x : M), f x = g x) :
                                                          f = g
                                                          theorem FirstOrder.Language.Embedding.ext_iff {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {f : L.Embedding M N} {g : L.Embedding M N} :
                                                          f = g ∀ (x : M), f x = g x
                                                          theorem FirstOrder.Language.Embedding.toHom_injective {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] :
                                                          Function.Injective fun (x : L.Embedding M N) => x.toHom
                                                          @[simp]
                                                          theorem FirstOrder.Language.Embedding.toHom_inj {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {f : L.Embedding M N} {g : L.Embedding M N} :
                                                          f.toHom = g.toHom f = g
                                                          theorem FirstOrder.Language.Embedding.injective {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (f : L.Embedding M N) :
                                                          @[simp]
                                                          theorem FirstOrder.Language.Embedding.ofInjective_toFun {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] [L.IsAlgebraic] {f : L.Hom M N} (hf : Function.Injective f) :
                                                          def FirstOrder.Language.Embedding.ofInjective {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] [L.IsAlgebraic] {f : L.Hom M N} (hf : Function.Injective f) :
                                                          L.Embedding M N

                                                          In an algebraic language, any injective homomorphism is an embedding.

                                                          Equations
                                                          Instances For
                                                            @[simp]
                                                            theorem FirstOrder.Language.Embedding.coeFn_ofInjective {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] [L.IsAlgebraic] {f : L.Hom M N} (hf : Function.Injective f) :
                                                            @[simp]
                                                            theorem FirstOrder.Language.Embedding.ofInjective_toHom {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] [L.IsAlgebraic] {f : L.Hom M N} (hf : Function.Injective f) :
                                                            def FirstOrder.Language.Embedding.refl (L : FirstOrder.Language) (M : Type w) [L.Structure M] :
                                                            L.Embedding M M

                                                            The identity embedding from a structure to itself.

                                                            Equations
                                                            Instances For
                                                              instance FirstOrder.Language.Embedding.instInhabited {L : FirstOrder.Language} {M : Type w} [L.Structure M] :
                                                              Inhabited (L.Embedding M M)
                                                              Equations
                                                              def FirstOrder.Language.Embedding.comp {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {P : Type u_1} [L.Structure P] (hnp : L.Embedding N P) (hmn : L.Embedding M N) :
                                                              L.Embedding M P

                                                              Composition of first-order embeddings.

                                                              Equations
                                                              • hnp.comp hmn = { toFun := hnp hmn, inj' := , map_fun' := , map_rel' := }
                                                              Instances For
                                                                @[simp]
                                                                theorem FirstOrder.Language.Embedding.comp_apply {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {P : Type u_1} [L.Structure P] (g : L.Embedding N P) (f : L.Embedding M N) (x : M) :
                                                                (g.comp f) x = g (f x)
                                                                theorem FirstOrder.Language.Embedding.comp_assoc {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {P : Type u_1} [L.Structure P] {Q : Type u_2} [L.Structure Q] (f : L.Embedding M N) (g : L.Embedding N P) (h : L.Embedding P Q) :
                                                                (h.comp g).comp f = h.comp (g.comp f)

                                                                Composition of first-order embeddings is associative.

                                                                theorem FirstOrder.Language.Embedding.comp_injective {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {P : Type u_1} [L.Structure P] (h : L.Embedding N P) :
                                                                @[simp]
                                                                theorem FirstOrder.Language.Embedding.comp_inj {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {P : Type u_1} [L.Structure P] (h : L.Embedding N P) (f : L.Embedding M N) (g : L.Embedding M N) :
                                                                h.comp f = h.comp g f = g
                                                                theorem FirstOrder.Language.Embedding.toHom_comp_injective {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {P : Type u_1} [L.Structure P] (h : L.Embedding N P) :
                                                                Function.Injective h.toHom.comp
                                                                @[simp]
                                                                theorem FirstOrder.Language.Embedding.toHom_comp_inj {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {P : Type u_1} [L.Structure P] (h : L.Embedding N P) (f : L.Hom M N) (g : L.Hom M N) :
                                                                h.toHom.comp f = h.toHom.comp g f = g
                                                                @[simp]
                                                                theorem FirstOrder.Language.Embedding.comp_toHom {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {P : Type u_1} [L.Structure P] (hnp : L.Embedding N P) (hmn : L.Embedding M N) :
                                                                (hnp.comp hmn).toHom = hnp.toHom.comp hmn.toHom
                                                                @[simp]
                                                                theorem FirstOrder.Language.Embedding.comp_refl {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (f : L.Embedding M N) :
                                                                @[simp]
                                                                theorem FirstOrder.Language.Embedding.refl_comp {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (f : L.Embedding M N) :
                                                                def FirstOrder.Language.StrongHomClass.toEmbedding {L : FirstOrder.Language} {F : Type u_3} {M : Type u_4} {N : Type u_5} [L.Structure M] [L.Structure N] [FunLike F M N] [EmbeddingLike F M N] [L.StrongHomClass F M N] :
                                                                FL.Embedding M N

                                                                Any element of an injective StrongHomClass can be realized as a first_order embedding.

                                                                Equations
                                                                Instances For
                                                                  instance FirstOrder.Language.Equiv.instEquivLike {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] :
                                                                  EquivLike (L.Equiv M N) M N
                                                                  Equations
                                                                  • FirstOrder.Language.Equiv.instEquivLike = { coe := fun (f : L.Equiv M N) => f.toFun, inv := fun (f : L.Equiv M N) => f.invFun, left_inv := , right_inv := , coe_injective' := }
                                                                  instance FirstOrder.Language.Equiv.instStrongHomClass {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] :
                                                                  L.StrongHomClass (L.Equiv M N) M N
                                                                  Equations
                                                                  • =
                                                                  def FirstOrder.Language.Equiv.symm {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (f : L.Equiv M N) :
                                                                  L.Equiv N M

                                                                  The inverse of a first-order equivalence is a first-order equivalence.

                                                                  Equations
                                                                  • f.symm = let __src := f.symm; { toEquiv := __src, map_fun' := , map_rel' := }
                                                                  Instances For
                                                                    instance FirstOrder.Language.Equiv.hasCoeToFun {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] :
                                                                    CoeFun (L.Equiv M N) fun (x : L.Equiv M N) => MN
                                                                    Equations
                                                                    • FirstOrder.Language.Equiv.hasCoeToFun = DFunLike.hasCoeToFun
                                                                    @[simp]
                                                                    theorem FirstOrder.Language.Equiv.symm_symm {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (f : L.Equiv M N) :
                                                                    f.symm.symm = f
                                                                    @[simp]
                                                                    theorem FirstOrder.Language.Equiv.apply_symm_apply {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (f : L.Equiv M N) (a : N) :
                                                                    f (f.symm a) = a
                                                                    @[simp]
                                                                    theorem FirstOrder.Language.Equiv.symm_apply_apply {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (f : L.Equiv M N) (a : M) :
                                                                    f.symm (f a) = a
                                                                    @[simp]
                                                                    theorem FirstOrder.Language.Equiv.map_fun {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (φ : L.Equiv M N) {n : } (f : L.Functions n) (x : Fin nM) :
                                                                    @[simp]
                                                                    theorem FirstOrder.Language.Equiv.map_constants {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (φ : L.Equiv M N) (c : L.Constants) :
                                                                    φ c = c
                                                                    @[simp]
                                                                    theorem FirstOrder.Language.Equiv.map_rel {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (φ : L.Equiv M N) {n : } (r : L.Relations n) (x : Fin nM) :
                                                                    def FirstOrder.Language.Equiv.toEmbedding {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] :
                                                                    L.Equiv M NL.Embedding M N

                                                                    A first-order equivalence is also a first-order embedding.

                                                                    Equations
                                                                    • FirstOrder.Language.Equiv.toEmbedding = FirstOrder.Language.StrongHomClass.toEmbedding
                                                                    Instances For
                                                                      def FirstOrder.Language.Equiv.toHom {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] :
                                                                      L.Equiv M NL.Hom M N

                                                                      A first-order equivalence is also a first-order homomorphism.

                                                                      Equations
                                                                      • FirstOrder.Language.Equiv.toHom = FirstOrder.Language.HomClass.toHom
                                                                      Instances For
                                                                        @[simp]
                                                                        theorem FirstOrder.Language.Equiv.toEmbedding_toHom {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (f : L.Equiv M N) :
                                                                        f.toEmbedding.toHom = f.toHom
                                                                        @[simp]
                                                                        theorem FirstOrder.Language.Equiv.coe_toHom {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {f : L.Equiv M N} :
                                                                        f.toHom = f
                                                                        @[simp]
                                                                        theorem FirstOrder.Language.Equiv.coe_toEmbedding {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (f : L.Equiv M N) :
                                                                        f.toEmbedding = f
                                                                        theorem FirstOrder.Language.Equiv.injective_toEmbedding {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] :
                                                                        Function.Injective FirstOrder.Language.Equiv.toEmbedding
                                                                        theorem FirstOrder.Language.Equiv.coe_injective {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] :
                                                                        Function.Injective DFunLike.coe
                                                                        theorem FirstOrder.Language.Equiv.ext {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] ⦃f : L.Equiv M N ⦃g : L.Equiv M N (h : ∀ (x : M), f x = g x) :
                                                                        f = g
                                                                        theorem FirstOrder.Language.Equiv.ext_iff {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {f : L.Equiv M N} {g : L.Equiv M N} :
                                                                        f = g ∀ (x : M), f x = g x
                                                                        theorem FirstOrder.Language.Equiv.bijective {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (f : L.Equiv M N) :
                                                                        theorem FirstOrder.Language.Equiv.injective {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (f : L.Equiv M N) :
                                                                        theorem FirstOrder.Language.Equiv.surjective {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (f : L.Equiv M N) :
                                                                        def FirstOrder.Language.Equiv.refl (L : FirstOrder.Language) (M : Type w) [L.Structure M] :
                                                                        L.Equiv M M

                                                                        The identity equivalence from a structure to itself.

                                                                        Equations
                                                                        Instances For
                                                                          instance FirstOrder.Language.Equiv.instInhabited {L : FirstOrder.Language} {M : Type w} [L.Structure M] :
                                                                          Inhabited (L.Equiv M M)
                                                                          Equations
                                                                          @[simp]
                                                                          theorem FirstOrder.Language.Equiv.refl_apply {L : FirstOrder.Language} {M : Type w} [L.Structure M] (x : M) :
                                                                          def FirstOrder.Language.Equiv.comp {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {P : Type u_1} [L.Structure P] (hnp : L.Equiv N P) (hmn : L.Equiv M N) :
                                                                          L.Equiv M P

                                                                          Composition of first-order equivalences.

                                                                          Equations
                                                                          • hnp.comp hmn = let __src := hmn.trans hnp.toEquiv; { toFun := hnp hmn, invFun := __src.invFun, left_inv := , right_inv := , map_fun' := , map_rel' := }
                                                                          Instances For
                                                                            @[simp]
                                                                            theorem FirstOrder.Language.Equiv.comp_apply {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {P : Type u_1} [L.Structure P] (g : L.Equiv N P) (f : L.Equiv M N) (x : M) :
                                                                            (g.comp f) x = g (f x)
                                                                            @[simp]
                                                                            theorem FirstOrder.Language.Equiv.comp_refl {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (g : L.Equiv M N) :
                                                                            @[simp]
                                                                            theorem FirstOrder.Language.Equiv.refl_comp {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (g : L.Equiv M N) :
                                                                            theorem FirstOrder.Language.Equiv.comp_assoc {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {P : Type u_1} [L.Structure P] {Q : Type u_2} [L.Structure Q] (f : L.Equiv M N) (g : L.Equiv N P) (h : L.Equiv P Q) :
                                                                            (h.comp g).comp f = h.comp (g.comp f)

                                                                            Composition of first-order homomorphisms is associative.

                                                                            theorem FirstOrder.Language.Equiv.injective_comp {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {P : Type u_1} [L.Structure P] (h : L.Equiv N P) :
                                                                            @[simp]
                                                                            theorem FirstOrder.Language.Equiv.comp_toHom {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {P : Type u_1} [L.Structure P] (hnp : L.Equiv N P) (hmn : L.Equiv M N) :
                                                                            (hnp.comp hmn).toHom = hnp.toHom.comp hmn.toHom
                                                                            @[simp]
                                                                            theorem FirstOrder.Language.Equiv.comp_toEmbedding {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {P : Type u_1} [L.Structure P] (hnp : L.Equiv N P) (hmn : L.Equiv M N) :
                                                                            (hnp.comp hmn).toEmbedding = hnp.toEmbedding.comp hmn.toEmbedding
                                                                            @[simp]
                                                                            theorem FirstOrder.Language.Equiv.self_comp_symm {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (f : L.Equiv M N) :
                                                                            @[simp]
                                                                            theorem FirstOrder.Language.Equiv.symm_comp_self {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (f : L.Equiv M N) :
                                                                            @[simp]
                                                                            theorem FirstOrder.Language.Equiv.symm_comp_self_toEmbedding {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (f : L.Equiv M N) :
                                                                            f.symm.toEmbedding.comp f.toEmbedding = FirstOrder.Language.Embedding.refl L M
                                                                            @[simp]
                                                                            theorem FirstOrder.Language.Equiv.self_comp_symm_toEmbedding {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (f : L.Equiv M N) :
                                                                            f.toEmbedding.comp f.symm.toEmbedding = FirstOrder.Language.Embedding.refl L N
                                                                            @[simp]
                                                                            theorem FirstOrder.Language.Equiv.symm_comp_self_toHom {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (f : L.Equiv M N) :
                                                                            f.symm.toHom.comp f.toHom = FirstOrder.Language.Hom.id L M
                                                                            @[simp]
                                                                            theorem FirstOrder.Language.Equiv.self_comp_symm_toHom {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (f : L.Equiv M N) :
                                                                            f.toHom.comp f.symm.toHom = FirstOrder.Language.Hom.id L N
                                                                            @[simp]
                                                                            theorem FirstOrder.Language.Equiv.comp_symm {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {P : Type u_1} [L.Structure P] (f : L.Equiv M N) (g : L.Equiv N P) :
                                                                            (g.comp f).symm = f.symm.comp g.symm
                                                                            theorem FirstOrder.Language.Equiv.comp_right_injective {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {P : Type u_1} [L.Structure P] (h : L.Equiv M N) :
                                                                            Function.Injective fun (f : L.Equiv N P) => f.comp h
                                                                            @[simp]
                                                                            theorem FirstOrder.Language.Equiv.comp_right_inj {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {P : Type u_1} [L.Structure P] (h : L.Equiv M N) (f : L.Equiv N P) (g : L.Equiv N P) :
                                                                            f.comp h = g.comp h f = g
                                                                            def FirstOrder.Language.StrongHomClass.toEquiv {L : FirstOrder.Language} {F : Type u_3} {M : Type u_4} {N : Type u_5} [L.Structure M] [L.Structure N] [EquivLike F M N] [L.StrongHomClass F M N] :
                                                                            FL.Equiv M N

                                                                            Any element of a bijective StrongHomClass can be realized as a first_order isomorphism.

                                                                            Equations
                                                                            Instances For
                                                                              instance FirstOrder.Language.sumStructure (L₁ : FirstOrder.Language) (L₂ : FirstOrder.Language) (S : Type u_3) [L₁.Structure S] [L₂.Structure S] :
                                                                              (L₁.sum L₂).Structure S
                                                                              Equations
                                                                              • One or more equations did not get rendered due to their size.
                                                                              @[simp]
                                                                              theorem FirstOrder.Language.funMap_sum_inl {L₁ : FirstOrder.Language} {L₂ : FirstOrder.Language} {S : Type u_3} [L₁.Structure S] [L₂.Structure S] {n : } (f : L₁.Functions n) :
                                                                              @[simp]
                                                                              theorem FirstOrder.Language.funMap_sum_inr {L₁ : FirstOrder.Language} {L₂ : FirstOrder.Language} {S : Type u_3} [L₁.Structure S] [L₂.Structure S] {n : } (f : L₂.Functions n) :
                                                                              @[simp]
                                                                              theorem FirstOrder.Language.relMap_sum_inl {L₁ : FirstOrder.Language} {L₂ : FirstOrder.Language} {S : Type u_3} [L₁.Structure S] [L₂.Structure S] {n : } (R : L₁.Relations n) :
                                                                              @[simp]
                                                                              theorem FirstOrder.Language.relMap_sum_inr {L₁ : FirstOrder.Language} {L₂ : FirstOrder.Language} {S : Type u_3} [L₁.Structure S] [L₂.Structure S] {n : } (R : L₂.Relations n) :
                                                                              Equations
                                                                              • FirstOrder.Language.emptyStructure = { funMap := fun {n : } => Empty.elim, RelMap := fun {n : } => Empty.elim }
                                                                              Equations
                                                                              • FirstOrder.Language.instUniqueStructureEmpty = { default := FirstOrder.Language.emptyStructure, uniq := }
                                                                              @[instance 100]
                                                                              instance FirstOrder.Language.strongHomClassEmpty {F : Type u_3} {M : Type u_4} {N : Type u_5} [FunLike F M N] :
                                                                              FirstOrder.Language.empty.StrongHomClass F M N
                                                                              Equations
                                                                              • =
                                                                              @[simp]
                                                                              theorem Function.emptyHom_toFun {M : Type w} {N : Type w'} (f : MN) :
                                                                              ∀ (a : M), (Function.emptyHom f) a = f a
                                                                              def Function.emptyHom {M : Type w} {N : Type w'} (f : MN) :

                                                                              Makes a Language.empty.Hom out of any function.

                                                                              Equations
                                                                              Instances For
                                                                                def Embedding.empty {M : Type w} {N : Type w'} (f : M N) :

                                                                                Makes a Language.empty.Embedding out of any function.

                                                                                Equations
                                                                                Instances For
                                                                                  @[simp]
                                                                                  theorem FirstOrder.Language.toFun_embedding_empty {M : Type w} {N : Type w'} (f : M N) :
                                                                                  (Embedding.empty f) = f
                                                                                  @[simp]
                                                                                  theorem FirstOrder.Language.toEmbedding_embedding_empty {M : Type w} {N : Type w'} (f : M N) :
                                                                                  (Embedding.empty f).toEmbedding = f
                                                                                  def Equiv.empty {M : Type w} {N : Type w'} (f : M N) :

                                                                                  Makes a Language.empty.Equiv out of any function.

                                                                                  Equations
                                                                                  • f.empty = { toEquiv := f, map_fun' := , map_rel' := }
                                                                                  Instances For
                                                                                    @[simp]
                                                                                    theorem FirstOrder.Language.toFun_equiv_empty {M : Type w} {N : Type w'} (f : M N) :
                                                                                    f.empty = f
                                                                                    @[simp]
                                                                                    theorem FirstOrder.Language.toEquiv_equiv_empty {M : Type w} {N : Type w'} (f : M N) :
                                                                                    f.empty.toEquiv = f
                                                                                    @[simp]
                                                                                    theorem Equiv.inducedStructure_RelMap {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [L.Structure M] (e : M N) :
                                                                                    ∀ {n : } (r : L.Relations n) (x : Fin nN), FirstOrder.Language.Structure.RelMap r x = FirstOrder.Language.Structure.RelMap r (e.symm x)
                                                                                    @[simp]
                                                                                    theorem Equiv.inducedStructure_funMap {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [L.Structure M] (e : M N) :
                                                                                    ∀ {n : } (f : L.Functions n) (x : Fin nN), FirstOrder.Language.Structure.funMap f x = e (FirstOrder.Language.Structure.funMap f (e.symm x))
                                                                                    def Equiv.inducedStructure {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [L.Structure M] (e : M N) :
                                                                                    L.Structure N

                                                                                    A structure induced by a bijection.

                                                                                    Equations
                                                                                    • One or more equations did not get rendered due to their size.
                                                                                    Instances For
                                                                                      def Equiv.inducedStructureEquiv {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [L.Structure M] (e : M N) :
                                                                                      L.Equiv M N

                                                                                      A bijection as a first-order isomorphism with the induced structure on the codomain.

                                                                                      Equations
                                                                                      • e.inducedStructureEquiv = { toEquiv := e, map_fun' := , map_rel' := }
                                                                                      Instances For
                                                                                        @[simp]
                                                                                        theorem Equiv.toEquiv_inducedStructureEquiv {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [L.Structure M] (e : M N) :
                                                                                        e.inducedStructureEquiv.toEquiv = e
                                                                                        @[simp]
                                                                                        theorem Equiv.toFun_inducedStructureEquiv {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [L.Structure M] (e : M N) :
                                                                                        e.inducedStructureEquiv = e
                                                                                        @[simp]
                                                                                        theorem Equiv.toFun_inducedStructureEquiv_Symm {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [L.Structure M] (e : M N) :
                                                                                        e.inducedStructureEquiv.symm = e.symm