Documentation

Mathlib.Algebra.Category.Grp.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
  • One or more equations did not get rendered due to their size.

The free-forgetful adjunction for abelian groups.

Equations
  • One or more equations did not get rendered due to their size.

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

Equations
  • One or more equations did not get rendered due to their size.

The free-forgetful adjunction for groups.

Equations
  • One or more equations did not get rendered due to their size.

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

Equations
  • One or more equations did not get rendered due to their size.

The abelianization-forgetful adjuction from Group to CommGroup.

Equations
  • One or more equations did not get rendered due to their size.

The functor taking a monoid to its subgroup of units.

Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem MonCat.val_units_map_hom_apply {X✝ Y✝ : MonCat} (f : X✝ Y✝) (u : (↑X✝)ˣ) :
@[simp]

The forgetful-units adjunction between Grp and MonCat.

Equations
  • One or more equations did not get rendered due to their size.

The functor taking a monoid to its subgroup of units.

Equations
  • One or more equations did not get rendered due to their size.
@[simp]

The forgetful-units adjunction between CommGrp and CommMonCat.

Equations
  • One or more equations did not get rendered due to their size.