# 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 #

• adjunctions related to commutative monoids

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

Equations
@[simp]
theorem adjoin_one_map (X Y : Semigroup) (f : X →ₙ* Y) :
@[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 AddSemigroup to AddMon

Equations

The adjoin_one-forgetful adjunction from Semigroup to Mon.

Equations
def free  :
Type u Mon

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

Equations