The category of presheaves of modules is abelian

instance PresheafOfModules.instIsNormalEpiCategory {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (R : CategoryTheory.Functor Cᵒᵖ RingCat) : CategoryTheory.IsNormalEpiCategory (PresheafOfModules R)

instance PresheafOfModules.instIsNormalMonoCategory {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (R : CategoryTheory.Functor Cᵒᵖ RingCat) : CategoryTheory.IsNormalMonoCategory (PresheafOfModules R)

noncomputable instance PresheafOfModules.instAbelian {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (R : CategoryTheory.Functor Cᵒᵖ RingCat) : CategoryTheory.Abelian (PresheafOfModules R)

Equations

• PresheafOfModules.instAbelian R = CategoryTheory.Abelian.mk