English
The abelianization functor abelianize: GrpCat → CommGrpCat is left adjoint to forgetting functor forget₂ CommGrpCat GrpCat; equivalently, Hom_CommGrp(abelianize(G), A) ≅ Hom_Grp(G, forget(A)) natural in G and A.
Русский
Функтор абелизации abelianize: GrpCat → CommGrpCat является левым сопряжением к забывательному функтору forget₂ CommGrpCat GrpCat; эквивалентно, Hom_CommGrp(abelianize(G), A) ≅ Hom_Grp(G, forget(A)) естественно по G и A.
LaTeX
$$$\operatorname{Hom}_{\text{CommGrp}}(\operatorname{abelianize}(G), A) \cong \operatorname{Hom}_{\text{Grp}}(G, \operatorname{forget}_{\text{CommGrp} \to Grp}(A)).$$$
Lean4
/-- The abelianization-forgetful adjunction from `Group` to `CommGroup`. -/
def abelianizeAdj : abelianize ⊣ forget₂ CommGrpCat.{u} GrpCat.{u} :=
Adjunction.mkOfHomEquiv
{ homEquiv := fun _ _ =>
((ConcreteCategory.homEquiv (C := CommGrpCat)).trans Abelianization.lift.symm).trans
(ConcreteCategory.homEquiv (C := GrpCat)).symm
homEquiv_naturality_left_symm := by
intros
ext
simp only
apply Eq.symm
apply Abelianization.lift_unique
intros
apply Abelianization.lift_apply_of }
