mathlib documentation

algebra.category.Mon.adjunctions

Adjunctions regarding the category of monoids #

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

@[simp]
@[instance]
Equations

The adjoin_one-forgetful adjunction from Semigroup to Mon.

Equations