Universal Property of the Grothendieck Group (Group Completion) I am following the (german) construction of the Grothendieck group at https://de.wikipedia.org/wiki/Grothendieck-Gruppe. It is very precise and easy to follow until to the point of the universal property.
I understand that for a commutative semi group $(H,+)$ we define $$(x,y) \sim (x',y') : \iff \exists t \in H : x+y'+t=x'+y+t $$
which gives an equivalence relation on $H^2$. The equivalence class of said relation will be denoted as $G(H)$ the Grothendieck group of $H$ and with component wise addition it forms an abelian group. 
In the article they give $\varphi_H : H \to G(H)$ as $\varphi_H(x)=[x+x,x]$ and then they claim that for any Group $G$ and semi group morphism $\Psi: H \to G$ there exists exactly one groupmorphism  $\lambda: G(H) \to G$ such that $\lambda \circ \varphi_H = \Psi$  (Universal Property)
I can't deduce from that how $\lambda$ must be defined, of course it would be a group morphism, because $\Psi$ is, and furthermore it would be uniquely determined by $\Psi$, but how can I show that $\lambda$ is well defined? For this I suppose that I need more details about how $\lambda$ actually looks i.e. $$\lambda([x,y])=? $$
I thought about taking $\lambda([x,y])=\Psi(y)$ as a projection, but then realized that with such a definition I cannot deduce that $$G(\mathbb{N},+) \cong (\mathbb{Z},+) $$
 A: The idea behind constructing $\mathbb{Z}$ formally out of $\mathbb{N}$ is to create a set of "formal differences" $x-y$ encoded as ordered pairs $(x,y)$ modulo the relation $(x,y)\sim(x+z,y+z)$. Similarly we construct $\mathbb{Q}$ formally out of $\mathbb{Z}$ by making a set of "formal quotients $x/y$ encoded as ordered pairs $(x,y)$ with $y\ne 0$ modulo the relation $(xz,yz)$ for all $z\ne 0$. (Then we define addition.)
The same holds in general for Grothendieck constructions. In particular, given a semigroup $H$ (it is most natural to consider cancellative semigroups) the Groethendieck construction consists of formal differences once again encoded as ordered pairs $(x,y)$. Perhaps $(x,y)\sim (x',y')$ should mean that "$x-y=x'-y'$" (which doesn't make sense in a semigroup without all inverses) which we would write down as $x+y'=x'+y$, and I assume we add $+t$ to both sides for extra padding in case $H$ is not cancellative.
For the universal property, since $(x,y)$ is supposed to be $x-y$, we want $\Psi(x,y)$ to be $\Psi(x)-\Psi(y)$, so we can just define it that way and verify the universal property holds.
