Commit 2025-01-01 20:42 c781ca86
View on Github →feat(Algebra/Category/Grp/Ulift): some properties of the universe lift functor for groups. (#19968) Prove some basic properties of the universe lift functor for groups:
- It is fully faithful.
- It preserves all limits and creates small limits.
- On the category of additive commutative groups, it preserves zero morphisms and is an additive functor. TODO: colimits.
- depends on: #19966