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.{v_1, u_1} J] [CategoryTheory.Category.{v_2, u_2} C] [CategoryTheory.Limits.HasColimitsOfShape J C] [CategoryTheory.Preadditive C] : CategoryTheory.Limits.colim.Additive

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

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

instance instHasFilteredColimitsAddCommGrpCat : CategoryTheory.Limits.HasFilteredColimits AddCommGrpCat

instance instAB5AddCommGrpCat : CategoryTheory.AB5 AddCommGrpCat

instance Ab.hasFilteredColimitsOfSize [UnivLE.{u, w}] [UnivLE.{v, w}] : CategoryTheory.Limits.HasFilteredColimitsOfSize.{u, v, w, w + 1} Ab

instance Ab.ab5OfSize [UnivLE.{u, w}] [UnivLE.{v, w}] : CategoryTheory.AB5OfSize.{u, v, w, w + 1} Ab

instance instAB4AddCommGrpCat : CategoryTheory.AB4 AddCommGrpCat

instance instHasExactLimitsOfShapeDiscreteAddCommGrpCat {J : Type u} : CategoryTheory.HasExactLimitsOfShape (CategoryTheory.Discrete J) AddCommGrpCat

instance instAB4StarAddCommGrpCat : CategoryTheory.AB4Star AddCommGrpCat

instance instHasSeparatorAddCommGrpCat : CategoryTheory.HasSeparator AddCommGrpCat

instance instIsGrothendieckAbelianAddCommGrpCat : CategoryTheory.IsGrothendieckAbelian.{u, u, u + 1} AddCommGrpCat