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)

@[instance_reducible]

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

Equations

• One or more equations did not get rendered due to their size.