Commit 2025-01-22 07:51 fb39772b
View on Github →feat(Algebra/Category/Grp/Ulift): the universe lifting functor for commutative 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 ℚ / ℤ.