English
There is an adjunction between the abelianization functor abelianize: GrpCat -> CommGrpCat and the forgetful functor forget₂ CommGrpCat GrpCat: GrpCat ⊣ forget₂ CommGrpCat GrpCat; equivalently, for every group G and abelian group H, Hom_CommGrp(abelianize(G), H) ≅ Hom_Grp(G, forget(H)).
Русский
Существует сопряжение между абелизацией абелилизационной функцией abelianize: GrpCat → CommGrpCat и забывательным функтором forget₂ CommGrpCat GrpCat: GrpCat ⊣ forget₂ CommGrpCat GrpCat; эквивалентно, для любой группы G и абелевой группы H: Hom_CommGrp(abelianize(G), H) ≅ Hom_Grp(G, forget(H)).
LaTeX
$$$\operatorname{Hom}_{\text{CommGrp}}(\operatorname{abelianize}(G), H) \cong \operatorname{Hom}_{\text{Grp}}(G, \operatorname{forget}_{\text{CommGrp}\to Grp}(H)).$$$
Lean4
/-- The free-forgetful adjunction for groups.
-/
def adj : free ⊣ forget GrpCat.{u} :=
Adjunction.mkOfHomEquiv
{ homEquiv := fun _ _ => ConcreteCategory.homEquiv.trans FreeGroup.lift.symm
homEquiv_naturality_left_symm := by
intros
ext : 1
-- Porting note (https://github.com/leanprover-community/mathlib4/issues/11041): `ext` doesn't apply this theorem anymore
apply FreeGroup.ext_hom
intros
rfl }
