English
Same as above: if all localized kernels are finitely generated, then the kernel of the original ring homomorphism is finitely generated.
Русский
То же самое: если все локализованные ядра конечны, то ядро исходного кольцевого гомоморфа конечного порождено.
LaTeX
$$$\\forall g, (Localization.awayMap f g.val).\\ker FG \\Rightarrow (\\ker f) FG$$$
Lean4
/-- To check that the kernel of a ring homomorphism is finitely generated,
it suffices to check this after localizing at a spanning set of the source.
-/
theorem ker_fg_of_localizationSpan (t : Set R) (ht : Ideal.span t = ⊤)
(H : ∀ g : t, (RingHom.ker (Localization.awayMap f g.val)).FG) : (RingHom.ker f).FG :=
by
apply Ideal.fg_of_localizationSpan t ht
intro g
rw [← IsLocalization.ker_map (Localization.Away (f g.val)) f (Submonoid.map_powers f g.val)]
exact H g
