The range of a tilde map on an affine basic open

On D(r), the range of the map of tilde sheaves induced by a module map is the localization of its range. The statement uses the canonical Localization.Away r-action transported to the underlying R-module of sections by IsLocalizedModule.module. It does not identify that action definitionally with the structure-sheaf action, nor compare categorical coherent subobjects or glue them across opens.

theorem AlgebraicGeometry.tilde.localized'_range_eq_range_map_basicOpen (R : CommRingCat) (K M : ModuleCat ↑R) (g : K ⟶ M) (r : ↑R) : let S := Submonoid.powers r; let U := PrimeSpectrum.basicOpen r; let fK := ModuleCat.Hom.hom (toOpen K U); let fM := ModuleCat.Hom.hom (toOpen M U); have h := ModuleCat.Hom.hom ((modulesSpecToSheaf.map (tilde.map g)).hom.app (Opposite.op U)); Submodule.localized' (Localization.Away r) S fM (ModuleCat.Hom.hom g).range = (LinearMap.extendScalarsOfIsLocalization S (Localization.Away r) h).range

The range of tilde.map g on D(r) is the localization away from r of g's range. The result applies to an inclusion N.subtype as well as an arbitrary module map. Both localized-module structures and scalar towers are proof-local; no global instance for the section modules is introduced.