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.

Equations

• AddCommGroupCat.free = CategoryTheory.Functor.mk { obj := fun (α : Type u) => AddCommGroupCat.of (FreeAbelianGroup α), map := fun {X Y : Type u} => FreeAbelianGroup.map }

@[simp]

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

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

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

The free-forgetful adjunction for abelian groups.

Equations

• AddCommGroupCat.adj = CategoryTheory.Adjunction.mkOfHomEquiv (CategoryTheory.Adjunction.CoreHomEquiv.mk fun (X : Type u) (G : AddCommGroupCat) => FreeAbelianGroup.lift.symm)

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

Equations

• AddCommGroupCat.instIsRightAdjointTypeTypesAddCommGroupCatInstAddCommGroupCatLargeCategoryForgetConcreteCategory = { 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 = CategoryTheory.Functor.mk { obj := fun (α : Type u) => GroupCat.of (FreeGroup α), map := fun {X Y : Type u} => FreeGroup.map }

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

The free-forgetful adjunction for groups.

Equations

• GroupCat.adj = CategoryTheory.Adjunction.mkOfHomEquiv (CategoryTheory.Adjunction.CoreHomEquiv.mk fun (X : Type u) (G : GroupCat) => FreeGroup.lift.symm)

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

Equations

• GroupCat.instIsRightAdjointTypeTypesGroupCatInstGroupCatLargeCategoryForgetConcreteCategory = { 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

• abelianizeAdj = CategoryTheory.Adjunction.mkOfHomEquiv (CategoryTheory.Adjunction.CoreHomEquiv.mk fun (G : GroupCat) (A : CommGroupCat) => Abelianization.lift.symm)

@[simp]

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

@[simp]

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

def MonCat.units : CategoryTheory.Functor MonCat GroupCat

The functor taking a monoid to its subgroup of units.

Equations

• MonCat.units = CategoryTheory.Functor.mk { obj := fun (R : MonCat) => GroupCat.of (↑R)ˣ, map := fun {X Y : MonCat} (f : X ⟶ Y) => GroupCat.ofHom (Units.map f) }

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

The forgetful-units adjunction between Group and Mon.

Equations

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

instance instIsRightAdjointGroupCatInstGroupCatLargeCategoryMonCatInstMonCatLargeCategoryUnits : CategoryTheory.IsRightAdjoint MonCat.units

Equations

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

@[simp]

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

@[simp]

theorem CommMonCat.units_map : ∀ {X Y : CommMonCat} (f : X ⟶ Y), CommMonCat.units.toPrefunctor.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

• CommMonCat.units = CategoryTheory.Functor.mk { obj := fun (R : CommMonCat) => CommGroupCat.of (↑R)ˣ, map := fun {X Y : CommMonCat} (f : X ⟶ Y) => CommGroupCat.ofHom (Units.map f) }

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

The forgetful-units adjunction between CommGroup and CommMon.

Equations

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

instance instIsRightAdjointCommGroupCatInstCommGroupCatLargeCategoryCommMonCatInstCommMonCatLargeCategoryUnits : CategoryTheory.IsRightAdjoint CommMonCat.units

Equations

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