The category of abelian groups satisfies Grothendieck's axiom AB5 #
instance
instAdditiveFunctorColim
{J : Type u_1}
{C : Type u_2}
[CategoryTheory.Category.{u_3, u_1} J]
[CategoryTheory.Category.{u_4, u_2} C]
[CategoryTheory.Limits.HasColimitsOfShape J C]
[CategoryTheory.Preadditive C]
:
CategoryTheory.Limits.colim.Additive
Equations
- ⋯ = ⋯
noncomputable instance
instPreservesHomologyFunctorAddCommGrpColim
{J : Type u}
[CategoryTheory.SmallCategory J]
[CategoryTheory.IsFiltered J]
:
CategoryTheory.Limits.colim.PreservesHomology
Equations
- instPreservesHomologyFunctorAddCommGrpColim = CategoryTheory.Limits.colim.preservesHomologyOfMapExact ⋯
noncomputable instance
instPreservesFiniteLimitsFunctorAddCommGrpColim
{J : Type u}
[CategoryTheory.SmallCategory J]
[CategoryTheory.IsFiltered J]
:
CategoryTheory.Limits.PreservesFiniteLimits CategoryTheory.Limits.colim
Equations
- instPreservesFiniteLimitsFunctorAddCommGrpColim = CategoryTheory.Limits.colim.preservesFiniteLimitsOfPreservesHomology