シャープモノイド

$0+0=0$ なので $0\in P^\times$ である。$u,v\in P^\times$ とし、逆元をそれぞれ $u',v'$ とする。このとき
$$ (u+v)+(u'+v')=(u+u')+(v+v')=0 $$
なので $u+v\in P^\times$ である。また $u'$ 自身も $u$ を逆元に持つため $u'\in P^\times$。したがってすべての元が逆元を持ち、可換性は $P$ から継承される。

$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)$ であり、prop-sharp-monoid-units-group により $u+v\in P^\times$ なので推移律も成り立つ。
$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性を示す。integralな場合、
$$ \overline P^{\mathrm{gp}}\cong P^{\mathrm{gp}}/P^\times $$
である。$\overline x\in\overline P^{\mathrm{gp}}$ と正整数 $n$ に対し $n\overline x\in\overline P$ とする。代表元 $x\in P^{\mathrm{gp}}$ と $p\in P$ を選ぶと、ある $u\in P^\times$ により $nx=p+u$ である。右辺は $P$ に属するので、$P$ のsaturated性から $x\in P$。したがって $\overline x\in\overline P$ であり、$\overline P$ はsaturatedである。