Functors between monoids and groups

[ScriptRaccoon]

This PR adds 3 functors

• the forgetful functor Grp ---> Mon
• the group of units functor Mon ---> Grp (which is right adjoint to the forgetful functor)
• the enveloping group functor Mon ---> Grp (which is left adjoint to the forgetful functor)

All properties have been decided.