# Adjunctions regarding the category of (abelian) groups #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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
@[protected, instance]
Equations
def Group.free  :

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

Equations

Equations
@[protected, instance]
Equations

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

Equations

The abelianization-forgetful adjuction from Group to CommGroup.

Equations
def Mon.units  :

The functor taking a monoid to its subgroup of units.

Equations
Instances for Mon.units
@[simp]
theorem Mon.units_map (R S : Mon) (f : R S) :
@[simp]
theorem Mon.units_obj (R : Mon) :

The forgetful-units adjunction between Group and Mon.

Equations
@[protected, instance]
Equations

The functor taking a monoid to its subgroup of units.

Equations
Instances for CommMon.units
@[simp]
theorem CommMon.units_obj (R : CommMon) :
@[simp]
theorem CommMon.units_map (R S : CommMon) (f : R S) :

The forgetful-units adjunction between CommGroup and CommMon.

Equations
@[protected, instance]
Equations