Tensoring local equivalences of module presheaves on a space

On a topological space, sheafification inverts the result of whiskering a stalkwise isomorphism of module presheaves by an arbitrary module presheaf. Unlike the arbitrary-site result for an invertible factor, this needs no flatness or rank-one hypothesis: stalks commute with the tensor product, and tensoring an isomorphism remains an isomorphism.

theorem PresheafOfModules.W_whiskerLeft_of_isIso_stalk {Y : TopCat} {R : TopCat.Presheaf CommRingCat Y} (M : PresheafOfModules (CategoryTheory.Functor.comp R (CategoryTheory.forget₂ CommRingCat RingCat))) {G₁ G₂ : PresheafOfModules (CategoryTheory.Functor.comp R (CategoryTheory.forget₂ CommRingCat RingCat))} (g : G₁ ⟶ G₂) (hg : ∀ (y : ↑Y), CategoryTheory.IsIso (stalkMapAdd g y)) : (Opens.grothendieckTopology ↑Y).W ((toPresheaf (CategoryTheory.Functor.comp R (CategoryTheory.forget₂ CommRingCat RingCat))).map (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M g))

Sheafification inverts M ◁ g on a topological space whenever every stalk map of g is an isomorphism.