Skip to content

Commit

Permalink
fixing the build
Browse files Browse the repository at this point in the history
  • Loading branch information
joelriou committed May 13, 2024
1 parent bfa64f7 commit 757e593
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions Mathlib/Algebra/Category/ModuleCat/Presheaf/Abelian.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down

0 comments on commit 757e593

Please sign in to comment.