# 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 : Y) :
@[simp]
@[simp]

The functor of adjoining a neutral element zero to a semigroup

@[simp]
@[instance]
Equations
@[instance]

The adjoin_one-forgetful adjunction from AddSemigroup to AddMon

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