Patching submodules across two principal localizations

For a finite module over a Noetherian ring, submodules of its localizations away from r and s that agree in the common localization away from r * s come from one finitely generated submodule. The witness is the intersection of their inverse images in the original module.

The overlap hypothesis compares the localizations at r * s of those two inverse images. This is a purely algebraic two-chart statement. It constructs no sheaf or coherent subobject on a union of basic opens, and proves no quasi-compact-open descent theorem.

theorem Submodule.exists_fg_two_away_localized_submodule_of_overlap {R : Type u} [CommRing R] [IsNoetherianRing R] {M : Type w} [AddCommGroup M] [Module R M] [Module.Finite R M] (r s : R) (Pr : Submodule (Localization.Away r) (LocalizedModule.Away r M)) (Ps : Submodule (Localization.Away s) (LocalizedModule.Away s M)) (hOverlap : have fr := LocalizedModule.mkLinearMap (Submonoid.powers r) M; have fs := LocalizedModule.mkLinearMap (Submonoid.powers s) M; let frs := LocalizedModule.mkLinearMap (Submonoid.powers (r * s)) M; localized' (Localization.Away (r * s)) (Submonoid.powers (r * s)) frs (comap fr (restrictScalars R Pr)) = localized' (Localization.Away (r * s)) (Submonoid.powers (r * s)) frs (comap fs (restrictScalars R Ps))) : ∃ (N : Submodule R M), N.FG ∧ localized' (Localization.Away r) (Submonoid.powers r) (LocalizedModule.mkLinearMap (Submonoid.powers r) M) N = Pr ∧ localized' (Localization.Away s) (Submonoid.powers s) (LocalizedModule.mkLinearMap (Submonoid.powers s) M) N = Ps

Two compatible submodules on the principal localizations of a finite module have a single finitely generated lift. Compatibility is equality in the canonical common localization away from r * s, after pulling both submodules back to M. The witness is the intersection of these two inverse images. No geometric sheaf-gluing statement is asserted.