English
Given an ultrahomogeneous structure M, any finitely generated S embedding into M can be extended to embed into any T that also embeds into M.
Русский
Пусть M ультрахомогенна; любая FG-подструктура S, встраиваемая в M, может быть дополнительно встроена в любую T, который тоже встраивается в M.
LaTeX
$$extend_embedding (M_homog) {S FG} {T} ...$$
Lean4
/-- Any embedding from a finitely generated `S` to an ultrahomogeneous structure `M`
can be extended to an embedding from any structure with an embedding to `M`. -/
theorem extend_embedding (M_homog : L.IsUltrahomogeneous M) {S : Type*} [L.Structure S] (S_FG : FG L S) {T : Type*}
[L.Structure T] [h : Nonempty (T ↪[L] M)] (f : S ↪[L] M) (g : S ↪[L] T) : ∃ f' : T ↪[L] M, f = f'.comp g :=
by
let ⟨r⟩ := h
let s := r.comp g
let ⟨t, eq⟩ := M_homog s.toHom.range (S_FG.range s.toHom) (f.comp s.equivRange.symm.toEmbedding)
use t.toEmbedding.comp r
change _ = t.toEmbedding.comp s
ext x
have eq' := congr_fun (congr_arg DFunLike.coe eq) ⟨s x, Hom.mem_range.2 ⟨x, rfl⟩⟩
simp only [Embedding.comp_apply, coe_subtype] at eq'
simp only [Embedding.comp_apply, ← eq', Equiv.coe_toEmbedding, EmbeddingLike.apply_eq_iff_eq]
apply (Embedding.equivRange (Embedding.comp r g)).injective
ext
simp only [Equiv.apply_symm_apply, Embedding.equivRange_apply, s]
