# Adjunctions regarding the category of (abelian) groups #

This file contains construction of basic adjunctions concerning the category of groups and the category of abelian groups.

## Main definitions #

• AddCommGroup.free: constructs the functor associating to a type X the free abelian group with generators x : X.
• Group.free: constructs the functor associating to a type X the free group with generators x : X.
• abelianize: constructs the functor which associates to a group G its abelianization Gᵃᵇ.

## Main statements #

• AddCommGroup.adj: proves that AddCommGroup.free is the left adjoint of the forgetful functor from abelian groups to types.
• Group.adj: proves that Group.free is the left adjoint of the forgetful functor from groups to types.
• abelianize_adj: proves that abelianize is left adjoint to the forgetful functor from abelian groups to groups.

The free functor Type u ⥤ AddCommGroup sending a type X to the free abelian group with generators x : X.

Equations
@[simp]
theorem AddCommGroup.free_obj_coe {α : Type u} :
@[simp]
theorem AddCommGroup.free_map_coe {α β : Type u} {f : α → β} (x : free_abelian_group α) :
x = f <\$> x

The free-forgetful adjunction for abelian groups.

Equations
@[instance]
Equations
def Group.free  :
Type u Group

The free functor Type u ⥤ Group sending a type X to the free group with generators x : X.

Equations

The abelianization functor Group ⥤ CommGroup sending a group G to its abelianization Gᵃᵇ.
The abelianization-forgetful adjuction from Group to CommGroup.