Documentation

Mathlib.ModelTheory.Substructures

First-Order Substructures #

This file defines substructures of first-order structures in a similar manner to the various substructures appearing in the algebra library.

Main Definitions #

Main Results #

def FirstOrder.Language.ClosedUnder {L : FirstOrder.Language} {M : Type w} [L.Structure M] {n : } (f : L.Functions n) (s : Set M) :

Indicates that a set in a given structure is a closed under a function symbol.

Equations
Instances For
    @[simp]
    theorem FirstOrder.Language.closedUnder_univ (L : FirstOrder.Language) {M : Type w} [L.Structure M] {n : } (f : L.Functions n) :
    theorem FirstOrder.Language.ClosedUnder.inter {L : FirstOrder.Language} {M : Type w} [L.Structure M] {n : } {f : L.Functions n} {s : Set M} {t : Set M} (hs : FirstOrder.Language.ClosedUnder f s) (ht : FirstOrder.Language.ClosedUnder f t) :
    theorem FirstOrder.Language.ClosedUnder.inf {L : FirstOrder.Language} {M : Type w} [L.Structure M] {n : } {f : L.Functions n} {s : Set M} {t : Set M} (hs : FirstOrder.Language.ClosedUnder f s) (ht : FirstOrder.Language.ClosedUnder f t) :
    theorem FirstOrder.Language.ClosedUnder.sInf {L : FirstOrder.Language} {M : Type w} [L.Structure M] {n : } {f : L.Functions n} {S : Set (Set M)} (hS : sS, FirstOrder.Language.ClosedUnder f s) :
    structure FirstOrder.Language.Substructure (L : FirstOrder.Language) (M : Type w) [L.Structure M] :

    A substructure of a structure M is a set closed under application of function symbols.

    Instances For
      theorem FirstOrder.Language.Substructure.fun_mem {L : FirstOrder.Language} {M : Type w} [L.Structure M] (self : L.Substructure M) {n : } (f : L.Functions n) :
      instance FirstOrder.Language.Substructure.instSetLike {L : FirstOrder.Language} {M : Type w} [L.Structure M] :
      SetLike (L.Substructure M) M
      Equations
      • FirstOrder.Language.Substructure.instSetLike = { coe := FirstOrder.Language.Substructure.carrier, coe_injective' := }
      def FirstOrder.Language.Substructure.Simps.coe {L : FirstOrder.Language} {M : Type w} [L.Structure M] (S : L.Substructure M) :
      Set M

      See Note [custom simps projection]

      Equations
      Instances For
        @[simp]
        theorem FirstOrder.Language.Substructure.mem_carrier {L : FirstOrder.Language} {M : Type w} [L.Structure M] {s : L.Substructure M} {x : M} :
        x s x s
        theorem FirstOrder.Language.Substructure.ext {L : FirstOrder.Language} {M : Type w} [L.Structure M] {S : L.Substructure M} {T : L.Substructure M} (h : ∀ (x : M), x S x T) :
        S = T

        Two substructures are equal if they have the same elements.

        def FirstOrder.Language.Substructure.copy {L : FirstOrder.Language} {M : Type w} [L.Structure M] (S : L.Substructure M) (s : Set M) (hs : s = S) :
        L.Substructure M

        Copy a substructure replacing carrier with a set that is equal to it.

        Equations
        • S.copy s hs = { carrier := s, fun_mem := }
        Instances For
          theorem FirstOrder.Language.Term.realize_mem {L : FirstOrder.Language} {M : Type w} [L.Structure M] {S : L.Substructure M} {α : Type u_3} (t : L.Term α) (xs : αM) (h : ∀ (a : α), xs a S) :
          @[simp]
          theorem FirstOrder.Language.Substructure.coe_copy {L : FirstOrder.Language} {M : Type w} [L.Structure M] {S : L.Substructure M} {s : Set M} (hs : s = S) :
          (S.copy s hs) = s
          theorem FirstOrder.Language.Substructure.copy_eq {L : FirstOrder.Language} {M : Type w} [L.Structure M] {S : L.Substructure M} {s : Set M} (hs : s = S) :
          S.copy s hs = S
          theorem FirstOrder.Language.Substructure.constants_mem {L : FirstOrder.Language} {M : Type w} [L.Structure M] {S : L.Substructure M} (c : L.Constants) :
          c S
          instance FirstOrder.Language.Substructure.instTop {L : FirstOrder.Language} {M : Type w} [L.Structure M] :
          Top (L.Substructure M)

          The substructure M of the structure M.

          Equations
          • FirstOrder.Language.Substructure.instTop = { top := { carrier := Set.univ, fun_mem := } }
          instance FirstOrder.Language.Substructure.instInhabited {L : FirstOrder.Language} {M : Type w} [L.Structure M] :
          Inhabited (L.Substructure M)
          Equations
          • FirstOrder.Language.Substructure.instInhabited = { default := }
          @[simp]
          theorem FirstOrder.Language.Substructure.mem_top {L : FirstOrder.Language} {M : Type w} [L.Structure M] (x : M) :
          @[simp]
          theorem FirstOrder.Language.Substructure.coe_top {L : FirstOrder.Language} {M : Type w} [L.Structure M] :
          = Set.univ
          instance FirstOrder.Language.Substructure.instInf {L : FirstOrder.Language} {M : Type w} [L.Structure M] :
          Inf (L.Substructure M)

          The inf of two substructures is their intersection.

          Equations
          • FirstOrder.Language.Substructure.instInf = { inf := fun (S₁ S₂ : L.Substructure M) => { carrier := S₁ S₂, fun_mem := } }
          @[simp]
          theorem FirstOrder.Language.Substructure.coe_inf {L : FirstOrder.Language} {M : Type w} [L.Structure M] (p : L.Substructure M) (p' : L.Substructure M) :
          (p p') = p p'
          @[simp]
          theorem FirstOrder.Language.Substructure.mem_inf {L : FirstOrder.Language} {M : Type w} [L.Structure M] {p : L.Substructure M} {p' : L.Substructure M} {x : M} :
          x p p' x p x p'
          instance FirstOrder.Language.Substructure.instInfSet {L : FirstOrder.Language} {M : Type w} [L.Structure M] :
          InfSet (L.Substructure M)
          Equations
          • FirstOrder.Language.Substructure.instInfSet = { sInf := fun (s : Set (L.Substructure M)) => { carrier := ts, t, fun_mem := } }
          @[simp]
          theorem FirstOrder.Language.Substructure.coe_sInf {L : FirstOrder.Language} {M : Type w} [L.Structure M] (S : Set (L.Substructure M)) :
          (sInf S) = sS, s
          theorem FirstOrder.Language.Substructure.mem_sInf {L : FirstOrder.Language} {M : Type w} [L.Structure M] {S : Set (L.Substructure M)} {x : M} :
          x sInf S pS, x p
          theorem FirstOrder.Language.Substructure.mem_iInf {L : FirstOrder.Language} {M : Type w} [L.Structure M] {ι : Sort u_3} {S : ιL.Substructure M} {x : M} :
          x ⨅ (i : ι), S i ∀ (i : ι), x S i
          @[simp]
          theorem FirstOrder.Language.Substructure.coe_iInf {L : FirstOrder.Language} {M : Type w} [L.Structure M] {ι : Sort u_3} {S : ιL.Substructure M} :
          (⨅ (i : ι), S i) = ⋂ (i : ι), (S i)
          instance FirstOrder.Language.Substructure.instCompleteLattice {L : FirstOrder.Language} {M : Type w} [L.Structure M] :
          CompleteLattice (L.Substructure M)

          Substructures of a structure form a complete lattice.

          Equations
          def FirstOrder.Language.Substructure.closure (L : FirstOrder.Language) {M : Type w} [L.Structure M] :
          LowerAdjoint SetLike.coe

          The L.Substructure generated by a set.

          Equations
          Instances For
            theorem FirstOrder.Language.Substructure.mem_closure {L : FirstOrder.Language} {M : Type w} [L.Structure M] {s : Set M} {x : M} :
            x (FirstOrder.Language.Substructure.closure L).toFun s ∀ (S : L.Substructure M), s Sx S
            @[simp]

            The substructure generated by a set includes the set.

            theorem FirstOrder.Language.Substructure.not_mem_of_not_mem_closure {L : FirstOrder.Language} {M : Type w} [L.Structure M] {s : Set M} {P : M} (hP : P(FirstOrder.Language.Substructure.closure L).toFun s) :
            Ps
            @[simp]
            theorem FirstOrder.Language.Substructure.closed {L : FirstOrder.Language} {M : Type w} [L.Structure M] (S : L.Substructure M) :
            @[simp]
            theorem FirstOrder.Language.Substructure.closure_le {L : FirstOrder.Language} {M : Type w} [L.Structure M] {S : L.Substructure M} {s : Set M} :

            A substructure S includes closure L s if and only if it includes s.

            Substructure closure of a set is monotone in its argument: if s ⊆ t, then closure L s ≤ closure L t.

            theorem FirstOrder.Language.Substructure.closure_eq_of_le {L : FirstOrder.Language} {M : Type w} [L.Structure M] {S : L.Substructure M} {s : Set M} (h₁ : s S) (h₂ : S (FirstOrder.Language.Substructure.closure L).toFun s) :
            theorem FirstOrder.Language.Substructure.mem_closure_iff_exists_term {L : FirstOrder.Language} {M : Type w} [L.Structure M] {s : Set M} {x : M} :
            x (FirstOrder.Language.Substructure.closure L).toFun s ∃ (t : L.Term s), FirstOrder.Language.Term.realize Subtype.val t = x
            theorem Set.Countable.substructure_closure (L : FirstOrder.Language) {M : Type w} [L.Structure M] {s : Set M} [Countable ((l : ) × L.Functions l)] (h : s.Countable) :
            theorem FirstOrder.Language.Substructure.closure_induction {L : FirstOrder.Language} {M : Type w} [L.Structure M] {s : Set M} {p : MProp} {x : M} (h : x (FirstOrder.Language.Substructure.closure L).toFun s) (Hs : xs, p x) (Hfun : ∀ {n : } (f : L.Functions n), FirstOrder.Language.ClosedUnder f (setOf p)) :
            p x

            An induction principle for closure membership. If p holds for all elements of s, and is preserved under function symbols, then p holds for all elements of the closure of s.

            theorem FirstOrder.Language.Substructure.dense_induction {L : FirstOrder.Language} {M : Type w} [L.Structure M] {p : MProp} (x : M) {s : Set M} (hs : (FirstOrder.Language.Substructure.closure L).toFun s = ) (Hs : xs, p x) (Hfun : ∀ {n : } (f : L.Functions n), FirstOrder.Language.ClosedUnder f (setOf p)) :
            p x

            If s is a dense set in a structure M, Substructure.closure L s = ⊤, then in order to prove that some predicate p holds for all x : M it suffices to verify p x for x ∈ s, and verify that p is preserved under function symbols.

            closure forms a Galois insertion with the coercion to set.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              @[simp]
              theorem FirstOrder.Language.Substructure.closure_eq {L : FirstOrder.Language} {M : Type w} [L.Structure M] (S : L.Substructure M) :

              Closure of a substructure S equals S.

              theorem FirstOrder.Language.Substructure.closure_unionᵢ {L : FirstOrder.Language} {M : Type w} [L.Structure M] {ι : Sort u_3} (s : ιSet M) :
              (FirstOrder.Language.Substructure.closure L).toFun (⋃ (i : ι), s i) = ⨆ (i : ι), (FirstOrder.Language.Substructure.closure L).toFun (s i)
              Equations
              • =

              comap and map #

              @[simp]
              theorem FirstOrder.Language.Substructure.comap_coe {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (φ : L.Hom M N) (S : L.Substructure N) :
              def FirstOrder.Language.Substructure.comap {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (φ : L.Hom M N) (S : L.Substructure N) :
              L.Substructure M

              The preimage of a substructure along a homomorphism is a substructure.

              Equations
              Instances For
                @[simp]
                theorem FirstOrder.Language.Substructure.mem_comap {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {S : L.Substructure N} {f : L.Hom M N} {x : M} :
                theorem FirstOrder.Language.Substructure.comap_comap {L : FirstOrder.Language} {M : Type w} {N : Type u_1} {P : Type u_2} [L.Structure M] [L.Structure N] [L.Structure P] (S : L.Substructure P) (g : L.Hom N P) (f : L.Hom M N) :
                @[simp]
                theorem FirstOrder.Language.Substructure.map_coe {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (φ : L.Hom M N) (S : L.Substructure M) :
                def FirstOrder.Language.Substructure.map {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (φ : L.Hom M N) (S : L.Substructure M) :
                L.Substructure N

                The image of a substructure along a homomorphism is a substructure.

                Equations
                Instances For
                  @[simp]
                  theorem FirstOrder.Language.Substructure.mem_map {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {f : L.Hom M N} {S : L.Substructure M} {y : N} :
                  theorem FirstOrder.Language.Substructure.mem_map_of_mem {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (f : L.Hom M N) {S : L.Substructure M} {x : M} (hx : x S) :
                  theorem FirstOrder.Language.Substructure.apply_coe_mem_map {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (f : L.Hom M N) (S : L.Substructure M) (x : S) :
                  theorem FirstOrder.Language.Substructure.map_map {L : FirstOrder.Language} {M : Type w} {N : Type u_1} {P : Type u_2} [L.Structure M] [L.Structure N] [L.Structure P] (S : L.Substructure M) (g : L.Hom N P) (f : L.Hom M N) :
                  theorem FirstOrder.Language.Substructure.map_le_iff_le_comap {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {f : L.Hom M N} {S : L.Substructure M} {T : L.Substructure N} :
                  theorem FirstOrder.Language.Substructure.map_le_of_le_comap {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (S : L.Substructure M) {T : L.Substructure N} {f : L.Hom M N} :
                  theorem FirstOrder.Language.Substructure.le_comap_of_map_le {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (S : L.Substructure M) {T : L.Substructure N} {f : L.Hom M N} :
                  theorem FirstOrder.Language.Substructure.le_comap_map {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (S : L.Substructure M) {f : L.Hom M N} :
                  theorem FirstOrder.Language.Substructure.map_comap_le {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {S : L.Substructure N} {f : L.Hom M N} :
                  theorem FirstOrder.Language.Substructure.monotone_map {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {f : L.Hom M N} :
                  theorem FirstOrder.Language.Substructure.monotone_comap {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {f : L.Hom M N} :
                  theorem FirstOrder.Language.Substructure.map_sup {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (S : L.Substructure M) (T : L.Substructure M) (f : L.Hom M N) :
                  theorem FirstOrder.Language.Substructure.map_iSup {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {ι : Sort u_3} (f : L.Hom M N) (s : ιL.Substructure M) :
                  theorem FirstOrder.Language.Substructure.comap_inf {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (S : L.Substructure N) (T : L.Substructure N) (f : L.Hom M N) :
                  theorem FirstOrder.Language.Substructure.comap_iInf {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {ι : Sort u_3} (f : L.Hom M N) (s : ιL.Substructure N) :
                  @[simp]
                  theorem FirstOrder.Language.Substructure.map_bot {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (f : L.Hom M N) :
                  @[simp]
                  theorem FirstOrder.Language.Substructure.comap_top {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (f : L.Hom M N) :
                  theorem FirstOrder.Language.Substructure.map_closure {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (f : L.Hom M N) (s : Set M) :
                  @[simp]
                  theorem FirstOrder.Language.Substructure.closure_image {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {s : Set M} (f : L.Hom M N) :

                  map f and comap f form a GaloisCoinsertion when f is injective.

                  Equations
                  Instances For
                    theorem FirstOrder.Language.Substructure.comap_map_eq_of_injective {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {f : L.Hom M N} (hf : Function.Injective f) (S : L.Substructure M) :
                    theorem FirstOrder.Language.Substructure.comap_inf_map_of_injective {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {f : L.Hom M N} (hf : Function.Injective f) (S : L.Substructure M) (T : L.Substructure M) :
                    theorem FirstOrder.Language.Substructure.comap_iInf_map_of_injective {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {ι : Type u_3} {f : L.Hom M N} (hf : Function.Injective f) (S : ιL.Substructure M) :
                    theorem FirstOrder.Language.Substructure.comap_sup_map_of_injective {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {f : L.Hom M N} (hf : Function.Injective f) (S : L.Substructure M) (T : L.Substructure M) :
                    theorem FirstOrder.Language.Substructure.comap_iSup_map_of_injective {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {ι : Type u_3} {f : L.Hom M N} (hf : Function.Injective f) (S : ιL.Substructure M) :
                    theorem FirstOrder.Language.Substructure.map_le_map_iff_of_injective {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {f : L.Hom M N} (hf : Function.Injective f) {S : L.Substructure M} {T : L.Substructure M} :

                    map f and comap f form a GaloisInsertion when f is surjective.

                    Equations
                    Instances For
                      theorem FirstOrder.Language.Substructure.map_comap_eq_of_surjective {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {f : L.Hom M N} (hf : Function.Surjective f) (S : L.Substructure N) :
                      theorem FirstOrder.Language.Substructure.map_inf_comap_of_surjective {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {f : L.Hom M N} (hf : Function.Surjective f) (S : L.Substructure N) (T : L.Substructure N) :
                      theorem FirstOrder.Language.Substructure.map_iInf_comap_of_surjective {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {ι : Type u_3} {f : L.Hom M N} (hf : Function.Surjective f) (S : ιL.Substructure N) :
                      theorem FirstOrder.Language.Substructure.map_sup_comap_of_surjective {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {f : L.Hom M N} (hf : Function.Surjective f) (S : L.Substructure N) (T : L.Substructure N) :
                      theorem FirstOrder.Language.Substructure.map_iSup_comap_of_surjective {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {ι : Type u_3} {f : L.Hom M N} (hf : Function.Surjective f) (S : ιL.Substructure N) :
                      theorem FirstOrder.Language.Substructure.comap_le_comap_iff_of_surjective {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {f : L.Hom M N} (hf : Function.Surjective f) {S : L.Substructure N} {T : L.Substructure N} :
                      instance FirstOrder.Language.Substructure.inducedStructure {L : FirstOrder.Language} {M : Type w} [L.Structure M] {S : L.Substructure M} :
                      L.Structure S
                      Equations
                      • One or more equations did not get rendered due to their size.
                      def FirstOrder.Language.Substructure.subtype {L : FirstOrder.Language} {M : Type w} [L.Structure M] (S : L.Substructure M) :
                      L.Embedding (S) M

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

                      Equations
                      • S.subtype = { toFun := Subtype.val, inj' := , map_fun' := , map_rel' := }
                      Instances For
                        @[simp]
                        theorem FirstOrder.Language.Substructure.coeSubtype {L : FirstOrder.Language} {M : Type w} [L.Structure M] (S : L.Substructure M) :
                        S.subtype = Subtype.val
                        def FirstOrder.Language.Substructure.topEquiv {L : FirstOrder.Language} {M : Type w} [L.Structure M] :
                        L.Equiv () M

                        The equivalence between the maximal substructure of a structure and the structure itself.

                        Equations
                        • FirstOrder.Language.Substructure.topEquiv = { toFun := .subtype, invFun := fun (m : M) => m, , left_inv := , right_inv := , map_fun' := , map_rel' := }
                        Instances For
                          @[simp]
                          theorem FirstOrder.Language.Substructure.coe_topEquiv {L : FirstOrder.Language} {M : Type w} [L.Structure M] :
                          FirstOrder.Language.Substructure.topEquiv = Subtype.val
                          @[simp]
                          theorem FirstOrder.Language.Substructure.realize_boundedFormula_top {L : FirstOrder.Language} {M : Type w} [L.Structure M] {α : Type u_3} {n : } {φ : L.BoundedFormula α n} {v : α} {xs : Fin n} :
                          φ.Realize v xs φ.Realize (Subtype.val v) (Subtype.val xs)
                          @[simp]
                          theorem FirstOrder.Language.Substructure.realize_formula_top {L : FirstOrder.Language} {M : Type w} [L.Structure M] {α : Type u_3} {φ : L.Formula α} {v : α} :
                          φ.Realize v φ.Realize (Subtype.val v)
                          theorem FirstOrder.Language.Substructure.closure_induction' {L : FirstOrder.Language} {M : Type w} [L.Structure M] (s : Set M) {p : (x : M) → x (FirstOrder.Language.Substructure.closure L).toFun sProp} (Hs : ∀ (x : M) (h : x s), p x ) (Hfun : ∀ {n : } (f : L.Functions n), FirstOrder.Language.ClosedUnder f {x : M | ∃ (hx : x (FirstOrder.Language.Substructure.closure L).toFun s), p x hx}) {x : M} (hx : x (FirstOrder.Language.Substructure.closure L).toFun s) :
                          p x hx

                          A dependent version of Substructure.closure_induction.

                          def FirstOrder.Language.LHom.substructureReduct {L : FirstOrder.Language} {M : Type w} [L.Structure M] {L' : FirstOrder.Language} [L'.Structure M] (φ : L →ᴸ L') [φ.IsExpansionOn M] :
                          L'.Substructure M ↪o L.Substructure M

                          Reduces the language of a substructure along a language hom.

                          Equations
                          • φ.substructureReduct = { toFun := fun (S : L'.Substructure M) => { carrier := S, fun_mem := }, inj' := , map_rel_iff' := }
                          Instances For
                            @[simp]
                            theorem FirstOrder.Language.LHom.mem_substructureReduct {L : FirstOrder.Language} {M : Type w} [L.Structure M] {L' : FirstOrder.Language} [L'.Structure M] (φ : L →ᴸ L') [φ.IsExpansionOn M] {x : M} {S : L'.Substructure M} :
                            x φ.substructureReduct S x S
                            @[simp]
                            theorem FirstOrder.Language.LHom.coe_substructureReduct {L : FirstOrder.Language} {M : Type w} [L.Structure M] {L' : FirstOrder.Language} [L'.Structure M] (φ : L →ᴸ L') [φ.IsExpansionOn M] {S : L'.Substructure M} :
                            (φ.substructureReduct S) = S
                            def FirstOrder.Language.Substructure.withConstants {L : FirstOrder.Language} {M : Type w} [L.Structure M] (S : L.Substructure M) {A : Set M} (h : A S) :
                            (L.withConstants A).Substructure M

                            Turns any substructure containing a constant set A into a L[[A]]-substructure.

                            Equations
                            • S.withConstants h = { carrier := S, fun_mem := }
                            Instances For
                              @[simp]
                              theorem FirstOrder.Language.Substructure.mem_withConstants {L : FirstOrder.Language} {M : Type w} [L.Structure M] {S : L.Substructure M} {A : Set M} (h : A S) {x : M} :
                              x S.withConstants h x S
                              @[simp]
                              theorem FirstOrder.Language.Substructure.coe_withConstants {L : FirstOrder.Language} {M : Type w} [L.Structure M] {S : L.Substructure M} {A : Set M} (h : A S) :
                              (S.withConstants h) = S
                              @[simp]
                              theorem FirstOrder.Language.Substructure.reduct_withConstants {L : FirstOrder.Language} {M : Type w} [L.Structure M] {S : L.Substructure M} {A : Set M} (h : A S) :
                              (L.lhomWithConstants A).substructureReduct (S.withConstants h) = S
                              theorem FirstOrder.Language.Substructure.subset_closure_withConstants {L : FirstOrder.Language} {M : Type w} [L.Structure M] {A : Set M} {s : Set M} :
                              A ((FirstOrder.Language.Substructure.closure (L.withConstants A)).toFun s)
                              theorem FirstOrder.Language.Substructure.closure_withConstants_eq {L : FirstOrder.Language} {M : Type w} [L.Structure M] {A : Set M} {s : Set M} :
                              (FirstOrder.Language.Substructure.closure (L.withConstants A)).toFun s = ((FirstOrder.Language.Substructure.closure L).toFun (A s)).withConstants
                              @[simp]
                              theorem FirstOrder.Language.Hom.domRestrict_toFun {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (f : L.Hom M N) (p : L.Substructure M) :
                              ∀ (a : p), (f.domRestrict p) a = f a
                              def FirstOrder.Language.Hom.domRestrict {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (f : L.Hom M N) (p : L.Substructure M) :
                              L.Hom (p) N

                              The restriction of a first-order hom to a substructure s ⊆ M gives a hom s → N.

                              Equations
                              • f.domRestrict p = f.comp p.subtype.toHom
                              Instances For
                                @[simp]
                                theorem FirstOrder.Language.Hom.codRestrict_toFun_coe {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (p : L.Substructure N) (f : L.Hom M N) (h : ∀ (c : M), f c p) (c : M) :
                                def FirstOrder.Language.Hom.codRestrict {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (p : L.Substructure N) (f : L.Hom M N) (h : ∀ (c : M), f c p) :
                                L.Hom M p

                                A first-order hom f : M → N whose values lie in a substructure p ⊆ N can be restricted to a hom M → p.

                                Equations
                                Instances For
                                  @[simp]
                                  theorem FirstOrder.Language.Hom.comp_codRestrict {L : FirstOrder.Language} {M : Type w} {N : Type u_1} {P : Type u_2} [L.Structure M] [L.Structure N] [L.Structure P] (f : L.Hom M N) (g : L.Hom N P) (p : L.Substructure P) (h : ∀ (b : N), g b p) :
                                  @[simp]
                                  theorem FirstOrder.Language.Hom.subtype_comp_codRestrict {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (f : L.Hom M N) (p : L.Substructure N) (h : ∀ (b : M), f b p) :
                                  p.subtype.toHom.comp (FirstOrder.Language.Hom.codRestrict p f h) = f
                                  def FirstOrder.Language.Hom.range {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (f : L.Hom M N) :
                                  L.Substructure N

                                  The range of a first-order hom f : M → N is a submodule of N. See Note [range copy pattern].

                                  Equations
                                  Instances For
                                    theorem FirstOrder.Language.Hom.range_coe {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (f : L.Hom M N) :
                                    f.range = Set.range f
                                    @[simp]
                                    theorem FirstOrder.Language.Hom.mem_range {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {f : L.Hom M N} {x : N} :
                                    x f.range ∃ (y : M), f y = x
                                    theorem FirstOrder.Language.Hom.range_eq_map {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (f : L.Hom M N) :
                                    theorem FirstOrder.Language.Hom.mem_range_self {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (f : L.Hom M N) (x : M) :
                                    f x f.range
                                    @[simp]
                                    theorem FirstOrder.Language.Hom.range_comp {L : FirstOrder.Language} {M : Type w} {N : Type u_1} {P : Type u_2} [L.Structure M] [L.Structure N] [L.Structure P] (f : L.Hom M N) (g : L.Hom N P) :
                                    (g.comp f).range = FirstOrder.Language.Substructure.map g f.range
                                    theorem FirstOrder.Language.Hom.range_comp_le_range {L : FirstOrder.Language} {M : Type w} {N : Type u_1} {P : Type u_2} [L.Structure M] [L.Structure N] [L.Structure P] (f : L.Hom M N) (g : L.Hom N P) :
                                    (g.comp f).range g.range
                                    theorem FirstOrder.Language.Hom.range_eq_top {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {f : L.Hom M N} :
                                    theorem FirstOrder.Language.Hom.range_le_iff_comap {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {f : L.Hom M N} {p : L.Substructure N} :
                                    theorem FirstOrder.Language.Hom.map_le_range {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {f : L.Hom M N} {p : L.Substructure M} :
                                    def FirstOrder.Language.Hom.eqLocus {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (f : L.Hom M N) (g : L.Hom M N) :
                                    L.Substructure M

                                    The substructure of elements x : M such that f x = g x

                                    Equations
                                    • f.eqLocus g = { carrier := {x : M | f x = g x}, fun_mem := }
                                    Instances For
                                      theorem FirstOrder.Language.Hom.eqOn_closure {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {f : L.Hom M N} {g : L.Hom M N} {s : Set M} (h : Set.EqOn (f) (g) s) :

                                      If two L.Homs are equal on a set, then they are equal on its substructure closure.

                                      theorem FirstOrder.Language.Hom.eq_of_eqOn_top {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {f : L.Hom M N} {g : L.Hom M N} (h : Set.EqOn f g ) :
                                      f = g
                                      theorem FirstOrder.Language.Hom.eq_of_eqOn_dense {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {s : Set M} (hs : (FirstOrder.Language.Substructure.closure L).toFun s = ) {f : L.Hom M N} {g : L.Hom M N} (h : Set.EqOn (f) (g) s) :
                                      f = g
                                      def FirstOrder.Language.Embedding.domRestrict {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (f : L.Embedding M N) (p : L.Substructure M) :
                                      L.Embedding (p) N

                                      The restriction of a first-order embedding to a substructure s ⊆ M gives an embedding s → N.

                                      Equations
                                      • f.domRestrict p = f.comp p.subtype
                                      Instances For
                                        @[simp]
                                        theorem FirstOrder.Language.Embedding.domRestrict_apply {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (f : L.Embedding M N) (p : L.Substructure M) (x : p) :
                                        (f.domRestrict p) x = f x
                                        def FirstOrder.Language.Embedding.codRestrict {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (p : L.Substructure N) (f : L.Embedding M N) (h : ∀ (c : M), f c p) :
                                        L.Embedding M p

                                        A first-order embedding f : M → N whose values lie in a substructure p ⊆ N can be restricted to an embedding M → p.

                                        Equations
                                        Instances For
                                          @[simp]
                                          theorem FirstOrder.Language.Embedding.codRestrict_apply {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (p : L.Substructure N) (f : L.Embedding M N) {h : ∀ (c : M), f c p} (x : M) :
                                          @[simp]
                                          theorem FirstOrder.Language.Embedding.codRestrict_apply' {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (p : L.Substructure N) (f : L.Embedding M N) {h : ∀ (c : M), f c p} (x : M) :
                                          @[simp]
                                          theorem FirstOrder.Language.Embedding.comp_codRestrict {L : FirstOrder.Language} {M : Type w} {N : Type u_1} {P : Type u_2} [L.Structure M] [L.Structure N] [L.Structure P] (f : L.Embedding M N) (g : L.Embedding N P) (p : L.Substructure P) (h : ∀ (b : N), g b p) :
                                          @[simp]
                                          theorem FirstOrder.Language.Embedding.subtype_comp_codRestrict {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (f : L.Embedding M N) (p : L.Substructure N) (h : ∀ (b : M), f b p) :
                                          noncomputable def FirstOrder.Language.Embedding.substructureEquivMap {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (f : L.Embedding M N) (s : L.Substructure M) :
                                          L.Equiv s (FirstOrder.Language.Substructure.map f.toHom s)

                                          The equivalence between a substructure s and its image s.map f.toHom, where f is an embedding.

                                          Equations
                                          • One or more equations did not get rendered due to their size.
                                          Instances For
                                            @[simp]
                                            theorem FirstOrder.Language.Embedding.substructureEquivMap_apply {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (f : L.Embedding M N) (p : L.Substructure M) (x : p) :
                                            ((f.substructureEquivMap p) x) = f x
                                            @[simp]
                                            theorem FirstOrder.Language.Embedding.subtype_substructureEquivMap {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (f : L.Embedding M N) (s : L.Substructure M) :
                                            (FirstOrder.Language.Substructure.map f.toHom s).subtype.comp (f.substructureEquivMap s).toEmbedding = f.comp s.subtype
                                            noncomputable def FirstOrder.Language.Embedding.equivRange {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (f : L.Embedding M N) :
                                            L.Equiv M f.toHom.range

                                            The equivalence between the domain and the range of an embedding f.

                                            Equations
                                            • One or more equations did not get rendered due to their size.
                                            Instances For
                                              @[simp]
                                              theorem FirstOrder.Language.Embedding.equivRange_apply {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (f : L.Embedding M N) (x : M) :
                                              (f.equivRange x) = f x
                                              @[simp]
                                              theorem FirstOrder.Language.Embedding.subtype_equivRange {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (f : L.Embedding M N) :
                                              f.toHom.range.subtype.comp f.equivRange.toEmbedding = f
                                              theorem FirstOrder.Language.Equiv.toHom_range {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (f : L.Equiv M N) :
                                              f.toHom.range =
                                              def FirstOrder.Language.Substructure.inclusion {L : FirstOrder.Language} {M : Type w} [L.Structure M] {S : L.Substructure M} {T : L.Substructure M} (h : S T) :
                                              L.Embedding S T

                                              The embedding associated to an inclusion of substructures.

                                              Equations
                                              Instances For
                                                @[simp]
                                                theorem FirstOrder.Language.Substructure.coe_inclusion {L : FirstOrder.Language} {M : Type w} [L.Structure M] {S : L.Substructure M} {T : L.Substructure M} (h : S T) :
                                                theorem FirstOrder.Language.Substructure.range_subtype {L : FirstOrder.Language} {M : Type w} [L.Structure M] (S : L.Substructure M) :
                                                S.subtype.toHom.range = S