Finite generation before localizing a submodule

Every finitely generated submodule of a localized module is the localization of some finitely generated submodule of the original module. The original module need not be finite, and no Noetherian hypothesis is used.

This is an algebraic statement for any multiplicative set. It does not assert that the associated morphism of spectra is an open immersion, or extend a finite-type quasi-coherent subsheaf across a quasi-compact open.

theorem Submodule.exists_fg_localized_submodule {R : Type u} [CommSemiring R] {R' : Type v} [CommSemiring R'] [Algebra R R'] {M : Type w} [AddCommMonoid M] [Module R M] {M' : Type x} [AddCommMonoid M'] [Module R M'] [Module R' M'] [IsScalarTower R R' M'] (S : Submonoid R) [IsLocalization S R'] (f : M →ₗ[R] M') [IsLocalizedModule S f] (P : Submodule R' M') (hP : P.FG) : ∃ (N : Submodule R M), N.FG ∧ localized' R' S f N = P

A finitely generated submodule of a localized module has a finitely generated submodule upstairs whose localization is exactly the given one.