Groupification and perfection of a commutative monoid The following definitions and proposition are taken from the paper The geometry of Frobenioids I by S. Mochizuki.
Let $\mathbb{N}_{\ge 1}$ be the set of positive integers.
$\mathbb{N}_{\ge 1}$ is a directed set by the order relation $a|b$.
Let $M$, $N$ be commutative monoids(the binary operations are written additively).
A map $f\colon M \rightarrow N$ is called a morphism if $f(x + y) = f(x) + f(y)$ for any $x, y$ and $f(0) = 0$.
For every $n \in \mathbb{N}_{\ge 1}$, the multiplication map $x \rightarrow nx$ on $M$ is a morphism.
$M$ is said to be torsion-free if $nx = 0$ implies $x = 0$ for every $n \in \mathbb{N}_{\ge 1}$.
Let $M^{gp}$ be the groupification of $M$, i.e. the grothendieck group of $M$.
Let $\psi\colon M \rightarrow M^{gp}$ be the canonical map.
If $\psi$ is injective, $M$ is said to be integral.
$M$ is said to be saturated if $na \in \psi(M)$ for some $n \in \mathbb{N}_{\ge 1}$ and $a \in M^{gp}$, then $a \in \psi(M)$.
$M$ is said to be perfect if the multiplication map $x \rightarrow nx$ is bijective for every $n \in \mathbb{N}_{\ge 1}$.
The perfection $M^{pf}$ of $M$ is defined as follows.
Let $M_a = M$ for every $a \in \mathbb{N}_{\ge 1}$.
if $a|b$, we define a morphism $f_{ba}\colon M_a \rightarrow M_b$ by $f_{ba}(x) = (b/a)x$.
Then $(M_a)_{a\in \mathbb{N}_{\ge 1}}$ and $(f_{ba})$ consitute a direct(or inductive) system.
We define $M^{pf} = colim_{a\in \mathbb{N}_{\ge 1}} M_a$.
There exists the canonical morphism $\phi\colon M = M_1 \rightarrow M^{pf}$.
My question:
How do we prove the following proposition?
Proposition
(1) $\phi\colon M \rightarrow M^{pf}$ is injective if $M$ is torsion-free, integral, and saturated.
(2) $M$ is perfect if and only if $\phi$ is an isomorhism.
Motivation
Recently(August, 2012), S. Mochizuki submitted a series of papers(Inter-universal Teichmuller Theory I,II,III,IV) which develops his new theory. As an application of his theory, he wrote a proof of ABC conjecture.
I think the validity of the proof has not yet been confirmed by other mathematicians.
However, considering his track record, I think it's worthwhile to read the papers.
He referred to The geometry of Frobenioids I for the notation and terminolgy concerning monoids and categories.
 A: (1) If $M \to M^{pf}$ is not injective,  there exist $x \neq y$ and $n\in \mathbb{N}_{\geq 1}$ such that $f_{n1}(x) = f_{n1}(y)$. (The fact that elements are equal in the colimit iff they are equal in some term requires some thought. It is not a general property; it follows here from the structure of the diagram defining the colimit.) So let us assume that $x,y\in M$ satisfy $nx = ny$.
Let $Z = [x] - [y]$ in $M^{gp}$. We have $nZ = [nx] - [ny] = 0$, which lies in the image $\psi(M)$, so saturation implies that $Z \in \psi(M)$. Say $Z=\psi(z)$ for $z\in M$. Since $Z$ satisfies $Z + [y] = [x]$, integrality implies that $z + y = x$. The element $z$ satisfies $\psi(nz)=nZ=0\in M^{gp}$, so integrality implies $nz = 0\in M$. Since $M$ is torsion-free this implies $z = 0$, so $z+y=x$ becomes $y = x$. This shows that $M\to M^{pf}$ is injective.
(2) Since $M^{pf}$ is perfect (an inverse to $x\mapsto nx$ is the map induced by sending $x\in M_a$ to $x\in M_{na}$), an isomorphism $M\to M^{pf}$ implies that $M$ is perfect. Conversely, if $M$ is perfect, we can change coordinates on $M_a$ by $x \mapsto \frac{1}{n}x$ (the inverse of $x\mapsto nx$, which is automatically a morphism). Now the direct system is constant and so $M\to M_1\to M^{pf}$ is an isomorphism.
A: Aha. What does this '$\mathrm{colim}$' means? $M^{pf} = \displaystyle(\coprod_{a\in\mathbb N} M_a)/\sim$, where $m_a$ and $m_b$ are identified ($m_a\sim m_b$), if $a|b$ and $m_b = (b/a)\cdot m_a$. 
Somehow, $M_a$ wants to represent the 'formal' $a$-fractions of $M$, regarding that any $m$ in $M_1$ is represented as $a\cdot m$ in $M_a$, so $m$ in $M_a$ wants to represent $\frac 1a\cdot m$.
Now pick $m,u$ such that $\phi(m)=\phi(u)$, denote $m_1$ and $u_1$ the (copy of) $m$ and $u$ in $M_1$, so it means $m_1=u_1$. 
Identity in $M^{pf}$ means that
$$\exists m_1\sim w_{a_1} \sim w_{a_2} \sim \dots \sim w_{a_k} \sim u_1 $$
i.e., $w_{a_1}=a_1\cdot m_1$,  next one is either $w_{a_2}=(a_2/a_1)\cdot w_{a_1} = a_2\cdot m_1$, or $w_{a_1} = (a_1/a_2)w_{a_2}$
...
