Partial Isomorphisms

This file defines partial isomorphisms between first-order structures.

Main Definitions

• FirstOrder.Language.PartialEquiv is defined so that L.PartialEquiv M N, annotated M ≃ₚ[L] N, is the type of equivalences between substructures of M and N. These can be ordered, with an order that is defined here in terms of a commutative square, but could also be defined as the order on the graphs of the partial equivalences under inclusion as subsets of M × N.
• FirstOrder.Language.FGEquiv is the type of partial equivalences M ≃ₚ[L] N with finitely-generated domain (or equivalently, codomain).
• FirstOrder.Language.IsExtensionPair is defined so that L.IsExtensionPair M N indicates that any finitely-generated partial equivalence from M to N can be extended to include an arbitrary element m : M in its domain.

Main Results

• FirstOrder.Language.embedding_from_cg shows that if structures M and N form an equivalence pair with M countably-generated, then any finite-generated partial equivalence between them can be extended to an embedding M ↪[L] N.
• FirstOrder.Language.equiv_from_cg shows that if countably-generated structures M and N form an equivalence pair in both directions, then any finite-generated partial equivalence between them can be extended to an isomorphism M ↪[L] N.
• The proofs of these results are adapted in part from David Wärn's approach to countable dense linear orders, a special case of this phenomenon in the case where L = Language.order.

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.

def FirstOrder.«term_≃ₚ[_]_» : Lean.TrailingParserDescr

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

@[implicit_reducible]

noncomputable instance FirstOrder.Language.PartialEquiv.instInhabited_self {L : Language} {M : Type w} [L.Structure M] : Inhabited (L.PartialEquiv M M)

def FirstOrder.Language.PartialEquiv.symm {L : 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.

@[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

theorem FirstOrder.Language.PartialEquiv.symm_bijective {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] : Function.Bijective symm

@[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) : f.symm.toEquiv x = f.toEquiv.symm x

@[implicit_reducible]

instance FirstOrder.Language.PartialEquiv.instLE {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] : LE (L.PartialEquiv M N)

theorem FirstOrder.Language.PartialEquiv.le_def {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (f g : L.PartialEquiv M N) : f ≤ g ↔ ∃ (h : f.dom ≤ g.dom), g.cod.subtype.comp (g.toEquiv.toEmbedding.comp (Substructure.inclusion h)) = f.cod.subtype.comp f.toEquiv.toEmbedding

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 ≤ g → f.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 ≤ g → f.cod ≤ g.cod

theorem FirstOrder.Language.PartialEquiv.subtype_toEquiv_inclusion {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {f g : L.PartialEquiv M N} (h : f ≤ g) : g.cod.subtype.comp (g.toEquiv.toEmbedding.comp (Substructure.inclusion ⋯)) = f.cod.subtype.comp f.toEquiv.toEmbedding

theorem FirstOrder.Language.PartialEquiv.toEquiv_inclusion {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {f g : L.PartialEquiv M N} (h : f ≤ g) : g.toEquiv.toEmbedding.comp (Substructure.inclusion ⋯) = (Substructure.inclusion ⋯).comp f.toEquiv.toEmbedding

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) : g.toEquiv ((Substructure.inclusion ⋯) x) = (Substructure.inclusion ⋯) (f.toEquiv x)

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 ≤ g → g ≤ h → f ≤ h

@[implicit_reducible]

instance FirstOrder.Language.PartialEquiv.instPartialOrder {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] : PartialOrder (L.PartialEquiv M N)

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) : f.symm ≤ g.symm

theorem FirstOrder.Language.PartialEquiv.monotone_symm {L : 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 : 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) : L.PartialEquiv M N

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

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) : f.domRestrict h ≤ f

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) : f ≤ g.domRestrict hg

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) : L.PartialEquiv M N

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

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) : f.codRestrict h ≤ f

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) : f ≤ g.codRestrict hg

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.

@[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.

@[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, ⋯⟩)

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.

@[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 = ⊤) : (toEquivOfEqTop h_dom h_cod).toEmbedding = toEmbeddingOfEqTop h_dom

theorem FirstOrder.Language.PartialEquiv.dom_fg_iff_cod_fg {L : Language} {M : Type w} [L.Structure M] {N : Type u_1} [L.Structure N] (f : L.PartialEquiv M N) : f.dom.FG ↔ f.cod.FG

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) : L.PartialEquiv M N

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

theorem FirstOrder.Language.Embedding.toPartialEquiv_injective {L : 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 : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (f : L.Embedding M N) : PartialEquiv.toEmbeddingOfEqTop ⋯ = f

@[simp]

theorem FirstOrder.Language.Embedding.toPartialEquiv_toEmbedding {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {f : L.PartialEquiv M N} (h : f.dom = ⊤) : (PartialEquiv.toEmbeddingOfEqTop h).toPartialEquiv = f

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 ι] [IsDirectedOrder ι] (S : ι →o L.PartialEquiv M N) : L.PartialEquiv M N

The limit of a directed system of PartialEquivs.

@[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 ι] [IsDirectedOrder ι] (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 ι] [IsDirectedOrder ι] (S : ι →o L.PartialEquiv M N) : (partialEquivLimit S).cod = ⨆ (x : ι), (S x).cod

@[simp]

theorem FirstOrder.Language.DirectLimit.partialEquivLimit_comp_inclusion {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {ι : Type u_1} [Preorder ι] [Nonempty ι] [IsDirectedOrder ι] (S : ι →o L.PartialEquiv M N) {i : ι} : (partialEquivLimit S).toEquiv.toEmbedding.comp (Substructure.inclusion ⋯) = (Substructure.inclusion ⋯).comp (S i).toEquiv.toEmbedding

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 ι] [IsDirectedOrder ι] (S : ι →o L.PartialEquiv M N) (i : ι) : S i ≤ partialEquivLimit S

@[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.

def FirstOrder.Language.IsExtensionPair (L : Language) (M : Type w) (N : Type w') [L.Structure M] [L.Structure N] : Prop

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.

theorem FirstOrder.Language.countable_self_fgequiv_of_countable {L : Language} {M : Type w} [L.Structure M] [Countable M] : Countable (L.FGEquiv M M)

@[implicit_reducible]

instance FirstOrder.Language.inhabited_self_FGEquiv {L : Language} {M : Type w} [L.Structure M] : Inhabited (L.FGEquiv M M)

@[implicit_reducible]

instance FirstOrder.Language.inhabited_FGEquiv_of_IsEmpty_Constants_and_Relations {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] [IsEmpty L.Constants] [IsEmpty (L.Relations 0)] : Inhabited (L.FGEquiv M N)

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.

@[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.

def FirstOrder.Language.IsExtensionPair.definedAtLeft {L : 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.

def FirstOrder.Language.IsExtensionPair.definedAtRight {L : 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.

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.