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 typeX
the free abelian group with generatorsx : X
.Group.free
: constructs the functor associating to a typeX
the free group with generatorsx : X
.abelianize
: constructs the functor which associates to a groupG
its abelianizationGᵃᵇ
.
Main statements #
AddCommGroup.adj
: proves thatAddCommGroup.free
is the left adjoint of the forgetful functor from abelian groups to types.Group.adj
: proves thatGroup.free
is the left adjoint of the forgetful functor from groups to types.abelianize_adj
: proves thatabelianize
is left adjoint to the forgetful functor from abelian groups to groups.
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]
@[simp]
theorem
AddCommGroup.free_map_coe
{α β : Type u}
{f : α → β}
(x : free_abelian_group α) :
⇑(AddCommGroup.free.map f) x = f <$> x
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}
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}
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}
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}
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}