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.

Equations

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

@[simp]

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

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

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

The free-forgetful adjunction for abelian groups.

Equations

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

instance AddCommGrp.instIsLeftAdjointFree : AddCommGrp.free.IsLeftAdjoint

Equations

• AddCommGrp.instIsLeftAdjointFree = ⋯

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

Equations

• AddCommGrp.instIsRightAdjointForget = ⋯

instance AddCommGrp.instIsLeftAdjointFree_1 : AddCommGrp.free.IsLeftAdjoint

Equations

• AddCommGrp.instIsLeftAdjointFree_1 = ⋯

instance AddCommGrp.instPreservesMonomorphismsFree : AddCommGrp.free.PreservesMonomorphisms

Equations

• AddCommGrp.instPreservesMonomorphismsFree = ⋯

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.

Equations

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

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

The free-forgetful adjunction for groups.

Equations

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

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

Equations

• Grp.instIsRightAdjointForget = ⋯

def Grp.abelianize : CategoryTheory.Functor Grp CommGrp

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 Grp.abelianizeAdj : Grp.abelianize ⊣ CategoryTheory.forget₂ CommGrp Grp

The abelianization-forgetful adjuction from Group to CommGroup.

Equations

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

def MonCat.units : CategoryTheory.Functor MonCat Grp

The functor taking a monoid to its subgroup of units.

Equations

• MonCat.units = { obj := fun (R : MonCat) => Grp.of (↑R)ˣ, map := fun {X Y : MonCat} (f : X ⟶ Y) => Grp.ofHom (Units.map f), map_id := MonCat.units.proof_1, map_comp := @MonCat.units.proof_2 }

@[simp]

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

@[simp]

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

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

The forgetful-units adjunction between Grp and MonCat.

Equations

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

instance instIsRightAdjointGrpMonCatUnits : MonCat.units.IsRightAdjoint

Equations

• instIsRightAdjointGrpMonCatUnits = ⋯

def CommMonCat.units : CategoryTheory.Functor CommMonCat CommGrp

The functor taking a monoid to its subgroup of units.

Equations

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

@[simp]

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

@[simp]

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

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

The forgetful-units adjunction between CommGrp and CommMonCat.

Equations

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

instance instIsRightAdjointCommGrpCommMonCatUnits : CommMonCat.units.IsRightAdjoint

Equations

• instIsRightAdjointCommGrpCommMonCatUnits = ⋯