feat(Algebra/Category/ModuleCat): the category of presheaves of modul…

…es is abelian (#12721)

Mathlib.lean

@@ -88,6 +88,7 @@ import Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
 import Mathlib.Algebra.Category.ModuleCat.Monoidal.Closed
 import Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric
 import Mathlib.Algebra.Category.ModuleCat.Presheaf
+import Mathlib.Algebra.Category.ModuleCat.Presheaf.Abelian
 import Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits
 import Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits
 import Mathlib.Algebra.Category.ModuleCat.Products

Mathlib/Algebra/Category/ModuleCat/Presheaf.lean

@@ -224,6 +224,8 @@ def evaluation (X : Cᵒᵖ) : PresheafOfModules.{v} R ⥤ ModuleCat (R.obj X) w
   obj M := M.obj X
   map f := f.app X
 
+instance (X : Cᵒᵖ) : (evaluation R X).Additive where
+
 variable {R}
 
 /-- Given a presheaf of modules `M` on a category `C` and `f : X ⟶ Y` in `Cᵒᵖ`, this

Mathlib/Algebra/Category/ModuleCat/Presheaf/Abelian.lean

@@ -0,0 +1,36 @@
+/-
+Copyright (c) 2024 Joël Riou. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joël Riou
+-/
+import Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits
+import Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits
+import Mathlib.Algebra.Category.ModuleCat.Abelian
+import Mathlib.CategoryTheory.Abelian.Basic
+
+/-!
+# The category of presheaves of modules is abelian
+
+-/
+
+universe v v₁ u₁ u
+
+open CategoryTheory Category Limits
+
+namespace PresheafOfModules
+
+variable {C : Type u₁} [Category.{v₁} C] (R : Cᵒᵖ ⥤ RingCat.{u})
+
+noncomputable instance : NormalEpiCategory (PresheafOfModules.{v} R) where
+  normalEpiOfEpi p _ := NormalEpi.mk _ (kernel.ι p)  (kernel.condition _)
+    (evaluationJointlyReflectsColimits _ _ (fun _ =>
+      Abelian.isColimitMapCoconeOfCokernelCoforkOfπ _ _))
+
+noncomputable instance : NormalMonoCategory (PresheafOfModules.{v} R) where
+  normalMonoOfMono i _ := NormalMono.mk _ (cokernel.π i) (cokernel.condition _)
+    (evaluationJointlyReflectsLimits _ _ (fun _ =>
+      Abelian.isLimitMapConeOfKernelForkOfι _ _))
+
+noncomputable instance : Abelian (PresheafOfModules.{v} R) where
+
+end PresheafOfModules