English
Every finitely generated substructure of a direct limit corresponds to a substructure at some stage of the directed system.
Русский
Каждая конечнопорожденная подструктура прямого предела описывается как образ подструктуры на некотором звене системы.
LaTeX
$$$\exists i,\exists T:\ L\text{Substructure}(G_i),\ T.map(\mathrm{of}\,L\iota G f i).toHom = S.$$$
Lean4
/-- Every finitely generated substructure of the direct limit corresponds to some
substructure in some component of the directed system. -/
theorem exists_fg_substructure_in_Sigma (S : L.Substructure (DirectLimit G f)) (S_fg : S.FG) :
∃ i, ∃ T : L.Substructure (G i), T.map (of L ι G f i).toHom = S :=
by
let ⟨A, A_closure⟩ := S_fg
let ⟨i, y, eq_y⟩ := exists_quotient_mk'_sigma_mk'_eq G _ (fun a : A ↦ a.1)
use i
use Substructure.closure L (range y)
rw [Substructure.map_closure]
simp only [Embedding.coe_toHom, of_apply]
rw [← image_univ, image_image, image_univ, ← eq_y, Subtype.range_coe_subtype, Finset.setOf_mem, A_closure]
