The category of sheaves of modules is Grothendieck abelian

instance SheafOfModules.instIsGrothendieckAbelian {C : Type u} [CategoryTheory.SmallCategory C] {J : CategoryTheory.GrothendieckTopology C} (R : CategoryTheory.Sheaf J RingCat) : CategoryTheory.IsGrothendieckAbelian.{u, u, u + 1} (SheafOfModules R)