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 #

Main statements #

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

Equations
@[simp]
theorem AddCommGroup.free_map_coe {α β : Type u} {f : α β} (x : free_abelian_group α) :

The free-forgetful adjunction for abelian groups.

Equations
def Group.free  :

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

Equations

The free-forgetful adjunction for groups.

Equations

The abelianization functor GroupCommGroup sending a group G to its abelianization Gᵃᵇ.

Equations

The functor taking a monoid to its subgroup of units.

Equations
Instances for Mon.units
@[simp]
theorem Mon.units_map (R S : Mon) (f : R S) :
@[simp]
theorem Mon.units_obj (R : Mon) :

The forgetful-units adjunction between Group and Mon.

Equations

The functor taking a monoid to its subgroup of units.

Equations
Instances for CommMon.units
@[simp]

The forgetful-units adjunction between CommGroup and CommMon.

Equations