English
An alternate characterization of an extension pair is that every finitely generated partial isomorphism can be extended to include any particular element of the domain.
Русский
Альтернативная характеристика пары расширения: каждая конечно порожденная частичная изоморфия может быть расширена так, чтобы включать любой выбранный элемент области определения.
LaTeX
$$$L.IsExtensionPair M N \iff \forall S:(L.Substructure M)\, (S.FG)\, (f:S \hookrightarrow N)\, (m:M),\ \exists g:(closure L\ {m} \sqcup S)\hookrightarrow N,\ f = g.\mathrm{comp}(Substructure.inclusion).$$$
Lean4
/-- An alternate characterization of an extension pair is that every finitely generated partial
isomorphism can be extended to include any particular element of the domain. -/
theorem isExtensionPair_iff_exists_embedding_closure_singleton_sup :
L.IsExtensionPair M N ↔
∀ (S : L.Substructure M) (_ : S.FG) (f : S ↪[L] N) (m : M),
∃ g : (closure L { m } ⊔ S : L.Substructure M) ↪[L] N, f = g.comp (Substructure.inclusion le_sup_right) :=
by
refine ⟨fun h S S_FG f m => ?_, fun h ⟨f, f_FG⟩ m => ?_⟩
· obtain ⟨⟨f', hf'⟩, mf', ff'1, ff'2⟩ := h ⟨⟨S, _, f.equivRange⟩, S_FG⟩ m
refine ⟨f'.toEmbedding.comp (Substructure.inclusion ?_), ?_⟩
· simp only [sup_le_iff, ff'1, closure_le, singleton_subset_iff, SetLike.mem_coe, mf', and_self]
· ext ⟨x, hx⟩
rw [Embedding.subtype_equivRange] at ff'2
simp only [← ff'2, Embedding.comp_apply, Substructure.coe_inclusion, inclusion_mk, Equiv.coe_toEmbedding,
coe_subtype, PartialEquiv.toEmbedding_apply]
· obtain ⟨f', eq_f'⟩ := h f.dom f_FG f.toEmbedding m
refine
⟨⟨⟨closure L { m } ⊔ f.dom, f'.toHom.range, f'.equivRange⟩, (fg_closure_singleton _).sup f_FG⟩,
subset_closure.trans (le_sup_left : (closure L) { m } ≤ _) (mem_singleton m),
⟨le_sup_right, Embedding.ext (fun _ => ?_)⟩⟩
rw [PartialEquiv.toEmbedding] at eq_f'
simp only [Embedding.comp_apply, Substructure.coe_inclusion, Equiv.coe_toEmbedding, coe_subtype,
Embedding.equivRange_apply, eq_f']
