English
For two countably generated structures M and N, if any PartialEquiv between finitely generated substructures can be extended to any element in both the domain and codomain, then there exists an L-equivalence M ≃_L N extending g.
Русский
Для двух счётно порожденных структур M и N, если любой частичный эквив между конечно порожденными подпредств может быть продолжен как к домену, так и к областью значений, существует эквивалентность на языке L между M и N, которая расширяет заданное g.
LaTeX
$$$\\exists f : M \\simeq_L N, \\ g \\le f.toEmbedding.toPartialEquiv$$$
Lean4
/-- 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`. -/
theorem equiv_between_cg (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 : M ≃[L] N, g ≤ f.toEmbedding.toPartialEquiv :=
by
rcases M_cg with ⟨X, X_count, X_gen⟩
rcases N_cg with ⟨Y, Y_count, Y_gen⟩
have _ : Countable (↑X : Type _) := by simpa only [countable_coe_iff]
have _ : Encodable (↑X : Type _) := Encodable.ofCountable _
have _ : Countable (↑Y : Type _) := by simpa only [countable_coe_iff]
have _ : Encodable (↑Y : Type _) := Encodable.ofCountable _
let D : Sum X Y → Order.Cofinal (FGEquiv L M N) := fun p ↦
Sum.recOn p (fun x ↦ ext_dom.definedAtLeft x) (fun y ↦ ext_cod.definedAtRight y)
let S : ℕ →o M ≃ₚ[L] N :=
⟨Subtype.val ∘ (Order.sequenceOfCofinals g D), (Subtype.mono_coe _).comp (Order.sequenceOfCofinals.monotone _ _)⟩
let F := @DirectLimit.partialEquivLimit L M N _ _ ℕ _ _ _ S
have _ : X ⊆ F.dom := by
intro x hx
have := Order.sequenceOfCofinals.encode_mem g D (Sum.inl ⟨x, hx⟩)
exact dom_le_dom (le_partialEquivLimit S (Encodable.encode (Sum.inl (⟨x, hx⟩ : X)) + 1)) this
have _ : Y ⊆ F.cod := by
intro y hy
have := Order.sequenceOfCofinals.encode_mem g D (Sum.inr ⟨y, hy⟩)
exact cod_le_cod (le_partialEquivLimit S (Encodable.encode (Sum.inr (⟨y, hy⟩ : Y)) + 1)) this
have dom_top : F.dom = ⊤ := by rwa [← top_le_iff, ← X_gen, Substructure.closure_le]
have cod_top : F.cod = ⊤ := by rwa [← top_le_iff, ← Y_gen, Substructure.closure_le]
refine ⟨toEquivOfEqTop dom_top cod_top, ?_⟩
convert le_partialEquivLimit S 0
rw [toEquivOfEqTop_toEmbedding]
apply Embedding.toPartialEquiv_toEmbedding
