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.val)
[CategoryTheory.Presheaf.IsLocallyInjective J α]
[CategoryTheory.Presheaf.IsLocallySurjective J α]
[J.WEqualsLocallyBijective AddCommGrpCat]
[CategoryTheory.HasWeakSheafify J AddCommGrpCat]
:
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.val)
[CategoryTheory.Presheaf.IsLocallyInjective J α]
[CategoryTheory.Presheaf.IsLocallySurjective J α]
[J.WEqualsLocallyBijective AddCommGrpCat]
[CategoryTheory.HasWeakSheafify J AddCommGrpCat]
:
(sheafification α).IsLocalization (J.W.inverseImage (toPresheaf R₀))