Properties of the universe lift functor for groups #

This file shows that the functors Grp.uliftFunctor and CommGrp.uliftFunctor (as well as the additive versions) are fully faithful, preserves all limits and create small limits.

Full faithfulness is pretty obvious. To prove that the functors preserves limits, we use the fact that the forgetful functor from Grp or CommGrp into Type creates all limits (because of the way limits are constructed in Grp and CommGrp), and that the universe lift functor on Type preserves all limits. Once we know that Grp.uliftFunctor preserves all limits and is fully faithful, it will automatically create all limits that exist, i.e. all small ones.

We then switch to AddCommGrp and show that AddCommGrp.uliftFunctor preserves zero morphisms and is an additive functor, which again is pretty obvious.

The last result is a proof that AddCommGrp.uliftFunctor preserves all colimits (and hence creates small colimits). This is the only non-formal part of this file, as we follow the same strategy as for the categories Type.

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 ℚ / ℤ.

Note that this does not work for noncommutative groups, because the existence of simple groups of arbitrary size implies that a general object G of Grp is not determined by the restriction of coyoneda.obj G to the category of groups at a smaller universe level. Indeed, the functor Grp.uliftFunctor does not commute with arbitrary colimits: if we take an increasing family K of simple groups in Grp.{u} of unbounded cardinality indexed by a linearly ordered type (for example finitary alternating groups on a family of types in u of unbouded cardinality), then the colimit of K in Grp.{u} exists and is the trivial group; meanwhile, the colimit of K ⋙ Grp.uliftFunctor.{u + 1} is nontrivial (it is the "union" of all the K j, which is too big to be in Grp.{u}).