Existence of "big" colimits in the category of additive commutative groups

If F : J ⥤ AddCommGrpCat.{w} is a functor, we show that F admits a colimit if and only if Colimits.Quot F (the quotient of the direct sum of the commutative groups F.obj j by the relations given by the morphisms in the diagram) is w-small.

theorem AddCommGrpCat.isColimit_iff_bijective_desc {J : Type u} [CategoryTheory.Category.{v, u} J] {F : CategoryTheory.Functor J AddCommGrpCat} (c : CategoryTheory.Limits.Cocone F) [DecidableEq J] : Nonempty (CategoryTheory.Limits.IsColimit c) ↔ Function.Bijective ⇑(Colimits.Quot.desc F c)

If c is a cocone of F such that Quot.desc F c is bijective, then c is a colimit cocone of F.

theorem AddCommGrpCat.hasColimit_iff_small_quot {J : Type u} [CategoryTheory.Category.{v, u} J] {F : CategoryTheory.Functor J AddCommGrpCat} [DecidableEq J] : CategoryTheory.Limits.HasColimit F ↔ Small.{w, max u w} (Colimits.Quot F)

A functor F : J ⥤ AddCommGrpCat.{w} has a colimit if and only if Colimits.Quot F is w-small.