English
An FG structure automatically yields CG structure via a standard mapping.
Русский
Структура FG автоматически порождает cg-структуру через стандартное отображение.
LaTeX
$$$$ [FG\\;L\\;M] \\Rightarrow CG\\;L\\;M. $$$$
Lean4
/-- A countably generated structure is ultrahomogeneous if and only if any equivalence between
finitely generated substructures can be extended to any element in the domain. -/
theorem isUltrahomogeneous_iff_IsExtensionPair (M_CG : CG L M) : L.IsUltrahomogeneous M ↔ L.IsExtensionPair M M :=
by
constructor
· intro M_homog ⟨f, f_FG⟩ m
let S := f.dom ⊔ closure L { m }
have dom_le_S : f.dom ≤ S := le_sup_left
let ⟨f', eq_f'⟩ :=
M_homog.extend_embedding (f.dom.fg_iff_structure_fg.1 f_FG) ((subtype _).comp f.toEquiv.toEmbedding)
(inclusion dom_le_S) (h := ⟨subtype _⟩)
refine
⟨⟨⟨S, f'.toHom.range, f'.equivRange⟩, f_FG.sup (fg_closure_singleton _)⟩,
subset_closure.trans (le_sup_right : _ ≤ S) (mem_singleton m), ⟨dom_le_S, ?_⟩⟩
ext
simp only [Embedding.comp_apply, Equiv.coe_toEmbedding, coe_subtype, eq_f', Embedding.equivRange_apply,
Substructure.coe_inclusion]
· intro h S S_FG f
let ⟨g, ⟨dom_le_dom, eq⟩⟩ := equiv_between_cg M_CG M_CG ⟨⟨S, f.toHom.range, f.equivRange⟩, S_FG⟩ h h
use g
simp only [Embedding.subtype_equivRange] at eq
rw [← eq]
ext
rfl
