Documentation

Mathlib.ModelTheory.PartialEquiv

Partial Isomorphisms #

This file defines partial isomorphisms between first-order structures.

Main Definitions #

Main Results #

structure FirstOrder.Language.PartialEquiv (L : 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.

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

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

Maps to the symmetric partial equivalence.

Equations
@[simp]
theorem FirstOrder.Language.PartialEquiv.symm_symm {L : 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 : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (f : L.PartialEquiv M N) (x : f.cod) :
instance FirstOrder.Language.PartialEquiv.instLE {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] :
Equations
  • One or more equations did not get rendered due to their size.
theorem FirstOrder.Language.PartialEquiv.dom_le_dom {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {f g : L.PartialEquiv M N} :
f gf.dom g.dom
theorem FirstOrder.Language.PartialEquiv.cod_le_cod {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {f g : L.PartialEquiv M N} :
f gf.cod g.cod
theorem FirstOrder.Language.PartialEquiv.toEquiv_inclusion_apply {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {f g : L.PartialEquiv M N} (h : f g) (x : f.dom) :
theorem FirstOrder.Language.PartialEquiv.le_iff {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {f g : L.PartialEquiv M N} :
f g ∃ (dom_le_dom : f.dom g.dom) (cod_le_cod : f.cod g.cod), ∀ (x : f.dom), (Substructure.inclusion cod_le_cod) (f.toEquiv x) = g.toEquiv ((Substructure.inclusion dom_le_dom) x)
theorem FirstOrder.Language.PartialEquiv.le_trans {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (f g h : L.PartialEquiv M N) :
f gg hf h
Equations
  • One or more equations did not get rendered due to their size.
theorem FirstOrder.Language.PartialEquiv.symm_le_symm {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {f g : L.PartialEquiv M N} (hfg : f g) :
theorem FirstOrder.Language.PartialEquiv.symm_le_iff {L : 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 : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {f 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 : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {f 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 : 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 : 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 : 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) :

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

Equations
  • One or more equations did not get rendered due to their size.
theorem FirstOrder.Language.PartialEquiv.domRestrict_le {L : 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) :
theorem FirstOrder.Language.PartialEquiv.le_domRestrict {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (f g : L.PartialEquiv M N) {A : L.Substructure M} (hf : f.dom A) (hg : A g.dom) (hfg : f g) :
noncomputable def FirstOrder.Language.PartialEquiv.codRestrict {L : 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) :

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

Equations
theorem FirstOrder.Language.PartialEquiv.codRestrict_le {L : 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) :
theorem FirstOrder.Language.PartialEquiv.le_codRestrict {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (f g : L.PartialEquiv M N) {A : L.Substructure N} (hf : f.cod A) (hg : A g.cod) (hfg : f g) :
def FirstOrder.Language.PartialEquiv.toEmbedding {L : 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
@[simp]
theorem FirstOrder.Language.PartialEquiv.toEmbedding_apply {L : 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 : 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
@[simp]
theorem FirstOrder.Language.PartialEquiv.toEmbeddingOfEqTop_apply {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {f : L.PartialEquiv M N} (h : f.dom = ) (m : M) :
(toEmbeddingOfEqTop h) m = (f.toEquiv m, )
@[deprecated FirstOrder.Language.PartialEquiv.toEmbeddingOfEqTop_apply (since := "2024-11-30")]
theorem FirstOrder.Language.PartialEquiv.toEmbeddingOfEqTop__apply {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {f : L.PartialEquiv M N} (h : f.dom = ) (m : M) :
(toEmbeddingOfEqTop h) m = (f.toEquiv m, )

Alias of FirstOrder.Language.PartialEquiv.toEmbeddingOfEqTop_apply.

def FirstOrder.Language.PartialEquiv.toEquivOfEqTop {L : 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
@[simp]
theorem FirstOrder.Language.PartialEquiv.toEquivOfEqTop_toEmbedding {L : 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 = ) :
noncomputable def FirstOrder.Language.Embedding.toPartialEquiv {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (f : L.Embedding M N) :

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

Equations
instance FirstOrder.Language.DirectLimit.instDirectedSystemSubtypeMemSubstructureDomCoeOrderHomPartialEquivEmbeddingInclusion {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {ι : Type u_1} [Preorder ι] (S : ι →o L.PartialEquiv M N) :
DirectedSystem (fun (i : ι) => (S i).dom) fun (x x_1 : ι) (h : x x_1) => (Substructure.inclusion )
instance FirstOrder.Language.DirectLimit.instDirectedSystemSubtypeMemSubstructureCodCoeOrderHomPartialEquivEmbeddingInclusion {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {ι : Type u_1} [Preorder ι] (S : ι →o L.PartialEquiv M N) :
DirectedSystem (fun (i : ι) => (S i).cod) fun (x x_1 : ι) (h : x x_1) => (Substructure.inclusion )
noncomputable def FirstOrder.Language.DirectLimit.partialEquivLimit {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {ι : Type u_1} [Preorder ι] [Nonempty ι] [IsDirected ι fun (x1 x2 : ι) => x1 x2] (S : ι →o 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.
@[simp]
theorem FirstOrder.Language.DirectLimit.dom_partialEquivLimit {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {ι : Type u_1} [Preorder ι] [Nonempty ι] [IsDirected ι fun (x1 x2 : ι) => x1 x2] (S : ι →o L.PartialEquiv M N) :
(partialEquivLimit S).dom = ⨆ (x : ι), (S x).dom
@[simp]
theorem FirstOrder.Language.DirectLimit.cod_partialEquivLimit {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {ι : Type u_1} [Preorder ι] [Nonempty ι] [IsDirected ι fun (x1 x2 : ι) => x1 x2] (S : ι →o L.PartialEquiv M N) :
(partialEquivLimit S).cod = ⨆ (x : ι), (S x).cod
theorem FirstOrder.Language.DirectLimit.le_partialEquivLimit {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {ι : Type u_1} [Preorder ι] [Nonempty ι] [IsDirected ι fun (x1 x2 : ι) => x1 x2] (S : ι →o L.PartialEquiv M N) (i : ι) :
@[reducible, inline]
abbrev FirstOrder.Language.FGEquiv (L : 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

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
Equations
  • One or more equations did not get rendered due to their size.
def FirstOrder.Language.FGEquiv.symm {L : 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
@[simp]
theorem FirstOrder.Language.FGEquiv.symm_coe {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (f : L.FGEquiv M N) :
f.symm = (↑f).symm
theorem FirstOrder.Language.isExtensionPair_iff_cod {L : 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 : 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 (↥((Substructure.closure L).toFun {m}S)) N), f = g.comp (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 : 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.

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

Equations

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

Equations
theorem FirstOrder.Language.embedding_from_cg {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (M_cg : 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 : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (M_cg : Structure.CG L M) (N_cg : 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.