The category of abelian groups satisfies Grothendieck's axiom AB5 #
theorem
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
theorem
instPreservesHomologyFunctorAddCommGrpColim
{J : Type u}
[CategoryTheory.SmallCategory J]
[CategoryTheory.IsFiltered J]
:
CategoryTheory.Limits.colim.PreservesHomology
theorem
instPreservesFiniteLimitsFunctorAddCommGrpColim
{J : Type u}
[CategoryTheory.SmallCategory J]
[CategoryTheory.IsFiltered J]
:
CategoryTheory.Limits.PreservesFiniteLimits CategoryTheory.Limits.colim