English
Let M and N be Fraïssé limits of a common class K of L-structures. For every finitely generated substructure A of M and every element m in M, there exists an embedding of the substructure S generated by A together with m into N that extends the given embedding of A.
Русский
Пусть M и N являются пределами Фраиссe класса K структур над языком L. Для любой FG-подструктуры A ⊆ M и любого элемента m ∈ M существует вложение подструктуры S, порождённой A и m, в N, которое расширяет заданное вложение A.
LaTeX
$$$IsFraisseLimit(K,M) \land IsFraisseLimit(K,N) \rightarrow L.IsExtensionPair M N$$$
Lean4
protected theorem isExtensionPair : L.IsExtensionPair M N :=
by
intro ⟨f, f_FG⟩ m
let S := f.dom ⊔ closure L { m }
have S_FG : S.FG := f_FG.sup (Substructure.fg_closure_singleton _)
have S_in_age_N : ⟨S, inferInstance⟩ ∈ L.age N :=
by
rw [hN.age, ← hM.age]
exact ⟨(fg_iff_structure_fg S).1 S_FG, ⟨subtype _⟩⟩
haveI nonempty_S_N : Nonempty (S ↪[L] N) := S_in_age_N.2
let ⟨g, g_eq⟩ :=
hN.ultrahomogeneous.extend_embedding (f.dom.fg_iff_structure_fg.1 f_FG) ((subtype f.cod).comp f.toEquiv.toEmbedding)
(inclusion (le_sup_left : _ ≤ S))
refine
⟨⟨⟨S, g.toHom.range, g.equivRange⟩, S_FG⟩, subset_closure.trans (le_sup_right : _ ≤ S) (mem_singleton m),
⟨le_sup_left, ?_⟩⟩
ext
simp [S, g_eq]
