Documentation

Mathlib.ModelTheory.PartialEquiv

Partial Isomorphisms #

This file defines partial isomorphisms between first-order structures.

Main Definitions #

Main Results #

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

A partial L-equivalence, implemented as an equivalence between substructures.

  • dom : L.Substructure M

    The substructure which is the domain of the equivalence.

  • cod : L.Substructure N

    The substructure which is the codomain of the equivalence.

  • toEquiv : L.Equiv self.dom self.cod

    The equivalence between the two subdomains.

Instances For

    A partial L-equivalence, implemented as an equivalence between substructures.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      noncomputable instance FirstOrder.Language.PartialEquiv.instInhabited_self {L : FirstOrder.Language} {M : Type w} [L.Structure M] :
      Inhabited (L.PartialEquiv M M)
      Equations
      def FirstOrder.Language.PartialEquiv.symm {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (f : L.PartialEquiv M N) :
      L.PartialEquiv N M

      Maps to the symmetric partial equivalence.

      Equations
      • f.symm = { dom := f.cod, cod := f.dom, toEquiv := f.toEquiv.symm }
      Instances For
        @[simp]
        theorem FirstOrder.Language.PartialEquiv.symm_symm {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (f : L.PartialEquiv M N) :
        f.symm.symm = f
        @[simp]
        theorem FirstOrder.Language.PartialEquiv.symm_apply {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (f : L.PartialEquiv M N) (x : f.cod) :
        f.symm.toEquiv x = f.toEquiv.symm x
        instance FirstOrder.Language.PartialEquiv.instLE {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] :
        LE (L.PartialEquiv M N)
        Equations
        • One or more equations did not get rendered due to their size.
        theorem FirstOrder.Language.PartialEquiv.le_def {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (f : L.PartialEquiv M N) (g : L.PartialEquiv M N) :
        f g ∃ (h : f.dom g.dom), g.cod.subtype.comp (g.toEquiv.toEmbedding.comp (FirstOrder.Language.Substructure.inclusion h)) = f.cod.subtype.comp f.toEquiv.toEmbedding
        theorem FirstOrder.Language.PartialEquiv.dom_le_dom {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {f : L.PartialEquiv M N} {g : L.PartialEquiv M N} :
        f gf.dom g.dom
        theorem FirstOrder.Language.PartialEquiv.cod_le_cod {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {f : L.PartialEquiv M N} {g : L.PartialEquiv M N} :
        f gf.cod g.cod
        theorem FirstOrder.Language.PartialEquiv.subtype_toEquiv_inclusion {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {f : L.PartialEquiv M N} {g : L.PartialEquiv M N} (h : f g) :
        g.cod.subtype.comp (g.toEquiv.toEmbedding.comp (FirstOrder.Language.Substructure.inclusion )) = f.cod.subtype.comp f.toEquiv.toEmbedding
        theorem FirstOrder.Language.PartialEquiv.toEquiv_inclusion {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {f : L.PartialEquiv M N} {g : L.PartialEquiv M N} (h : f g) :
        g.toEquiv.toEmbedding.comp (FirstOrder.Language.Substructure.inclusion ) = (FirstOrder.Language.Substructure.inclusion ).comp f.toEquiv.toEmbedding
        theorem FirstOrder.Language.PartialEquiv.toEquiv_inclusion_apply {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {f : L.PartialEquiv M N} {g : L.PartialEquiv M N} (h : f g) (x : f.dom) :
        theorem FirstOrder.Language.PartialEquiv.le_iff {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {f : L.PartialEquiv M N} {g : L.PartialEquiv M N} :
        f g ∃ (dom_le_dom : f.dom g.dom) (cod_le_cod : f.cod g.cod), ∀ (x : f.dom), (FirstOrder.Language.Substructure.inclusion cod_le_cod) (f.toEquiv x) = g.toEquiv ((FirstOrder.Language.Substructure.inclusion dom_le_dom) x)
        theorem FirstOrder.Language.PartialEquiv.le_trans {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (f : L.PartialEquiv M N) (g : L.PartialEquiv M N) (h : L.PartialEquiv M N) :
        f gg hf h
        instance FirstOrder.Language.PartialEquiv.instPartialOrder {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] :
        PartialOrder (L.PartialEquiv M N)
        Equations
        theorem FirstOrder.Language.PartialEquiv.symm_le_symm {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {f : L.PartialEquiv M N} {g : L.PartialEquiv M N} (hfg : f g) :
        f.symm g.symm
        theorem FirstOrder.Language.PartialEquiv.monotone_symm {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] :
        Monotone fun (f : L.PartialEquiv M N) => f.symm
        theorem FirstOrder.Language.PartialEquiv.symm_le_iff {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {f : L.PartialEquiv M N} {g : L.PartialEquiv N M} :
        f.symm g f g.symm
        theorem FirstOrder.Language.PartialEquiv.ext {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {f : L.PartialEquiv M N} {g : L.PartialEquiv M N} (h_dom : f.dom = g.dom) :
        (∀ (x : M) (h : x f.dom), f.cod.subtype (f.toEquiv x, h) = g.cod.subtype (g.toEquiv x, ))f = g
        theorem FirstOrder.Language.PartialEquiv.ext_iff {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {f : L.PartialEquiv M N} {g : L.PartialEquiv M N} :
        f = g ∃ (h_dom : f.dom = g.dom), ∀ (x : M) (h : x f.dom), f.cod.subtype (f.toEquiv x, h) = g.cod.subtype (g.toEquiv x, )
        theorem FirstOrder.Language.PartialEquiv.monotone_dom {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] :
        Monotone fun (f : L.PartialEquiv M N) => f.dom
        theorem FirstOrder.Language.PartialEquiv.monotone_cod {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] :
        Monotone fun (f : L.PartialEquiv M N) => f.cod
        noncomputable def FirstOrder.Language.PartialEquiv.domRestrict {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (f : L.PartialEquiv M N) {A : L.Substructure M} (h : A f.dom) :
        L.PartialEquiv M N

        Restriction of a partial equivalence to a substructure of the domain.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          theorem FirstOrder.Language.PartialEquiv.domRestrict_le {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (f : L.PartialEquiv M N) {A : L.Substructure M} (h : A f.dom) :
          f.domRestrict h f
          theorem FirstOrder.Language.PartialEquiv.le_domRestrict {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (f : L.PartialEquiv M N) (g : L.PartialEquiv M N) {A : L.Substructure M} (hf : f.dom A) (hg : A g.dom) (hfg : f g) :
          f g.domRestrict hg
          noncomputable def FirstOrder.Language.PartialEquiv.codRestrict {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (f : L.PartialEquiv M N) {A : L.Substructure N} (h : A f.cod) :
          L.PartialEquiv M N

          Restriction of a partial equivalence to a substructure of the codomain.

          Equations
          • f.codRestrict h = (f.symm.domRestrict h).symm
          Instances For
            theorem FirstOrder.Language.PartialEquiv.codRestrict_le {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (f : L.PartialEquiv M N) {A : L.Substructure N} (h : A f.cod) :
            f.codRestrict h f
            theorem FirstOrder.Language.PartialEquiv.le_codRestrict {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (f : L.PartialEquiv M N) (g : L.PartialEquiv M N) {A : L.Substructure N} (hf : f.cod A) (hg : A g.cod) (hfg : f g) :
            f g.codRestrict hg
            def FirstOrder.Language.PartialEquiv.toEmbedding {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (f : L.PartialEquiv M N) :
            L.Embedding (↥f.dom) N

            A partial equivalence as an embedding from its domain.

            Equations
            • f.toEmbedding = f.cod.subtype.comp f.toEquiv.toEmbedding
            Instances For
              @[simp]
              theorem FirstOrder.Language.PartialEquiv.toEmbedding_apply {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {f : L.PartialEquiv M N} (m : f.dom) :
              f.toEmbedding m = (f.toEquiv m)
              def FirstOrder.Language.PartialEquiv.toEmbeddingOfEqTop {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {f : L.PartialEquiv M N} (h : f.dom = ) :
              L.Embedding M N

              Given a partial equivalence which has the whole structure as domain, returns the corresponding embedding.

              Equations
              Instances For
                @[simp]
                theorem FirstOrder.Language.PartialEquiv.toEmbeddingOfEqTop__apply {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {f : L.PartialEquiv M N} (h : f.dom = ) (m : M) :
                (FirstOrder.Language.PartialEquiv.toEmbeddingOfEqTop h) m = (f.toEquiv m, )
                def FirstOrder.Language.PartialEquiv.toEquivOfEqTop {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {f : L.PartialEquiv M N} (h_dom : f.dom = ) (h_cod : f.cod = ) :
                L.Equiv M N

                Given a partial equivalence which has the whole structure as domain and as codomain, returns the corresponding equivalence.

                Equations
                Instances For
                  @[simp]
                  theorem FirstOrder.Language.PartialEquiv.toEquivOfEqTop_toEmbedding {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {f : L.PartialEquiv M N} (h_dom : f.dom = ) (h_cod : f.cod = ) :
                  theorem FirstOrder.Language.PartialEquiv.dom_fg_iff_cod_fg {L : FirstOrder.Language} {M : Type w} [L.Structure M] {N : Type u_2} [L.Structure N] (f : L.PartialEquiv M N) :
                  f.dom.FG f.cod.FG
                  noncomputable def FirstOrder.Language.Embedding.toPartialEquiv {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (f : L.Embedding M N) :
                  L.PartialEquiv M N

                  Given an embedding, returns the corresponding partial equivalence with as domain.

                  Equations
                  • f.toPartialEquiv = { dom := , cod := f.toHom.range, toEquiv := f.equivRange.comp FirstOrder.Language.Substructure.topEquiv }
                  Instances For
                    theorem FirstOrder.Language.Embedding.toPartialEquiv_injective {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] :
                    Function.Injective fun (f : L.Embedding M N) => f.toPartialEquiv
                    @[simp]
                    theorem FirstOrder.Language.Embedding.toEmbedding_toPartialEquiv {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.toPartialEquiv_toEmbedding {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {f : L.PartialEquiv M N} (h : f.dom = ) :
                    instance FirstOrder.Language.DirectLimit.instDirectedSystemSubtypeMemSubstructureDomCoeOrderHomPartialEquivEmbeddingInclusion {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {ι : Type u_2} [Preorder ι] (S : ι →o L.PartialEquiv M N) :
                    DirectedSystem (fun (i : ι) => (S i).dom) fun (x x_1 : ι) (h : x x_1) => (FirstOrder.Language.Substructure.inclusion )
                    Equations
                    • =
                    instance FirstOrder.Language.DirectLimit.instDirectedSystemSubtypeMemSubstructureCodCoeOrderHomPartialEquivEmbeddingInclusion {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {ι : Type u_2} [Preorder ι] (S : ι →o L.PartialEquiv M N) :
                    DirectedSystem (fun (i : ι) => (S i).cod) fun (x x_1 : ι) (h : x x_1) => (FirstOrder.Language.Substructure.inclusion )
                    Equations
                    • =
                    noncomputable def FirstOrder.Language.DirectLimit.partialEquivLimit {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {ι : Type u_2} [Preorder ι] [Nonempty ι] [IsDirected ι fun (x1 x2 : ι) => x1 x2] (S : ι →o L.PartialEquiv M N) :
                    L.PartialEquiv M N

                    The limit of a directed system of PartialEquivs.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      @[simp]
                      theorem FirstOrder.Language.DirectLimit.dom_partialEquivLimit {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {ι : Type u_2} [Preorder ι] [Nonempty ι] [IsDirected ι fun (x1 x2 : ι) => x1 x2] (S : ι →o L.PartialEquiv M N) :
                      @[simp]
                      theorem FirstOrder.Language.DirectLimit.cod_partialEquivLimit {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {ι : Type u_2} [Preorder ι] [Nonempty ι] [IsDirected ι fun (x1 x2 : ι) => x1 x2] (S : ι →o L.PartialEquiv M N) :
                      @[simp]
                      theorem FirstOrder.Language.DirectLimit.partialEquivLimit_comp_inclusion {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {ι : Type u_2} [Preorder ι] [Nonempty ι] [IsDirected ι fun (x1 x2 : ι) => x1 x2] (S : ι →o L.PartialEquiv M N) {i : ι} :
                      theorem FirstOrder.Language.DirectLimit.le_partialEquivLimit {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {ι : Type u_2} [Preorder ι] [Nonempty ι] [IsDirected ι fun (x1 x2 : ι) => x1 x2] (S : ι →o L.PartialEquiv M N) (i : ι) :
                      @[reducible, inline]
                      abbrev FirstOrder.Language.FGEquiv (L : FirstOrder.Language) (M : Type w) (N : Type w') [L.Structure M] [L.Structure N] :
                      Type (max 0 w w')

                      The type of equivalences between finitely generated substructures.

                      Equations
                      • L.FGEquiv M N = { f : L.PartialEquiv M N // f.dom.FG }
                      Instances For
                        def FirstOrder.Language.IsExtensionPair (L : FirstOrder.Language) (M : Type w) (N : Type w') [L.Structure M] [L.Structure N] :

                        Two structures M and N form an extension pair if the domain of any finitely-generated map from M to N can be extended to include any element of M.

                        Equations
                        • L.IsExtensionPair M N = ∀ (f : L.FGEquiv M N) (m : M), ∃ (g : L.FGEquiv M N), m (↑g).dom f g
                        Instances For
                          instance FirstOrder.Language.inhabited_self_FGEquiv {L : FirstOrder.Language} {M : Type w} [L.Structure M] :
                          Inhabited (L.FGEquiv M M)
                          Equations
                          instance FirstOrder.Language.inhabited_FGEquiv_of_IsEmpty_Constants_and_Relations {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [IsEmpty L.Constants] [IsEmpty (L.Relations 0)] [L.Structure N] :
                          Inhabited (L.FGEquiv M N)
                          Equations
                          • One or more equations did not get rendered due to their size.
                          @[simp]
                          theorem FirstOrder.Language.FGEquiv.symm_coe {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (f : L.FGEquiv M N) :
                          f.symm = (↑f).symm
                          def FirstOrder.Language.FGEquiv.symm {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (f : L.FGEquiv M N) :
                          L.FGEquiv N M

                          Maps to the symmetric finitely-generated partial equivalence.

                          Equations
                          • f.symm = (↑f).symm,
                          Instances For
                            theorem FirstOrder.Language.isExtensionPair_iff_cod {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] :
                            L.IsExtensionPair M N ∀ (f : L.FGEquiv N M) (m : M), ∃ (g : L.FGEquiv N M), m (↑g).cod f g
                            theorem FirstOrder.Language.isExtensionPair_iff_exists_embedding_closure_singleton_sup {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] :
                            L.IsExtensionPair M N ∀ (S : L.Substructure M), S.FG∀ (f : L.Embedding (↥S) N) (m : M), ∃ (g : L.Embedding (↥((FirstOrder.Language.Substructure.closure L).toFun {m} S)) N), f = g.comp (FirstOrder.Language.Substructure.inclusion )

                            An alternate characterization of an extension pair is that every finitely generated partial isomorphism can be extended to include any particular element of the domain.

                            theorem FirstOrder.Language.IsExtensionPair.cod {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] :
                            L.IsExtensionPair M N∀ (f : L.FGEquiv N M) (m : M), ∃ (g : L.FGEquiv N M), m (↑g).cod f g

                            Alias of the forward direction of FirstOrder.Language.isExtensionPair_iff_cod.

                            def FirstOrder.Language.IsExtensionPair.definedAtLeft {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (h : L.IsExtensionPair M N) (m : M) :
                            Order.Cofinal (L.FGEquiv M N)

                            The cofinal set of finite equivalences with a given element in their domain.

                            Equations
                            • h.definedAtLeft m = { carrier := {f : L.FGEquiv M N | m (↑f).dom}, mem_gt := }
                            Instances For
                              def FirstOrder.Language.IsExtensionPair.definedAtRight {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (h : L.IsExtensionPair N M) (n : N) :
                              Order.Cofinal (L.FGEquiv M N)

                              The cofinal set of finite equivalences with a given element in their codomain.

                              Equations
                              • h.definedAtRight n = { carrier := {f : L.FGEquiv M N | n (↑f).cod}, mem_gt := }
                              Instances For
                                theorem FirstOrder.Language.embedding_from_cg {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (M_cg : FirstOrder.Language.Structure.CG L M) (g : L.FGEquiv M N) (H : L.IsExtensionPair M N) :
                                ∃ (f : L.Embedding M N), g f.toPartialEquiv

                                For a countably generated structure M and a structure N, if any partial equivalence between finitely generated substructures can be extended to any element in the domain, then there exists an embedding of M in N.

                                theorem FirstOrder.Language.equiv_between_cg {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (M_cg : FirstOrder.Language.Structure.CG L M) (N_cg : FirstOrder.Language.Structure.CG L N) (g : L.FGEquiv M N) (ext_dom : L.IsExtensionPair M N) (ext_cod : L.IsExtensionPair N M) :
                                ∃ (f : L.Equiv M N), g f.toEmbedding.toPartialEquiv

                                For two countably generated structure M and N, if any PartialEquiv between finitely generated substructures can be extended to any element in the domain and to any element in the codomain, then there exists an equivalence between M and N.