$m,n$ が同値であるとすると、$m=n\circ f$ を満たす $f:x\rightarrow y$ と $n=m\circ g$ を満たす $g:y\rightarrow x$ が存在する。よって $$ m\circ 1_x = m\circ g\circ f$$ が成立するので $m$ がモノ射である事より $g\circ f=1_x$。同様に $f\circ g=1_y$ であるので $f,g$ は同型射。

逆に、$m=n\circ f$を満たす $f$ が同型射であるとすると両辺に $f^{-1}$ を右から合成して $m\circ f^{-1}=n$ が成立する。 よって $m\leq n$ かつ $n\leq m$ であるので $m\sim n$ である。 $\square$

$g$ がモノ射であるとする。並行射 $\alpha,\beta: x\rightarrow p$ について $\bar{g}\circ \alpha = \bar{g}\circ\beta$ であるとすると $f\circ\bar{g}\circ\alpha=f\circ\bar{g}\circ\beta$ であるから図式の可換性より $g\circ\bar{f}\circ\alpha=g\circ\bar{f}\circ\beta$。よって $g$ はモノ射であるから $\bar{f}\circ\alpha=\bar{f}\circ\beta$である。従って、以下の可換図式を得るので引き戻しの普遍性より $\alpha=\beta$である。よって $\bar{g}$ はモノ射。$\square$

$$\xymatrix{ x \ar@<2pt>[rd]^{\alpha} \ar@<-2pt>[rd]_{\beta} \ar@/^1pc/[rrd]^{\bar{f}\circ\alpha = \bar{f}\circ\beta} \ar@/^-1pc/[rdd]_{\bar{g}\circ\alpha=\bar{g}\circ\beta} & & \\ & p \ar[r]^{\bar{f}} \ar[d]_{\bar{g}} & b \ar[d]^{g} \\ & a \ar[r]^{f} & c }$$

右の四角が引き戻しであるとし、以下の可換図式を考える。

$$\xymatrix{ x \ar@/^-1pc/[rdd]_-{f} \ar@/^2pc/[rrrd]^-{g} \ar@/^1pc/[rrd]^-{v} \ar[rd]^-{u} &&& \\ &\cdot \ar[r] \ar[d] & \cdot \ar[r] \ar[d] & \cdot \ar[d] \\ &\cdot \ar[r] & \cdot \ar[r] & \cdot }$$ まず、左の四角が引き戻しであるとして、外側の四角について考える。 図式の外側が可換となるような、$f,g$に対して右の四角に注目することと $v$の存在が一意であることがわかる。 すると $f,v$ について左に四角に注目することで、 $u$ の一意性もわかる。従って 外側の四角も引き戻しの図式である。

外側の四角が引き戻しであるとする。$f,v$ に対して $v$ の方に右の四角の上辺を合成すれば $g$ となり、これに外側の四角が引き戻しであることを使用すれば $u$ が一意であることがわかる。従って左側の四角も引き戻しの図式である。 $\square$

$\mathcal{C}$ を部分対象分類子 $\mathrm{true}:1\rightarrow\Omega$ を持つ圏であるとする。 $u$ の部分対象 $m:x\xhookrightarrow{}u$ に分類射 $\chi_x$ を対応させる対応 $\phi$ が全単射である事を示す。 まず、この対応が$m$の選び方に依らずwell-definedである事を示す。

