Commit 2025-01-20 10:42 e43c7732

feat(Algebra/Category/Grp/LargeColimits): large colimits in the category of commutative additive groups (#20522) If F : J ⥤ AddCommGrp.{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.

• depends on: #20416
• depends on: #20512