English
If M is a countably generated structure in language L and for every PartialEquiv between finitely generated substructures there is an extension to any element in the domain, then there exists an embedding of M into N.
Русский
Если структура M порождается счётно и для любого частичного эквивалента между конечнопорождёнными подструктурами существует продолжение к любому элементу области определения, то существует вложение M в N.
LaTeX
$$$\\exists f : M \\hookrightarrow_L N,\\ g \\le f.toPartialEquiv$$$
Lean4
/-- 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 embedding_from_cg (M_cg : Structure.CG L M) (g : L.FGEquiv M N) (H : L.IsExtensionPair M N) :
∃ f : M ↪[L] N, g ≤ f.toPartialEquiv := by
rcases M_cg with ⟨X, _, X_gen⟩
have _ : Countable (↑X : Type _) := by simpa only [countable_coe_iff]
have _ : Encodable (↑X : Type _) := Encodable.ofCountable _
let D : X → Order.Cofinal (FGEquiv L M N) := fun x ↦ H.definedAtLeft x
let S : ℕ →o M ≃ₚ[L] N :=
⟨Subtype.val ∘ (Order.sequenceOfCofinals g D), (Subtype.mono_coe _).comp (Order.sequenceOfCofinals.monotone _ _)⟩
let F := DirectLimit.partialEquivLimit S
have _ : X ⊆ F.dom := by
intro x hx
have := Order.sequenceOfCofinals.encode_mem g D ⟨x, hx⟩
exact dom_le_dom (le_partialEquivLimit S (Encodable.encode (⟨x, hx⟩ : X) + 1)) this
have isTop : F.dom = ⊤ := by rwa [← top_le_iff, ← X_gen, Substructure.closure_le]
exact ⟨toEmbeddingOfEqTop isTop, by convert (le_partialEquivLimit S 0); apply Embedding.toPartialEquiv_toEmbedding⟩
