Documentation
Mathlib
.
CategoryTheory
.
Abelian
.
GrothendieckAxioms
.
PresheafOfModules
Search
return to top
source
Imports
Init
Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit
Mathlib.Algebra.Category.Grp.FilteredColimits
Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Basic
Mathlib.CategoryTheory.Functor.ReflectsIso.Balanced
Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator
Imported by
PresheafOfModules
.
instIsGrothendieckAbelian
The category of presheaves of modules is Grothendieck abelian
#
source
instance
PresheafOfModules
.
instIsGrothendieckAbelian
{
C
:
Type
u}
[
CategoryTheory.SmallCategory
C
]
(
R
:
CategoryTheory.Functor
C
ᵒᵖ
RingCat
)
:
CategoryTheory.IsGrothendieckAbelian.{u, u, u + 1}
(
PresheafOfModules
R
)