English
A submodule N of a finitely generated module M over a semilocal ring R is finitely generated if its localization at every maximal ideal is finitely generated.
Русский
Подмодуль N модуля M над полусоединенным кольцом R конечно порожден, если локализации по всем максимальным идеалам конечно порождены.
LaTeX
$$$N \\text{ FG} \\iff \\forall P [P.IsMaximal], (N.localized' (R_p) P.primeCompl N).FG$$$
Lean4
/-- A submodule `N` of a module `M` over a semilocal ring `R` is finitely generated if
its localization at every maximal ideal is finitely generated. -/
theorem fg_of_isLocalized_maximal (N : Submodule R M)
(H : ∀ (P : Ideal R) [P.IsMaximal], (Submodule.localized' (Rₚ P) P.primeCompl (f P) N).FG) : N.FG :=
by
simp_rw [← Module.Finite.iff_fg] at ⊢ H
exact .of_isLocalized_maximal _ _ _ (fun P ↦ N.toLocalized' (Rₚ P) P.primeCompl (f P)) H
