mathlib3

6e52dfe3 - feat(algebra/category/Group/adjunctions): adjunction of abelianization and forgetful functor (#6154)

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. Co-authored-by: Julian-Kuelshammer <68201724+Julian-Kuelshammer@users.noreply.github.com>