AB axioms for the category of abelian groups

This file proves that the category of abelian groups satisfies Grothendieck's axioms AB5, AB4, and AB4*.

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

instance instPreservesHomologyFunctorAddCommGrpColim {J : Type u} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] : CategoryTheory.Limits.colim.PreservesHomology

instance instPreservesFiniteLimitsFunctorAddCommGrpColim {J : Type u} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] : CategoryTheory.Limits.PreservesFiniteLimits CategoryTheory.Limits.colim

instance instHasFilteredColimitsAddCommGrp : CategoryTheory.Limits.HasFilteredColimits AddCommGrp

instance instAB5AddCommGrp : CategoryTheory.AB5 AddCommGrp

instance instAB4AddCommGrp : CategoryTheory.AB4 AddCommGrp

instance instHasExactLimitsOfShapeDiscreteAddCommGrp {J : Type u} : CategoryTheory.HasExactLimitsOfShape (CategoryTheory.Discrete J) AddCommGrp

instance instAB4StarAddCommGrp : CategoryTheory.AB4Star AddCommGrp