English
If for every g in t the kernel of Localization.awayMap f g is finitely generated, then the kernel of f is finitely generated.
Русский
Если для каждого g из t ядро Localization.awayMap f g конечно порождено, то ядро f конечно порождено.
LaTeX
$$$\\forall g, (RingHom.ker (Localization.awayMap f g.val)).FG \\Rightarrow (RingHom.ker f).FG$$$
Lean4
/-- If `I` is an ideal such that there exists a set `{ r }` of `R` such
that the image of `I` in `Rᵣ` is finitely generated for each `r`, then `I` is finitely
generated. -/
theorem fg_of_localizationSpan {I : Ideal R} (t : Set R) (ht : Ideal.span t = ⊤)
(H : ∀ (g : t), (I.map (algebraMap R (Localization.Away g.val))).FG) : I.FG :=
by
apply Module.Finite.iff_fg.mp
let k (g : t) : I →ₗ[R] (I.map (algebraMap R (Localization.Away g.val))) :=
Algebra.idealMap I (S := Localization.Away g.val)
exact Module.Finite.of_localizationSpan' t ht k (fun g ↦ Module.Finite.iff_fg.mpr (H g))
