Back-and-forth equivalence from extension pairs

Mathlib's Language.IsExtensionPair M N says that every finitely generated partial equivalence from M to N extends to any given element of M. In a relational language a pair of tuples with the same atomic type is the same thing as a finite partial equivalence, so when M, N form an extension pair in both directions, the pairs of tuples with the same atomic type form a tuple back-and-forth system. Consequently atomic-type agreement already gives back-and-forth equivalence at every ordinal level: the back-and-forth hierarchy between such structures collapses at level zero.

This applies to dense linear orders without endpoints (Mathlib's dlo_isExtensionPair), and to countably generated ultrahomogeneous structures (Mathlib's isUltrahomogeneous_iff_IsExtensionPair). No countability or nonemptiness is assumed; the agreement on nullary relations needed by the empty tuples is carried by the given pair of tuples.

Main results

• TauCeti.SameAtomicType.exists_snoc_of_isExtensionPair: matching one-point extensions.
• TauCeti.isExtensionPair_iff_forall_exists_snoc: conversely, matching one-point extensions of tuples give an extension pair.
• TauCeti.isTupleBFSystem_sameAtomicType: the atomic-type pairs form a tuple back-and-forth system.
• TauCeti.SameAtomicType.bfEquiv_of_isExtensionPair: atomic-type agreement implies back-and-forth equivalence at every level.

theorem TauCeti.SameAtomicType.exists_snoc_of_isExtensionPair {L : FirstOrder.Language} [L.IsRelational] {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {n : ℕ} {a : Fin n → M} {b : Fin n → N} (h : SameAtomicType a b) (hMN : L.IsExtensionPair M N) (x : M) : ∃ (y : N), SameAtomicType (Fin.snoc a x) (Fin.snoc b y)

If every finitely generated partial equivalence from M to N extends to each element of M, then tuples with the same atomic type have matching one-point extensions on the M side.

theorem TauCeti.isExtensionPair_iff_forall_exists_snoc {L : FirstOrder.Language} [L.IsRelational] {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] : L.IsExtensionPair M N ↔ ∀ {n : ℕ} {a : Fin n → M} {b : Fin n → N}, SameAtomicType a b → ∀ (x : M), ∃ (y : N), SameAtomicType (Fin.snoc a x) (Fin.snoc b y)

In a relational language, M, N form an extension pair exactly when tuples with the same atomic type always have matching one-point extensions on the M side. This is how the extension property is checked for concrete structures, one new element at a time.

theorem TauCeti.isTupleBFSystem_sameAtomicType {L : FirstOrder.Language} [L.IsRelational] {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (hMN : L.IsExtensionPair M N) (hNM : L.IsExtensionPair N M) (h₀ : SameAtomicType Fin.elim0 Fin.elim0) : IsTupleBFSystem {p : (n : ℕ) × (Fin n → M) × (Fin n → N) | SameAtomicType p.snd.1 p.snd.2}

When M and N form an extension pair in both directions and their empty tuples agree (that is, on the nullary relations), the pairs of tuples with the same atomic type form a tuple back-and-forth system.

theorem TauCeti.SameAtomicType.bfEquiv_of_isExtensionPair {L : FirstOrder.Language} [L.IsRelational] {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {n : ℕ} {a : Fin n → M} {b : Fin n → N} (h : SameAtomicType a b) (hMN : L.IsExtensionPair M N) (hNM : L.IsExtensionPair N M) (α : Ordinal.{o}) : BFEquiv α n a b

When M and N form an extension pair in both directions, atomic-type agreement implies back-and-forth equivalence at every ordinal level.