…ory 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.

- [x] depends on: #20416
- [x] depends on: #20512



Co-authored-by: smorel394 <67864981+smorel394@users.noreply.github.com>

…mmutative additive groups preserves colimits (#20417)

Prove that the functor `AddCommGrp.ulift` preserves all colimits, hence creates small colimits. (This also finished the proof that it is an exact functor.)

Method: Suppose that we have a functor `K : J ⥤ AddCommGrp.{u}` (with `J` any category), a
colimit cocone `c` of `K` and a cocone `lc` of `K ⋙ uliftFunctor.{u v}`. We want to
construct a morphism of cocones `uliftFunctor.mapCocone c → lc` witnessing the fact
that `uliftFunctor.mapCocone c` is also a colimit cocone, but we have no direct way
to do this. The idea is to use that `AddCommGrp.{max v u}` has a small cogenerator,
which is just the additive (rational) circle `ℚ / ℤ`, so any abelian group of
any size can be recovered from its morphisms into `ℚ / ℤ`. More precisely, the functor
sending an abelian group `A` to its dual `A →+ ℚ / ℤ` is fully faithful, *if* we consider
the dual as a (right) module over the endomorphism ring of `ℚ / ℤ`. So an abelian
group `C` is totally determined by the restriction of the coyoneda
functor `A ↦ (C →+ A)` to the category of abelian groups at a smaller universe level.
We do not develop this totally here but do a direct construction. Every time we have
a morphism from `lc.pt` into `ℚ / ℤ`, or more generally into any small abelian group
`A`, we can construct a cocone of `K ⋙ uliftFunctor` by sticking `ULift A` at the
cocone point (this is `CategoryTheory.Limits.Cocone.extensions`), and this cocone is
actually made up of `u`-small abelian groups, hence gives a cocone of `K`. Using
the universal property of `c`, we get a morphism `c.pt →+ A`. So we have constructed
a map `(lc.pt →+ A) → (c.pt →+ A)`, and it is easy to prove that it is compatible with
postcomposition of morphisms of small abelian groups. To actually get the
morphism `c.pt →+ lc.pt`, we apply this to the canonical embedding of `lc.pt` into
`Π (_ : lc.pt →+ ℚ / ℤ), ℚ / ℤ` (this group is not small but is a product of small
groups, so our construction extends). To show that the image of `c.pt` in this product
is contained in that of `lc.pt`, we use the compatibility with postcomposition and the
fact that we can detect elements of the image just by applying morphisms from
`Π (_ : lc.pt →+ ℚ / ℤ), ℚ / ℤ` to `ℚ / ℤ`.

- [x] depends on: #20416
- [x] depends on: #20512
- [x] depends on: #20522