モノ射 $m: x\xhookrightarrow{}u$ と $n: y\xhookrightarrow {}u$ が同値であるとする。すなわち同型射 $\alpha:x\rightarrow y$ が存在して $m = n\circ\alpha$ であるとする。 $$\xymatrix{ x \ar@{^{(}->}[rd]^-{m} \ar[rr]^{\alpha} && y \ar@{^{(}->}[ld]^-{n} \\ & u & }$$

部分対象分類子の定義より、 $m,n$ それぞれに対応する分類射 $\chi_m,\chi_n$ が存在するのでこれらが同一である事を示せば良い。 まず、 $u\xhookleftarrow{n}y\rightarrow 1$ が $u\xrightarrow{\chi_n}\Omega\xleftarrow{\mathrm{true}}1$ に対する引き戻しであるので、任意の $f: z\rightarrow u$ に対して、以下が可換となるような $v:z\rightarrow y$ が一意に存在する。 $$\xymatrix{ z \ar[rd]^v \ar@{.>}@/^1pc/[rrd] \ar@/^-1pc/[rdd]_{f}& & \\ & y \ar@{^{(}->}[d]^{n} \ar@{.>}[r] & 1 \ar@{^{(}->}[d]^{\mathrm{true}} \\ & u \ar[r]^{\chi_n} & \Omega }$$ これを $m=n\circ\alpha$ を用いて書き直すと以下の可換図式を得る。

$$\xymatrix{ z \ar[rd]^{\alpha^{-1}\circ v} \ar@{.>}@/^1pc/[rrd] \ar@/^-1pc/[rdd]_{f}& & \\ & x \ar@{^{(}->}[d]^{m} \ar@{.>}[r] & 1 \ar@{^{(}->}[d]^{\mathrm{true}} \\ & u \ar[r]^{\chi_n} & \Omega }$$ すると $m$ がモノであることにより、この図式が可換となる $z$ から $x$ への射は $\alpha^{-1}\circ v$ ただ一つとなるので、 $u\xhookleftarrow{m}x\rightarrow 1$ は $u\xrightarrow{\chi_n}\Omega\xleftarrow{\mathrm{true}}1$の引き戻しとなっている。すなわち $\chi_n$ は $m$ の分類射になっていて、分類射の一意性から $\chi_m = \chi_n$。

続いて $\phi:[m:x\xhookrightarrow{}u]\mapsto\chi_x$ が全単射である事を示す。まず、$\mathcal{C}$ は有限完備であるから任意の射 $\chi:u\rightarrow \Omega$ に対して引き戻し $\chi^*\mathrm{true}$ が存在する。 $\mathrm{true}:1\rightarrow\Omega$ はモノであるので、 $\chi^*\mathrm{true}$ もモノであるから、これを代表元とする部分対象が存在する。よって $\phi$ は全射。 また、 $\phi([m:x\xhookrightarrow{}u])=\phi([n:y\xhookrightarrow{}u]) = \chi$ であるとすると、引き戻しは同型を除いて一意であることから、同型射 $\alpha:x\rightarrow y$ が存在して $m=n\circ \alpha$ となること。すなわち $m\sim n$ であることが示される。よって $[m:x\xhookrightarrow{}u]=[n:y\xhookrightarrow{}u]$ であるから $\phi$ は単射。 $\square$

$\mathrm{Sub}$ が表現可能関手である事と、 $\mathrm{Sub}$に関して普遍的構成が存在することは同値であるから、部分対象分類子が存在する条件と普遍的構成が存在する条件が一致する事を示せば良い。

$\mathrm{Sub}$ の普遍的構成とは 命題2.60 より、ある対象 $\Omega\in\mathcal{C}$ とある要素 $[\mathrm{true}:t\hookrightarrow\Omega]\in\mathrm{Sub}(\Omega)$ が存在して、 任意の対象 $u\in\mathcal{C}$ と任意の要素 $[m:x\hookrightarrow u] \in \mathrm{Sub}(u)$ について $$ [m] = \mathrm{Sub}(\chi)([\mathrm{true}]) $$ となるような $\chi:u\rightarrow\Omega$ が唯一つ存在するという事である。

すなわち、$\mathrm{Sub}(\chi)$ とは $\chi$ に沿った引き戻しの事であったから、任意のモノ射 $m:x\xhookrightarrow{}u$ に対して、以下の図式が引き戻しとなるような $\chi$ が唯一つ存在する事が 普遍的構成が存在する事、そして $\mathrm{Sub}$ が表現可能関手である事と同値である。

$$\xymatrix{ x \ar@{^{(}->}[d]_{m} \ar[r] & t \ar[d]^{\mathrm{true}} \\ u \ar[r]^{\chi} & \Omega \\ }$$

あとは $t$ が終対象である事を示せば、部分対象分類子が存在する条件と一致するので証明が完了する。 ここで、任意の $x$ に対して$1_x$ がモノである事に注意すると、以下が引き戻しとなるような $\chi$ が一意に存在する。 $$\xymatrix{ x \ar[d]_{1_x} \ar[r] & t \ar[d]^{\mathrm{true}} \\ x \ar[r]^{\chi} & \Omega \\ }$$ 従って、この $\chi$ を $\mathrm{true}$ に沿って引き戻した射 $x\rightarrow t$ が存在する。よって、$\mathcal{C}(x, t)\neq \emptyset $ である。 そして、任意の $f:x\rightarrow t$ に対して、以下の可換図式を考えるとこれは引き戻しの図式となっている。 $$\xymatrix{ x \ar[d]_{1_x} \ar[r]^f & t \ar[d]^{\mathrm{true}} \\ x \ar[r]^{\mathrm{true}\circ f} & \Omega \\ }$$ なぜならば、以下が可換となるような任意の $y$ と $\alpha:y\rightarrow x, \beta: y\rightarrow t$ について

$$\xymatrix{ y \ar@/^1pc/[rrd]^{\beta} \ar@/^-1pc/[rdd]_{\alpha}& & \\ & & t \ar[d]^{\mathrm{true}} \\ & x \ar[r]^{\mathrm{true}\circ f} & \Omega \\ }$$ $\mathrm{true}\circ f\circ\alpha = \mathrm{true}\circ\beta$ であり $\mathrm{true}$ がモノであるから $f\circ\alpha = \beta$ となるので 以下も可換となる。またこの時 $y\rightarrow x$ は $\alpha $ に一意に定まるからである。

$$\xymatrix{ y \ar[rd]^{\alpha} \ar@/^1pc/[rrd]^{\beta} \ar@/^-1pc/[rdd]_{\alpha}& & \\ & x\ar[d]_{1_x} \ar[r]^f & t \ar[d]^{\mathrm{true}} \\ & x \ar[r]^{\mathrm{true}\circ f} & \Omega \\ }$$ 従って、最初の図式の $\mathrm{true}\circ f$ は $1_x$ に対して一意に定まるものであり $f$ によらない。よって、もし2つの射 $f,g:x\rightarrow t$ が存在したとすると $\mathrm{true}\circ f=\mathrm{true}\circ g$ であって、 $\mathrm{true}$ はモノであるから $f=g$。 以上より任意の $x$ に対して射 $x\rightarrow t$ は唯一つしか存在しないので $t$ は終対象である。 $\square$

全ての $a\in\mathcal{C}$ について $\varprojlim_{i\in\mathcal{J}} F(i)(a)$ が存在するとする。 $\mathcal{J}$ の射 $f: i\rightarrow j$ に対応する自然変換 $F(f):F(i)\rightarrow F(j)$ を $\mathcal{C}$ の射 $u: a\rightarrow b$ についてcomponent-wiseに描くと以下のようになり、これが全ての $f:i\rightarrow j$ と $u:a\rightarrow b$ について可換となる。

$$ \xymatrix{ F(i)(a) \ar[d]_{F(f)_a} \ar[r]^{F(i)(u)} & F(i)(b) \ar[d]^{F(f)_b} \\ F(j)(a) \ar[r]_{F(j)(u)} & F(j)(b) }$$

ここで $\varprojlim_{i\in\mathcal{J}} F(i)(a)$ が存在するので、下図のような極限錐がそれぞれ存在する。

$$ \xymatrix{ \varprojlim_{i\in\mathcal{J}}F(i)(a) \ar[rd] \ar@/_1pc/[rdd] &&& \varprojlim_{i\in\mathcal{J}}F(i)(b) \ar[ld] \ar@/^1pc/[ldd] \\ & F(i)(a) \ar[d]_{F(f)_a} \ar[r]^{F(i)(u)} & F(i)(b) \ar[d]^{F(f)_b}& \\ & F(j)(a) \ar[r]_{F(j)(u)} & F(j)(b) & }$$

ここで $\varprojlim_{i\in\mathcal{J}}F(i)(a)$ の錐の側面に各 $F(i)(u)$ (図の水平の射) を合成したものは $F(-)(b):\mathcal{J}\rightarrow\mathcal{D}$ への錐となるので、下図が可換となる射 $\bar{u}: \varprojlim_{i\in\mathcal{J}}F(i)(a)\rightarrow\varprojlim_{i\in\mathcal{J}}F(i)(b)$ が唯一つ存在。

$$ \xymatrix{ \varprojlim_{i\in\mathcal{J}}F(i)(a) \ar[rd] \ar@/_1pc/[rdd] \ar@{.>}[rrr]^{\bar{u}} &&& \varprojlim_{i\in\mathcal{J}}F(i)(b) \ar[ld] \ar@/^1pc/[ldd] \\ & F(i)(a) \ar[d]_{F(f)_a} \ar[r]^{F(i)(u)} & F(i)(b) \ar[d]^{F(f)_b}& \\ & F(j)(a) \ar[r]_{F(j)(u)} & F(j)(b) & }$$

そこで、$\mathcal{C}$ の各対象 $a$ に $\varprojlim_{i\in\mathcal{J}}F(i)(a)$ を、射 $u:a\rightarrow b$ に $\bar{u}$ を対応させる関係を考えるとこれは関手 $G: \mathcal{C}\rightarrow\mathcal{D}$ となる。これが $\varprojlim_{i\in\mathcal{J}}F(i)$ である事を示す。

そこで任意の $H:\mathcal{C}\rightarrow\mathcal{D}$ から $F$ への錐を考える。 $$ \xymatrix{ \varprojlim_{i\in\mathcal{J}}F(i)(a) \ar[rd] \ar@/_1pc/[rdd] \ar@{.>}[rrr]^{\bar{u}} &&& \varprojlim_{i\in\mathcal{J}}F(i)(b) \ar[ld] \ar@/^1pc/[ldd] \\ & F(i)(a) \ar[d]_{F(f)_a} \ar[r]^{F(i)(u)} & F(i)(b) \ar[d]^{F(f)_b}& \\ & F(j)(a) \ar[r]_{F(j)(u)} & F(j)(b) & \\ H(a) \ar[ru] \ar@/^1pc/[ruu] \ar[rrr]^{H(u)} &&& H(b) \ar[lu] \ar@/_1pc/[luu] }$$

この左側だけに注目すると $\varprojlim_{i\in\mathcal{J}}$ についての普遍性より以下を可換にする射 $H(a)\rightarrow\varprojlim_{i\in\mathcal{J}}F(i)(a)$ が一意に存在。右側も同様。

$$ \xymatrix{ \varprojlim_{i\in\mathcal{J}}F(i)(a) \ar[rd] \ar@/_1pc/[rdd] \ar@{.>}[rrr]^{\bar{u}} &&& \varprojlim_{i\in\mathcal{J}}F(i)(b) \ar[ld] \ar@/^1pc/[ldd] \\ & F(i)(a) \ar[d]_{F(f)_a} \ar[r]^{F(i)(u)} & F(i)(b) \ar[d]^{F(f)_b}& \\ & F(j)(a) \ar[r]_{F(j)(u)} & F(j)(b) & \\ H(a) \ar[ru] \ar@/^1pc/[ruu] \ar@{.>}[uuu] \ar[rrr]^{H(u)} &&& H(b) \ar[lu] \ar@/_1pc/[luu] \ar@{.>}[uuu] }$$

この射の族 $\{H(a)\rightarrow\varprojlim_{i\in\mathcal{J}}F(i)(a)\}$ は自然変換 $H\rightarrow G$ となり、これが一意であるので $G\simeq \varprojlim_{i\in\mathcal{J}}F(i)$ である。$\square$

$x: \mathcal{C}^{\mathrm{op}}\rightarrow\mathbf{Set}$ について自然な同型 $\hat{\mathcal{C}}(x\times p, q) \simeq\hat{\mathcal{C}}(x, q^p)$ の成立を示せば良い。 稠密性定理 より適当な図式 $d:\mathcal{J}\rightarrow\mathcal{C}$ が存在して $ x = \varinjlim_{i\in\mathcal{J}}\mathcal{Y}(d_i)$ と書けるので、これと 命題2.55 の双対版、米田の補題を用いて $$\begin{aligned} \hat{\mathcal{C}}(x, q^p) &\simeq \hat{\mathcal{C}}\left(\varinjlim_{i\in\mathcal{J}}\mathcal{Y}(d_i), q^p\right)\simeq\varprojlim_{i\in\mathcal{J}} \hat{\mathcal{C}}(\mathcal{Y}(d_i), q^p) \simeq \varprojlim_{i\in\mathcal{J}} q^p(d_i) = \varprojlim_{i\in\mathcal{J}}\hat{\mathcal{C}}(\mathcal{Y}(d_i)\times p, q) \\ &\simeq \hat{\mathcal{C}}\left(\varinjlim_{i\in\mathcal{J}}\mathcal{Y}(d_i)\times p, q\right) = \hat{\mathcal{C}}(x\times p, q) \end{aligned}$$ $\square$

まず $1_a: a\rightarrow a$ は(左簡約可能であるから)モノ射なので $[1_a] \in\mathrm{Sub}(a)$ である。そして、任意のモノ射 $m: x\hookrightarrow a$ に対して、以下が可換であるから $[m]\leq[1_a]$ である。 $\square$ $$\xymatrix{ & a & \\ x \ar[ru]^m \ar[rr]^m & & a \ar[lu]_{1_a} }$$

まず、$\hat{\mathcal{C}}$ の終対象 $1:\mathcal{C}^{\mathrm{op}}\rightarrow\mathbf{Set}$ は点別に計算できるので、任意の $c\in\mathcal{C}$ について $1(c)$ は $\mathbf{Set}$ の終対象である。そこで $$ 1(c) = \{\ast\}$$ とおく。

部分対象分類子 $\Omega$ が存在するならば、米田の補題より $$ \Omega(c) \simeq \hat{\mathcal{C}}(\mathcal{Y}(c),\Omega) $$ であり、 $\hat{\mathcal{C}}(\mathcal{Y}(c),\Omega) \simeq \mathrm{Sub}(\mathcal{Y}(c))$ であるから、$\Omega=\mathrm{Sub}(\mathcal{Y}(-))$ でなければならない事が分かる。

実際に $\Omega$ が部分対象分類子である事を示す為には、任意のモノ射 $m:A\hookrightarrow U$ に対して以下が引き戻しとなるような射 $\chi: U\rightarrow \Omega$ が唯一つ存在する事を示せば良い。 $$\xymatrix{ A \ar[r] \ar@{^{(}->}[d]_{m} & 1 \ar[d]^{\mathrm{true}} \\ U \ar[r]^{\chi} & \Omega }$$ すなわち、引き戻しは点別に計算できるので、各 $c\in\mathcal{C}$ について $$\xymatrix{ A(c) \ar[r] \ar@{^{(}->}[d]_{m_c} & \{\ast\} \ar[d]^{\mathrm{true}_c} & \\ U(c) \ar[r]^-{\chi_c} & \mathrm{Sub}(\mathcal{Y}(c)) & \text{in $\mathbf{Set}$} }$$ が引き戻しとなるような $\chi_c$ が一意である事を示せば良い。

$$ \chi_c\circ m_c = [1_{\mathcal{Y}(c)}] $$

交換則・吸収則は有限積・余積について一般に成り立つ性質であるので、吸収則と冪等則について示す。

$a\leq a$ と $a\leq a\vee b$ より $a\leq a\wedge(a\vee b)$ である。これと $a\wedge(a\vee b)\leq a$ より $a\wedge(a\vee b)=a$。もう一方も同様。

また、吸収則において $b=a\wedge a$とおけば $ a\wedge(a\vee(a\wedge a)) = a$ が成り立つので、この括弧内に吸収則を用いて $a\wedge a = a$。もう一方も同様。$\square$

$a\wedge b \leq a$ かつ $a\wedge b \leq b\vee c$ より $a\wedge b \leq a\wedge(b\vee c)$ である。 同様にして $a\wedge c \leq a\wedge(b\vee c)$ でもある。よって $$(a\wedge b)\vee(a\wedge c)\leq a\wedge(b\vee c) $$ である。

また$a\wedge b\leq (a\wedge b)\vee(a\wedge c)$ より $b\leq (a\Rightarrow (a\wedge b)\vee(a\wedge c))$ である。 同様に $c\leq (a\Rightarrow (a\wedge b)\vee(a\wedge c))$ であるので $$ b\vee c\leq (a\Rightarrow(a\wedge b)\vee(a\wedge c))$$ である。従って $$ a\wedge(b\vee c)\leq (a\wedge b)\vee(a\wedge c)$$ である。以上より $$a\wedge(b\vee c) = (a\wedge b)\vee(a\wedge c)$$ である。また、これを用いてもう一方も示される。

$$ \begin{align*} (a\vee b)\wedge(a\vee c) &= ((a\vee b)\wedge a)\vee((a\vee b)\wedge c) \\ &= a\vee((a\vee b)\wedge c) \\ &= a\vee((a\wedge c)\vee(b\wedge c)) \\ &= (a\vee(a\wedge c))\vee(b\wedge c) \\ &= a\vee(b\wedge c) \end{align*}$$ $\square$

まず、任意の $a\in\mathcal{H}$ について $a\wedge\neg a=\bot$ である事を示す。 $(a\Rightarrow\bot)\leq(a\Rightarrow \bot)$ より$a\wedge(a\Rightarrow \bot)\leq \bot$ すなわち $a\wedge\neg a\leq\bot$ である。一方 $\bot$ は始対象であるから $\bot\leq a\wedge \neg a$ である。従って $a\wedge \neg a=\bot$ である。

これを用いて $$(a\vee b)\wedge (\neg a\wedge \neg b) = (a\wedge \neg a \wedge \neg b)\vee (b\wedge \neg a \wedge \neg b)=(\bot\wedge b)\vee(\bot\wedge b) = \bot\vee\bot = \bot$$ より$ \neg a\wedge \neg b \leq (a\vee b\Rightarrow\bot)$ すなわち $\neg a\wedge\neg b\leq\neg(a\vee b)$ である。

また、 $a\leq a\vee b$ より $$ a\wedge\neg(a\vee b) \leq (a\vee b)\wedge\neg(a\vee b) = \bot$$ であるので $\neg(a\vee b)\leq (a\Rightarrow\bot)$ すなわち $\neg(a\vee b)\leq \neg a$ である。同様にして $\neg (a\vee b)\leq \neg b$ であるので $\neg(a\vee b)\leq \neg a\wedge\neg b$ である。

従って $$\neg a\wedge \neg b = \neg(a \vee b)$$ である。$\square$

\begin{align*} &\neg\neg a= \neg\neg a\wedge(\neg a\vee a)=(\neg\neg a\wedge \neg a)\vee (\neg\neg a\wedge a) =\bot\vee(\neg\neg a\wedge a) \\ &= (\neg a\wedge a)\vee(\neg\neg a\wedge a) = (\neg a\vee \neg\neg a)\wedge a= \top\wedge a = a \end{align*} $\square$

1つ目はハイティング代数である事から成立。2つ目は二重否定除去則を使って $$ \neg a\vee\neg b = \neg\neg(\neg a\vee\neg b) = \neg(\neg\neg a\wedge\neg\neg b) = \neg(a\wedge b)$$ $\square$

$a\wedge c\leq b$ であるならば、 $$ c\leq \neg a\vee c = (\neg a\vee a)\wedge (\neg a\vee c) = \neg a\vee(a\wedge c) \leq \neg a\vee b$$ であり、 $c\leq\neg a\vee b$ であるならば $$ a\wedge c \leq a\wedge (\neg a\vee b) = (a\wedge \neg a)\vee(a\wedge b) = a\wedge b \leq b$$ であるので、 $\neg a\vee b$ は指数対象 $b^a$ である。指数対象は同型を除いて一意であるので $$ (a\Rightarrow b) \simeq \neg a\vee b$$ であるが、半順序集合において同型な対象は一致するので $$ (a\Rightarrow b) = \neg a\vee b$$ である。$\square$