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.

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.

Equations

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

@[simp]

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

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.

Equations

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

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

Equations

• AddCommGroupCat.instIsRightAdjointForget = { left := AddCommGroupCat.free, adj := AddCommGroupCat.adj }

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.

Equations

• GroupCat.free = { obj := fun (α : Type u) => GroupCat.of (FreeGroup α), map := fun {X Y : Type u} => FreeGroup.map, map_id := GroupCat.free.proof_1, map_comp := @GroupCat.free.proof_2 }

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

The free-forgetful adjunction for groups.

Equations

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

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

Equations

• GroupCat.instIsRightAdjointForget = { left := GroupCat.free, adj := GroupCat.adj }

def abelianize : CategoryTheory.Functor GroupCat CommGroupCat

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.

def abelianizeAdj : abelianize ⊣ CategoryTheory.forget₂ CommGroupCat GroupCat

The abelianization-forgetful adjuction from Group to CommGroup.

Equations

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

@[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.

Equations

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

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

The forgetful-units adjunction between GroupCat and MonCat.

Equations

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

instance instIsRightAdjointGroupCatMonCatUnits : CategoryTheory.IsRightAdjoint MonCat.units

Equations

• instIsRightAdjointGroupCatMonCatUnits = { left := CategoryTheory.forget₂ GroupCat MonCat, adj := GroupCat.forget₂MonAdj }

@[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.

Equations

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

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

The forgetful-units adjunction between CommGroupCat and CommMonCat.

Equations

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

instance instIsRightAdjointCommGroupCatCommMonCatUnits : CategoryTheory.IsRightAdjoint CommMonCat.units

Equations

• instIsRightAdjointCommGroupCatCommMonCatUnits = { left := CategoryTheory.forget₂ CommGroupCat CommMonCat, adj := CommGroupCat.forget₂CommMonAdj }