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

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

Main statements

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

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

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

@[simp]

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

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

def AddCommGrp.adj : free ⊣ CategoryTheory.forget AddCommGrp

The free-forgetful adjunction for abelian groups.

instance AddCommGrp.instIsLeftAdjointFree : free.IsLeftAdjoint

instance AddCommGrp.instIsRightAdjointForget : (CategoryTheory.forget AddCommGrp).IsRightAdjoint

instance AddCommGrp.instPreservesMonomorphismsFree : free.PreservesMonomorphisms

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

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

def Grp.adj : free ⊣ CategoryTheory.forget Grp

The free-forgetful adjunction for groups.

instance Grp.instIsRightAdjointForget : (CategoryTheory.forget Grp).IsRightAdjoint

def Grp.abelianize : CategoryTheory.Functor Grp CommGrp

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

def Grp.abelianizeAdj : abelianize ⊣ CategoryTheory.forget₂ CommGrp Grp

The abelianization-forgetful adjunction from Group to CommGroup.

def MonCat.units : CategoryTheory.Functor MonCat Grp

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✝)ˣ) : ↑((Grp.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✝)ˣ) : ↑((Grp.Hom.hom (units.map f)) u)⁻¹ = (Hom.hom f) ↑u⁻¹

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

The forgetful-units adjunction between Grp and MonCat.

instance instIsRightAdjointGrpMonCatUnits : MonCat.units.IsRightAdjoint

def CommMonCat.units : CategoryTheory.Functor CommMonCat CommGrp

The functor taking a monoid to its subgroup of units.

@[simp]

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

@[simp]

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

@[simp]

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

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

The forgetful-units adjunction between CommGrp and CommMonCat.

instance instIsRightAdjointCommGrpCommMonCatUnits : CommMonCat.units.IsRightAdjoint