English
The amalgamation property for age ensures existence of a common extension preserving embeddings for given M,N,P.
Русский
Свойство амальгамирования возраста обеспечивает существование общего расширения, сохраняющего вложения для M,N,P.
LaTeX
$$amalgamation_age (h) : Amalgamation (L.age M)$$
Lean4
theorem amalgamation_age (h : L.IsUltrahomogeneous M) : Amalgamation (L.age M) :=
by
rintro N P Q NP NQ ⟨Nfg, ⟨-⟩⟩ ⟨Pfg, ⟨PM⟩⟩ ⟨Qfg, ⟨QM⟩⟩
obtain ⟨g, hg⟩ :=
h (PM.comp NP).toHom.range (Nfg.range _) ((QM.comp NQ).comp (PM.comp NP).equivRange.symm.toEmbedding)
let s := (g.toHom.comp PM.toHom).range ⊔ QM.toHom.range
refine
⟨Bundled.of s, Embedding.comp (Substructure.inclusion le_sup_left) (g.toEmbedding.comp PM).equivRange.toEmbedding,
Embedding.comp (Substructure.inclusion le_sup_right) QM.equivRange.toEmbedding,
⟨(fg_iff_structure_fg _).1 (FG.sup (Pfg.range _) (Qfg.range _)), ⟨Substructure.subtype _⟩⟩, ?_⟩
ext n
apply Subtype.ext
have hgn := (Embedding.ext_iff.1 hg) ((PM.comp NP).equivRange n)
simp only [Embedding.comp_apply, Equiv.coe_toEmbedding, Equiv.symm_apply_apply, Substructure.coe_subtype,
Embedding.equivRange_apply] at hgn
simp only [Embedding.comp_apply, Equiv.coe_toEmbedding]
erw [Substructure.coe_inclusion, Substructure.coe_inclusion]
simp only [Embedding.equivRange_apply, hgn]
-- This used to be `simp only [...]` before https://github.com/leanprover/lean4/pull/2644
erw [Embedding.comp_apply, Equiv.coe_toEmbedding, Embedding.equivRange_apply]
simp
