Ken wrote:

> The problem with my approach on the boolean example seems to be that it's a bit hard to know what to do with -1 + -1.

Since 1+1 = 1 in the booleans, if we're creating a group where -1 is the inverse of 1 then we're forced to have -1 + -1 = -1. But that creates this "problem", which I was trying to inflict on you:

$$1 = 1 + 0 = 1 + (1 + -1) = (1 + 1) + -1 = 1 + -1 = 0.$$

In fact this "problem" is not really a problem, it's just a fact of life! Sometimes when you take a monoid and make it into a group by throwing in inverses of the existing elements, you get new equations between elements that weren't previously equal!

In particular, if you turn the boolean monoid into a group you get the trivial group, with 0 as its only element.

It's pretty easy to turn _commutative_ monoids into groups, as follows.

I hand you a commutative monoid \$$(M,+,0)\$$. You create a group where the elements are equivalence classes of "formal differences" \$$[x - y] \$$ where \$$x,y\in M\$$. "Formal" means that the minus sign is just a symbol. "Equivalence class" means that we decree

$$[x-y] = [x'-y'] \text{ if and only if } x + y' = x' + y$$

This is nice because if we really _could_ subtract, as we can in a commutative group, we would have \$$x - y = x' - y'\$$ if and only if \$$x + y' = x' + y\$$.

We can then define addition of these equivalence classes by

$$[x - y] + [x' - y'] := [(x+x') - (y+y')]$$

and we can define negatives of them by

$$-[x - y] := [y - x]$$

**Puzzle.** Show that this construction really gives a group, in fact a commutative group.

**Puzzle.** Show that if we apply this construction to the boolean monoid we get the trivial group.

**Puzzle.** Show that if we apply this construction to the natural numbers with its usual \$$+\$$ operation, we get the group of integers.

This construction actually gives rise to a left adjoint to the forgetful functor from _commutative_ groups (usually called abelian groups) to commutative monoids.

The noncommutative case requires more work - but luckily Anindya has sketched out how it goes in [comment #13](https://forum.azimuthproject.org/discussion/comment/19792/#Comment_19792). Basically instead of formal differences like \$$[x-y]\$$ we need fancier things like \$$[a_1 a_2^{-1} a_3 a_4^{-1} \dots ]\$$.