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

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

Main statements

• AddCommGrpCat.adj: proves that AddCommGrpCat.free is the left adjoint of the forgetful functor from abelian groups to types.
• GrpCat.adj: proves that GrpCat.free is the left adjoint of the forgetful functor from groups to types.
• abelianizeAdj: proves that GrpCat.abelianize is left adjoint to the forgetful functor from abelian groups to groups.

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

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

@[simp]

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

theorem AddCommGrpCat.free_map_coe {α β : Type u} {f : α → β} (x : FreeAbelianGroup α) : (CategoryTheory.ConcreteCategory.hom (free.map f)) x = f <$> x

def AddCommGrpCat.adj : free ⊣ CategoryTheory.forget AddCommGrpCat

The free-forgetful adjunction for abelian groups.

instance AddCommGrpCat.instIsLeftAdjointFree : free.IsLeftAdjoint

instance AddCommGrpCat.instIsRightAdjointForgetAddMonoidHomCarrier : (CategoryTheory.forget AddCommGrpCat).IsRightAdjoint

instance AddCommGrpCat.instPreservesMonomorphismsFree : free.PreservesMonomorphisms

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

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

def GrpCat.adj : free ⊣ CategoryTheory.forget GrpCat

The free-forgetful adjunction for groups.

instance GrpCat.instIsRightAdjointForgetMonoidHomCarrier : (CategoryTheory.forget GrpCat).IsRightAdjoint

def GrpCat.abelianize : CategoryTheory.Functor GrpCat CommGrpCat

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

def GrpCat.abelianizeAdj : abelianize ⊣ CategoryTheory.forget₂ CommGrpCat GrpCat

The abelianization-forgetful adjunction from Group to CommGroup.

def MonCat.units : CategoryTheory.Functor MonCat GrpCat

The functor taking a monoid to its subgroup of units.

@[simp]

theorem MonCat.val_units_map_hom_apply {X✝ Y✝ : MonCat} (f : X✝ ⟶ Y✝) (u : (↑X✝)ˣ) : ↑((GrpCat.Hom.hom (units.map f)) u) = (Hom.hom f) ↑u

@[simp]

theorem MonCat.units_obj_coe (R : MonCat) : ↑(units.obj R) = (↑R)ˣ

@[simp]

theorem MonCat.val_inv_units_map_hom_apply {X✝ Y✝ : MonCat} (f : X✝ ⟶ Y✝) (u : (↑X✝)ˣ) : ↑((GrpCat.Hom.hom (units.map f)) u)⁻¹ = (Hom.hom f) ↑u⁻¹

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

The forgetful-units adjunction between GrpCat and MonCat.

instance instIsRightAdjointGrpCatMonCatUnits : MonCat.units.IsRightAdjoint

def CommMonCat.units : CategoryTheory.Functor CommMonCat CommGrpCat

The functor taking a monoid to its subgroup of units.

@[simp]

theorem CommMonCat.val_units_map_hom_apply {X✝ Y✝ : CommMonCat} (f : X✝ ⟶ Y✝) (u : (↑X✝)ˣ) : ↑((CommGrpCat.Hom.hom (units.map f)) u) = (Hom.hom f) ↑u

@[simp]

theorem CommMonCat.val_inv_units_map_hom_apply {X✝ Y✝ : CommMonCat} (f : X✝ ⟶ Y✝) (u : (↑X✝)ˣ) : ↑((CommGrpCat.Hom.hom (units.map f)) u)⁻¹ = (Hom.hom f) ↑u⁻¹

@[simp]

theorem CommMonCat.units_obj_coe (R : CommMonCat) : ↑(units.obj R) = (↑R)ˣ

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

The forgetful-units adjunction between CommGrpCat and CommMonCat.

instance instIsRightAdjointCommGrpCatCommMonCatUnits : CommMonCat.units.IsRightAdjoint