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}
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}
Equations
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}
The functor taking a monoid to its subgroup of units.
Equations
Instances for Mon.units
The forgetful-units adjunction between Group
and Mon
.
Equations
- Group.forget₂_Mon_adj = {hom_equiv := λ (X : Group) (Y : Mon), {to_fun := λ (f : (category_theory.forget₂ Group Mon).obj X ⟶ Y), monoid_hom.to_hom_units f, inv_fun := λ (f : X ⟶ Mon.units.obj Y), (units.coe_hom ↥Y).comp f, left_inv := _, right_inv := _}, unit := {app := λ (X : Group), {to_fun := to_units.to_monoid_hom.to_fun, map_one' := _, map_mul' := _}, naturality' := Group.forget₂_Mon_adj._proof_5}, counit := {app := λ (X : Mon), units.coe_hom ↥X, naturality' := Group.forget₂_Mon_adj._proof_6}, hom_equiv_unit' := Group.forget₂_Mon_adj._proof_7, hom_equiv_counit' := Group.forget₂_Mon_adj._proof_8}
The functor taking a monoid to its subgroup of units.
Equations
- CommMon.units = {obj := λ (R : CommMon), CommGroup.of (↥R)ˣ, map := λ (R S : CommMon) (f : R ⟶ S), CommGroup.of_hom (units.map f), map_id' := CommMon.units._proof_1, map_comp' := CommMon.units._proof_2}
Instances for CommMon.units
The forgetful-units adjunction between CommGroup
and CommMon
.
Equations
- CommGroup.forget₂_CommMon_adj = {hom_equiv := λ (X : CommGroup) (Y : CommMon), {to_fun := λ (f : (category_theory.forget₂ CommGroup CommMon).obj X ⟶ Y), monoid_hom.to_hom_units f, inv_fun := λ (f : X ⟶ CommMon.units.obj Y), (units.coe_hom ↥Y).comp f, left_inv := _, right_inv := _}, unit := {app := λ (X : CommGroup), {to_fun := to_units.to_monoid_hom.to_fun, map_one' := _, map_mul' := _}, naturality' := CommGroup.forget₂_CommMon_adj._proof_5}, counit := {app := λ (X : CommMon), units.coe_hom ↥X, naturality' := CommGroup.forget₂_CommMon_adj._proof_6}, hom_equiv_unit' := CommGroup.forget₂_CommMon_adj._proof_7, hom_equiv_counit' := CommGroup.forget₂_CommMon_adj._proof_8}