mathlib3 documentation

algebra.category.Mon.adjunctions

Adjunctions regarding the category of monoids #

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

This file proves the adjunction between adjoining a unit to a semigroup and the forgetful functor from monoids to semigroups.

TODO #

The functor of adjoining a neutral element one to a semigroup.

Equations
@[simp]
@[simp]

The functor of adjoining a neutral element zero to a semigroup

Equations
@[simp]
@[protected, instance]
Equations
@[protected, instance]
Equations

The adjoin_one-forgetful adjunction from Semigroup to Mon.

Equations
def free  :

The free functor Type u ⥤ Mon sending a type X to the free monoid on X.

Equations

The free-forgetful adjunction for monoids.

Equations