English
If I is an ideal such that the image of I in each Localization.Away g is finitely generated, then I is finitely generated.
Русский
Если I — идеал и образ I в каждой Localization.Away g конечно порожден, то I конечно порожден.
LaTeX
$$$\\forall t,\\ (I.map (algebraMap R (Localization.Away g.val))).FG\\text{ for all } g,\\Rightarrow I.FG$$$
Lean4
/-- If there exists a set `{ r }` of `R` such that `Mᵣ` is `Rᵣ`-finite for each `r`,
then `M` is a finite `R`-module. -/
theorem of_localizationSpan (t : Set R) (ht : Ideal.span t = ⊤)
(H : ∀ (g : t), Module.Finite (Localization.Away g.val) (LocalizedModule (Submonoid.powers g.val) M)) :
Module.Finite R M :=
let f (g : t) : M →ₗ[R] LocalizedModule (Submonoid.powers g.val) M :=
LocalizedModule.mkLinearMap (Submonoid.powers g.val) M
of_localizationSpan' t ht f H
