mathlib documentation

algebra.category.Group.adjunctions

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 AddCommGroup.free :

Type u ⥤ AddCommGroup

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

Equations

AddCommGroup.free = {obj := λ (α : Type u), AddCommGroup.of (free_abelian_group α), map := λ (X Y : Type u), free_abelian_group.map, map_id' := AddCommGroup.free._proof_1, map_comp' := AddCommGroup.free._proof_2}

@[simp]

theorem AddCommGroup.free_obj_coe {α : Type u} :

↥(AddCommGroup.free.obj α) = free_abelian_group α

@[simp]

theorem AddCommGroup.free_map_coe {α β : Type u} {f : α → β} (x : free_abelian_group α) :

⇑(AddCommGroup.free.map f) x = f <$> x

def AddCommGroup.adj :

AddCommGroup.free ⊣ category_theory.forget AddCommGroup

The free-forgetful adjunction for abelian groups.

Equations

AddCommGroup.adj = category_theory.adjunction.mk_of_hom_equiv {hom_equiv := λ (X : Type u) (G : AddCommGroup), free_abelian_group.lift.symm, hom_equiv_naturality_left_symm' := AddCommGroup.adj._proof_1, hom_equiv_naturality_right' := AddCommGroup.adj._proof_2}

@[protected, instance]

def AddCommGroup.category_theory.forget.category_theory.is_right_adjoint :

category_theory.is_right_adjoint (category_theory.forget AddCommGroup)

Equations

AddCommGroup.category_theory.forget.category_theory.is_right_adjoint = {left := AddCommGroup.free, adj := AddCommGroup.adj}

def Group.free :

Type u ⥤ Group

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

Equations

Group.free = {obj := λ (α : Type u), Group.of (free_group α), map := λ (X Y : Type u), free_group.map, map_id' := Group.free._proof_1, map_comp' := Group.free._proof_2}

def Group.adj :

Group.free ⊣ category_theory.forget Group

The free-forgetful adjunction for groups.

Equations

Group.adj = category_theory.adjunction.mk_of_hom_equiv {hom_equiv := λ (X : Type u) (G : Group), free_group.lift.symm, hom_equiv_naturality_left_symm' := Group.adj._proof_1, hom_equiv_naturality_right' := Group.adj._proof_2}

@[protected, instance]

def Group.category_theory.forget.category_theory.is_right_adjoint :

category_theory.is_right_adjoint (category_theory.forget Group)

Equations

Group.category_theory.forget.category_theory.is_right_adjoint = {left := Group.free, adj := Group.adj}

def abelianize :

Group ⥤ CommGroup

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

Equations

abelianize = {obj := λ (G : Group), {α := abelianization ↥G G.group, str := abelianization.comm_group ↥G G.group}, map := λ (G H : Group) (f : G ⟶ H), ⇑abelianization.lift {to_fun := λ (x : ↥G), ⇑abelianization.of (⇑f x), map_one' := _, map_mul' := _}, map_id' := abelianize._proof_3, map_comp' := abelianize._proof_4}

def abelianize_adj :

abelianize ⊣ category_theory.forget₂ CommGroup Group

The abelianization-forgetful adjuction from Group to CommGroup.

Equations

abelianize_adj = category_theory.adjunction.mk_of_hom_equiv {hom_equiv := λ (G : Group) (A : CommGroup), abelianization.lift.symm, hom_equiv_naturality_left_symm' := abelianize_adj._proof_1, hom_equiv_naturality_right' := abelianize_adj._proof_2}