# 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 #

• AddCommGroupCat.free: constructs the functor associating to a type X the free abelian group with generators x : X.
• GroupCat.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 #

• AddCommGroupCat.adj: proves that AddCommGroupCat.free is the left adjoint of the forgetful functor from abelian groups to types.
• GroupCat.adj: proves that GroupCat.free is the left adjoint of the forgetful functor from groups to types.
• abelianizeAdj: 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
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem AddCommGroupCat.free_obj_coe {α : Type u} :
( α) =
theorem AddCommGroupCat.free_map_coe {α : Type u} {β : Type u} {f : αβ} (x : ) :
( f) x = f <\$> x

The free-forgetful adjunction for abelian groups.

Equations
• One or more equations did not get rendered due to their size.
Instances For
Equations

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

Equations
Instances For

Equations
• One or more equations did not get rendered due to their size.
Instances For
Equations

The abelianization functor Group ⥤ CommGroup sending a group G to its abelianization Gᵃᵇ.

Equations
• One or more equations did not get rendered due to their size.
Instances For

The abelianization-forgetful adjuction from Group to CommGroup.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem MonCat.units_map :
∀ {X Y : MonCat} (f : X Y), MonCat.units.map f =
@[simp]
theorem MonCat.units_obj (R : MonCat) :

The functor taking a monoid to its subgroup of units.

Equations
• One or more equations did not get rendered due to their size.
Instances For

The forgetful-units adjunction between GroupCat and MonCat.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CommMonCat.units_map :
∀ {X Y : CommMonCat} (f : X Y), CommMonCat.units.map f =

The functor taking a monoid to its subgroup of units.

Equations
• One or more equations did not get rendered due to their size.
Instances For

The forgetful-units adjunction between CommGroupCat and CommMonCat.

Equations
• One or more equations did not get rendered due to their size.
Instances For