Potential isomorphisms

Two structures are potentially isomorphic when some nonempty family of equivalences between finitely generated substructures has the back-and-forth extension property. Crucially, extensions must remain inside the chosen family. Mathlib's Language.IsExtensionPair instead requires every finitely generated partial equivalence to extend; holding in both directions, together with an initial finitely generated partial equivalence, it implies potential isomorphism (FirstOrder.Language.IsExtensionPair.potentialIso).

In any language, potential isomorphism is reflexive, since an isomorphism gives one (FirstOrder.Language.Equiv.potentialIso), symmetric (TauCeti.PotentialIso.symm), and transitive (TauCeti.PotentialIso.trans), by composing members of the two families.

The definition is the finitely-generated-partial-equivalence presentation of the back-and-forth systems used by Carol Karp, Finite-quantifier equivalence (1965). Cameron Freer's cameronfreer/infinitary-logic, InfinitaryLogic/Karp/PotentialIso.lean at checkpoint 9f82bd572af2d79a043c6bc3f1b745f14e0bcaa4, instead uses finite tuples; the two presentations agree for relational languages.

def TauCeti.PotentialIso {L : FirstOrder.Language} (M : Type w) (N : Type w') [L.Structure M] [L.Structure N] : Prop

Two structures are potentially isomorphic if a nonempty set of finitely generated partial equivalences admits extensions containing every element on either side.

theorem TauCeti.potentialIso_def {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] : PotentialIso M N ↔ ∃ (S : Set (L.FGEquiv M N)), S.Nonempty ∧ (∀ f ∈ S, ∀ (m : M), ∃ g ∈ S, m ∈ (↑g).dom ∧ f ≤ g) ∧ ∀ f ∈ S, ∀ (n : N), ∃ g ∈ S, n ∈ (↑g).cod ∧ f ≤ g

Potential isomorphism is witnessed by a nonempty family closed under extensions on both sides.

theorem FirstOrder.Language.Equiv.potentialIso {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (e : L.Equiv M N) : TauCeti.PotentialIso M N

An isomorphism gives a potential isomorphism by restricting it to finitely generated substructures.

@[simp]

theorem FirstOrder.Language.FGEquiv.symm_symm {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (f : L.FGEquiv M N) : f.symm.symm = f

Inverting a finitely generated partial equivalence twice gives it back.

theorem TauCeti.PotentialIso.symm {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (h : PotentialIso M N) : PotentialIso N M

Potential isomorphism is symmetric.

theorem TauCeti.PotentialIso.trans {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {P : Type u_1} [L.Structure P] (h₁ : PotentialIso M N) (h₂ : PotentialIso N P) : PotentialIso M P

Potential isomorphism is transitive.

theorem FirstOrder.Language.IsExtensionPair.potentialIso {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (hMN : L.IsExtensionPair M N) (hNM : L.IsExtensionPair N M) (hne : Nonempty (L.FGEquiv M N)) : TauCeti.PotentialIso M N

Mathlib's global two-sided extension property gives a potential isomorphism when there is an initial finitely generated partial equivalence.