units as a functor

Stream: Is there code for X?

[Yaël Dillies]

Do we have this functor anywhere?

import algebra.category.Group.basic

/-- `units` as a functor. -/
def Mon_to_Group : Mon ⥤ Group :=
{ obj := λ X, Group.of Xˣ,
  ... }

Am I right in thinking it is the free functor?

[Yaël Dillies]

I had to build the maps myself, so I suspect not.

[Eric Rodriguez]

curiosity: free functor seems to be the group completion, whose nlab article is way above my level

[Yaël Dillies]

The nLab article is about the commutative though, but I guess that doesn't change much?

[Eric Rodriguez]

i found the example in https://ncatlab.org/nlab/show/free+functor, seems the link is wrong there

[Kyle Miller]

The group-of-units functor is right adjoint to the forgetful functor, and the group completion functor (the result known as the universal enveloping group of a monoid in Bergman's book) is left adjoint to the forgetful functor.

These can be very different. Consider the monoid $\mathbb{N}$ under addition with its group of units ($\{0\}$) and its universal enveloping group ($\mathbb{Z}$).

[Yaël Dillies]

Ahah! I was right on one side at last.

[Yaël Dillies]

Thanks for the tip, Kyle. It turned out to be pretty easy.