Commit 2021-02-10 21:01 6e52dfe3
View on Github →feat(algebra/category/Group/adjunctions): adjunction of abelianization and forgetful functor (#6154)
Abelianization has been defined in group_theory/abelianization without realising it in category theory. This PR adds this feature. Furthermore, a module doc for abelianization is added and the one for adjunctions is expanded.