Documentation

Mathlib.Algebra.Category.ModuleCat.Presheaf.Abelian

The category of presheaves of modules is abelian #

source
noncomputable instance PresheafOfModules.instNormalEpiCategory {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (R : CategoryTheory.Functor Cᵒᵖ RingCat) :
CategoryTheory.NormalEpiCategory (PresheafOfModules R)
Equations
  • One or more equations did not get rendered due to their size.
source
noncomputable instance PresheafOfModules.instNormalMonoCategory {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (R : CategoryTheory.Functor Cᵒᵖ RingCat) :
CategoryTheory.NormalMonoCategory (PresheafOfModules R)
Equations
  • One or more equations did not get rendered due to their size.
source
noncomputable instance PresheafOfModules.instAbelian {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (R : CategoryTheory.Functor Cᵒᵖ RingCat) :
CategoryTheory.Abelian (PresheafOfModules R)
Equations