diff --git a/Mathlib/Algebra/Category/ModuleCat/Presheaf/Abelian.lean b/Mathlib/Algebra/Category/ModuleCat/Presheaf/Abelian.lean index 947671445a5df..80d80075b9e8a 100644 --- a/Mathlib/Algebra/Category/ModuleCat/Presheaf/Abelian.lean +++ b/Mathlib/Algebra/Category/ModuleCat/Presheaf/Abelian.lean @@ -24,12 +24,12 @@ 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πKernelConditionOfEpi _ _)) + Abelian.isColimitMapCoconeOfCokernelCoforkOfπ _ _)) noncomputable instance : NormalMonoCategory (PresheafOfModules.{v} R) where normalMonoOfMono i _ := NormalMono.mk _ (cokernel.π i) (cokernel.condition _) (evaluationJointlyReflectsLimits _ _ (fun _ => - Abelian.isLimitMapConeOfKernelForkOfιCokernelConditionOfMono _ _)) + Abelian.isLimitMapConeOfKernelForkOfι _ _)) noncomputable instance : Abelian (PresheafOfModules.{v} R) where