Commit 2025-01-06 12:15 5b6f2c61
View on Github →refactor(Algebra/Category/Grp/Colimits): change the construction of colimits in AddCommGrp
(#20474)
The old version of this file has a remark saying "TODO: In fact, in AddCommGrp
there is a much nicer model of colimits as quotients of finitely supported functions, and we really should implement this as well (or instead)."
This PR does precisely this (choosing the "instead" option). In fact, given a functor F : J ⥤ AddCommGrp.{w}
, it constructs a candidate for the colimit of F
as a quotient of DFinsupp (fun j ↦ F.obj j)
, without any smallness assumptions on J
. It then proves that this quotient is a colimit of F
if it is w
-small, then deduces that AddCommGrp.{w}
has all small colimits.