I want to construct the group $\mathbb{Q}\setminus 0$, the nonzero rational numbers under multiplication, from the monoid $\mathbb{Z}\setminus 0$ using the Grothendieck group construction.
First I form the free abelian group $F\langle\mathbb{Z}\setminus 0\rangle$. I'll use [x] to denote the symbols in this group. The Grothendieck group construction is $$F\langle\mathbb{Z}\setminus 0\rangle/B$$ $$\text{B generated by }[xy]-[x]-[y]$$
I did a lot of playing with the elements of this factor group, and I got that my eventual isomorphism with $\mathbb{Q}\setminus 0$ does these things:
(a) For $m\in \mathbb Z\setminus 0, [m]B\rightarrow m$ and $-1[m]B\rightarrow \frac{1}{m}$
(b) For $m\in \mathbb Z\setminus 0,k\in\mathbb{N}, k[m]B=[m]B$ and $ -k[m]B=-1[m]B$
(c) For $m,n\in \mathbb Z\setminus 0, ([m]+ -1[n])B \rightarrow \frac{m}{n}$
Now, I am fairly certain this is enough for me to show that the mapping with this property is an isomorphism, IF all the cosets in the factor group look like this. That's where I am having trouble.
First, I want to show that for any $m\neq n$, $[m]B\neq[n]B$, So I need to show there is no $b\in B$ such that $b=[m]-[n]$. I can definitely show that there are no $x,y$ such that $[m]-[n]=[xy]-[x]-[y]$, but $B$ contains all sorts of combinations of these generating elements, and I am unsure how to prove that there is no magic set of choices of these generating elements such that their sum comes out to $[m] - [n]$
I would suggest a different approach here. If one already guessed the answer for a universal construction like a Grothendieck group, it's often easier to check the universal property and not to construct an isomorphism to the explicit construction.
So, what one has to check here is that there is a map $i\colon\mathbb Z\setminus\{0\}\to \mathbb Q^\times$ such that for every multiplicative homomorphism $\varphi\colon\mathbb Z\setminus\{0\}\to A$ there is a unique homomorphims $\overline\varphi\colon \mathbb Q^\times\to A$ with $\overline\varphi\circ i = \varphi$.
Well, $i$ is pretty obviously just the inclusion map, and constructing $\overline\varphi$ given $\varphi$ is not difficult either: $\overline\varphi(m/n) := \varphi(m)\cdot\varphi(n)^{-1}$ has the desired properties:
Moreover, it is indeed unique with these properties (if $\varphi$ is given), because in this case one has to have $\overline\varphi(m) = \varphi(m)$ for $m\in \mathbb Z$, and $\overline\varphi(1/m) = \varphi(m)^{-1}$ because a homomorphism has to preserve inverses.