シャープモノイド

1 ⇒ 2：$a+b=0$ なら $a$ と $b$ は単元なので、シャープ性から $a=b=0$ である。
2 ⇒ 3：$a\neq0$、$b\neq0$ で $a+b=0$ とすると 2 に反する。
3 ⇒ 4：$\chi(0)=0$ である。$\chi(a+b)=\chi(a)+\chi(b)$ を確かめる。$a=0$ または $b=0$ なら両辺は $\chi$ の値そのものである。$a,b$ がともに $0$ でなければ、3 から $a+b\neq0$ なので左辺は $1$、右辺は $1+1=1$ である。
4 ⇒ 1：$u$ を単元、$u+v=0$ とすると $\chi(u)+\chi(v)=\chi(0)=0$ である。二元モノイドで和が $0$ になるのは両方が $0$ のときだけなので $\chi(u)=0$、すなわち $u=0$ である。$\square$

$p=p+0$ なので反射律が成り立つ。$q=p+u$ で $u\in P^\times$ なら、$u$ の逆元 $-u\in P^\times$ を用いて $p=q+(-u)$ となるため対称律が成り立つ。$q=p+u$、$r=q+v$ なら $r=p+(u+v)$ であり、単元どうしの和は単元なので（可換モノイド の記事の命題「逆元の一意性と単元群」）、推移律も成り立つ。
$p'\sim p$、$q'\sim q$ なら、ある $u,v\in P^\times$ により $p'=p+u$、$q'=q+v$ と書ける。したがって
$$ p'+q'=p+q+(u+v)\sim p+q $$
なので和は代表元によらない。結合律・交換律・零元は $P$ から継承される。

$\overline p\in\overline P$ が単元であるとする。ある $q\in P$ に対して
$$ \overline p+\overline q=\overline0 $$
なので $p+q\sim0$ である。よってある $u\in P^\times$ により $p+q=u$ と書ける。$u$ の逆元を $u'$ とすると
$$ p+(q+u')=0 $$
だから $p\in P^\times$ である。したがって $\overline p=\overline0$。ゆえに $\overline P$ の単元は $\overline0$ だけである。

$u\in P^\times$ なら、逆元 $v$ に対し $f(u)+f(v)=0$ なので $f(u)$ は $Q$ の単元である。$Q$ はシャープだから $f(u)=0$。したがって $q=p+u$ なら
$$ f(q)=f(p)+f(u)=f(p) $$
であり、$f$ は同値類上で一定である。そこで $\overline f(\overline p):=f(p)$ と定めればwell-definedなモノイド準同型になり、$f=\overline f\circ\pi$ を満たす。$\pi$ は全射なので、この等式を満たす $\overline f$ の値は各 $\overline p$ 上で $f(p)$ に強制され、一意である。

$\overline p+\overline r=\overline q+\overline r$ とする。すると、ある $u\in P^\times$ により
$$ p+r+u=q+r $$
となる。$P$ の消去律で $r$ を消して $p+u=q$ を得るので $\overline p=\overline q$。よって $\overline P$ はintegralである。$P$ が有限集合で生成されるなら、その生成元の像が $\overline P$ を生成するためfine性も保たれる。
saturated性を示す。$P$ をintegralとし、$\pi\colon P\to\overline P$ を群化に延ばした準同型を $\psi\colon P^{\mathrm{gp}}\to\overline P^{\mathrm{gp}}$、$a-b\mapsto\overline a-\overline b$ とする。$\overline P^{\mathrm{gp}}$ の元はすべて $\overline a-\overline b$ の形なので $\psi$ は全射であり、核は $P^\times$ である。

$k$ についての帰納法で示す。$k=1$ なら明らかである。$k\geq2$ とし、$a=g_1+(g_2+\cdots+g_k)$ と分ける。$a$ は既約なので $g_1=0$ または $g_2+\cdots+g_k=0$ である。後者なら prop-sharp-monoid-equivalent の 2 を繰り返し使って $g_2=\cdots=g_k=0$ となり、$a=g_1$ である。前者なら $a=g_2+\cdots+g_k$ に帰納法の仮定を使う。
$G$ を生成系とすると、$a$ は $G$ の元の有限和であり（$a\neq0$ なので空和ではない）、前半から $a$ は $G$ の元に等しい。$\square$

$P$ を生成する有限集合 $\{g_1,\ldots,g_n\}$ をとる。lem-sharp-monoid-atom-in-generators により既約元はこの中にあるので有限個である。
$0$ でない $p$ が既約元の和で書けないと仮定して矛盾を導く。$p$ は既約でないので、$0$ でない $a,b$ で $p=a+b$ と書け、$a,b$ の少なくとも一方は既約元の和で書けない（両方が書ければ $p$ も書ける）。それを $p_1$、他方を $c_1$ とすると $p=p_1+c_1$、$c_1\neq0$ である。$p_1$ に同じ議論を繰り返すと、既約元の和で書けない元の列 $p_0:=p,\ p_1,\ p_2,\ldots$ と $0$ でない元 $c_1,c_2,\ldots$ で
$$ p_k=p_{k+1}+c_{k+1}\qquad(k\geq0) $$
となるものが得られる。
$\mathbb N^n$ から $P$ への準同型 $\varphi(m_1,\ldots,m_n):=m_1g_1+\cdots+m_ng_n$ は全射なので、$\varphi(x_k)=p_k$ となる $x_k\in\mathbb N^n$ がとれる。Dicksonの補題（下に証明を畳んだ）により、$i< j$ で $x_i\leq x_j$（成分ごと）となるものがある。$d:=x_j-x_i\in\mathbb N^n$ とおくと $p_j=p_i+\varphi(d)$ である。一方、漸化式を $i$ から $j$ までつなげると $p_i=p_j+(c_{i+1}+\cdots+c_j)$ なので
$$ p_i+0=p_i+\bigl(\varphi(d)+c_{i+1}+\cdots+c_j\bigr) $$
であり、消去律から $\varphi(d)+c_{i+1}+\cdots+c_j=0$ を得る。prop-sharp-monoid-equivalent の 2 により各項は $0$ で、特に $c_j=0$ となって矛盾する。
以上で、既約元の全体 $\mathcal A$ が $P$ を生成することが分かった。$\mathcal A$ はどの生成系にも含まれるので、$\mathcal A$ に含まれる生成系は $\mathcal A$ 自身に限り、$\mathcal A$ はただ一つの極小な生成系である。$\square$