Commit 2024-04-19 14:49 e8ccef95
View on Github →feat: the forget functor from commutative groups to groups preserves all limits (#11669)
It is shown in this PR that the forget functor from commutative groups to groups preserves all limits (regardless of the universe parameters of the index category). It is also shown that a functor F : J ⥤ CommGroupCat (or F : J ⥤ GroupCat) has a limit iff the type (F ⋙ forget _).sections is small. This is related to the fact that the forget functor CommGroupCat.{u} ⥤ Type u is corepresentable (by ULift ℤ).