The category of sheaves of modules as a localization of presheaves of modules

Similarly as the category of sheaves with values in a category identify to a localization of the category of presheaves with respect to those morphisms which become isomorphisms after sheafification (see the file Mathlib/CategoryTheory/Sites/Localization.lean), we show that the sheafification functor from presheaves of modules to sheaves of modules is a localization functor.

theorem PresheafOfModules.inverseImage_W_toPresheaf_eq_inverseImage_isomorphisms {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R₀ : CategoryTheory.Functor Cᵒᵖ RingCat} {R : CategoryTheory.Sheaf J RingCat} (α : R₀ ⟶ R.obj) [CategoryTheory.Presheaf.IsLocallyInjective J α] [CategoryTheory.Presheaf.IsLocallySurjective J α] [J.WEqualsLocallyBijective AddCommGrpCat] [CategoryTheory.HasWeakSheafify J AddCommGrpCat] : J.W.inverseImage (toPresheaf R₀) = (CategoryTheory.MorphismProperty.isomorphisms (SheafOfModules R)).inverseImage (sheafification α)

instance PresheafOfModules.instIsLocalizationSheafOfModulesSheafificationInverseImageFunctorOppositeAbWToPresheaf {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R₀ : CategoryTheory.Functor Cᵒᵖ RingCat} {R : CategoryTheory.Sheaf J RingCat} (α : R₀ ⟶ R.obj) [CategoryTheory.Presheaf.IsLocallyInjective J α] [CategoryTheory.Presheaf.IsLocallySurjective J α] [J.WEqualsLocallyBijective AddCommGrpCat] [CategoryTheory.HasWeakSheafify J AddCommGrpCat] : (sheafification α).IsLocalization (J.W.inverseImage (toPresheaf R₀))