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

• free-forgetful adjunction for monoids
• 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]
theorem adjoin_zero_map (X Y : AddSemigroup) (f : Y) :

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

The free-forgetful adjunction for monoids.

Equations
@[protected, instance]
Equations