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 ]\\).