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 #

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  :
Type u Group

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