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.

def AddCommGroupCat.free : CategoryTheory.Functor (Type u) AddCommGroupCat

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

@[simp]

theorem AddCommGroupCat.free_obj_coe {α : Type u} : ↑(AddCommGroupCat.free.obj α) = FreeAbelianGroup α

@[simp]

theorem AddCommGroupCat.free_map_coe {α : Type u} {β : Type u} {f : α → β} (x : FreeAbelianGroup α) : ↑(AddCommGroupCat.free.map f) x = f <$> x

def AddCommGroupCat.adj : AddCommGroupCat.free ⊣ CategoryTheory.forget AddCommGroupCat

The free-forgetful adjunction for abelian groups.

instance AddCommGroupCat.instIsRightAdjointTypeTypesAddCommGroupCatInstAddCommGroupCatLargeCategoryForgetConcreteCategory : CategoryTheory.IsRightAdjoint (CategoryTheory.forget AddCommGroupCat)

def GroupCat.free : CategoryTheory.Functor (Type u) GroupCat

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

def GroupCat.adj : GroupCat.free ⊣ CategoryTheory.forget GroupCat

The free-forgetful adjunction for groups.

instance GroupCat.instIsRightAdjointTypeTypesGroupCatInstGroupCatLargeCategoryForgetConcreteCategory : CategoryTheory.IsRightAdjoint (CategoryTheory.forget GroupCat)

def abelianize : CategoryTheory.Functor GroupCat CommGroupCat

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

def abelianizeAdj : abelianize ⊣ CategoryTheory.forget₂ CommGroupCat GroupCat

The abelianization-forgetful adjuction from Group to CommGroup.

@[simp]

theorem MonCat.units_map : ∀ {X Y : MonCat} (f : X ⟶ Y), MonCat.units.map f = GroupCat.ofHom (Units.map f)

@[simp]

theorem MonCat.units_obj (R : MonCat) : MonCat.units.obj R = GroupCat.of (↑R)ˣ

def MonCat.units : CategoryTheory.Functor MonCat GroupCat

The functor taking a monoid to its subgroup of units.

def GroupCat.forget₂MonAdj : CategoryTheory.forget₂ GroupCat MonCat ⊣ MonCat.units

The forgetful-units adjunction between Group and Mon.

instance instIsRightAdjointGroupCatInstGroupCatLargeCategoryMonCatInstMonCatLargeCategoryUnits : CategoryTheory.IsRightAdjoint MonCat.units

@[simp]

theorem CommMonCat.units_obj (R : CommMonCat) : CommMonCat.units.obj R = CommGroupCat.of (↑R)ˣ

@[simp]

theorem CommMonCat.units_map : ∀ {X Y : CommMonCat} (f : X ⟶ Y), CommMonCat.units.map f = CommGroupCat.ofHom (Units.map f)

def CommMonCat.units : CategoryTheory.Functor CommMonCat CommGroupCat

The functor taking a monoid to its subgroup of units.

def CommGroupCat.forget₂CommMonAdj : CategoryTheory.forget₂ CommGroupCat CommMonCat ⊣ CommMonCat.units

The forgetful-units adjunction between CommGroup and CommMon.

instance instIsRightAdjointCommGroupCatInstCommGroupCatLargeCategoryCommMonCatInstCommMonCatLargeCategoryUnits : CategoryTheory.IsRightAdjoint CommMonCat.units