mathlib3 documentation

algebra.category.Group.adjunctions

Adjunctions regarding the category of (abelian) groups #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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}

def Mon.units :

The functor taking a monoid to its subgroup of units.

Equations

Mon.units = {obj := λ (R : Mon), Group.of (↥R)ˣ, map := λ (R S : Mon) (f : R ⟶ S), Group.of_hom (units.map f), map_id' := Mon.units._proof_1, map_comp' := Mon.units._proof_2}

Instances for Mon.units

Mon.units.category_theory.is_right_adjoint

@[simp]

theorem Mon.units_map (R S : Mon) (f : R ⟶ S) :

Mon.units.map f = Group.of_hom (units.map f)

@[simp]

theorem Mon.units_obj (R : Mon) :

Mon.units.obj R = Group.of (↥R)ˣ

def Group.forget₂_Mon_adj :

category_theory.forget₂ Group Mon ⊣ 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}

@[protected, instance]

def Mon.units.category_theory.is_right_adjoint :

category_theory.is_right_adjoint Mon.units

Equations

Mon.units.category_theory.is_right_adjoint = {left := category_theory.forget₂ Group Mon Group.has_forget_to_Mon, adj := Group.forget₂_Mon_adj}

def CommMon.units :

CommMon ⥤ CommGroup

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

CommMon.units.category_theory.is_right_adjoint

@[simp]

theorem CommMon.units_obj (R : CommMon) :

CommMon.units.obj R = CommGroup.of (↥R)ˣ

@[simp]

theorem CommMon.units_map (R S : CommMon) (f : R ⟶ S) :

CommMon.units.map f = CommGroup.of_hom (units.map f)

def CommGroup.forget₂_CommMon_adj :

category_theory.forget₂ CommGroup CommMon ⊣ 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}

@[protected, instance]

def CommMon.units.category_theory.is_right_adjoint :

category_theory.is_right_adjoint CommMon.units

Equations

CommMon.units.category_theory.is_right_adjoint = {left := category_theory.forget₂ CommGroup CommMon CommGroup.has_forget_to_CommMon, adj := CommGroup.forget₂_CommMon_adj}