寓圏と初等トポスの定義

関係合成の図式からそれぞれ直ちに読み取れる。

射のグラフの合成
恒等射のグラフと関係合成

単純計算で直ちに求まる。$x,y \colon X \to P$を任意に取り、$l \circ x = l \circ y$かつ$g_2 \circ r \circ x = g_2 \circ r \circ y$と仮定すると、
$f \circ l \circ x =  f \circ l \circ y$より、$g_1 \circ r \circ x = g_1 \circ r \circ y$が従う。$(T;g_1,g_2)$はjointly monic spanと仮定したから、$r \circ x = r \circ y$、引き戻しの普遍性より、$x = y$が従う。
よって$(P;l,g_2 \circ r)$はjointly monic familyの定義を満たす。

引き戻しはmonicを引き戻すことから、$t \colon 1 \to \Omega$を$\chi\colon A \to \Omega$で引き戻せばmonicを得られるので、
そのmonicが表示する$A$の部分対象を$\chi$と対応づければ良い。引き戻しのpasting lemmaより同型$\mathrm{Sub}(B) \simeq \mathcal{A}(B,\Omega)$の自然性が従う。

部分対象分類子による同型の自然性
なお、$A$の部分対象とは$A$に向かうmonicの同型類のことであったが、$(M;m)$と同型なmonic$(M';m')$、則ちある同型射$\theta \colon M \to M'$が存在して$m = m' \circ \theta$が成り立つような$(M';m')$を任意に取るとき、
$(M';m')$と$(M;m)$が同一の射$x \colon A \to \Omega$と対応することは次の図式から明らかである。

同型な1-tableと分類射
上の正方形図式が引き戻しであることは、向かい合う$\theta,1_A$がどちらも同型射であることから直ちに分かる。
引き戻しのpasting lemmaより、$m,m'$はいずれも$t$と$x$の引き戻しである。

仮定を満たすような$x,R$は、いずれも$1_{PB}$と自然同型で一対一になる。
$\ni_B$も$\in_B$も、自然同型$\mathcal{A}(B\times PB,\Omega) \simeq \mathrm{Sub}(B \times PB) \simeq \mathrm{Sub}(PB \times B) \simeq \mathrm{Rel}(\mathcal{A})(PB,B) \simeq \mathcal{A}(PB,PB)$で$1_{PB} \in \mathcal{A}(PB,PB)$と一対一に対応することから主張が成り立つ。

部分対象分類子とpower object及び$\in_B$の普遍性を組み合わせると次が成り立つ。

部分対象分類子とpower objectのタッグ
部分対象分類子の普遍性より、部分対象$[(T;\langle f_2,f_1 \rangle)] \in \mathrm{Sub}(B \times A)$は$f \colon B \times A \to \Omega$と一対一である。
同時にpower object及び$\in_B$の普遍性より、$f$と$\lambda f \colon A \to PB$は一対一であるから、したがって$\lambda f$は$B \times A$の部分対象$[(T;\langle f_2,f_1 \rangle)]$と一対一に対応している。
ここで$\langle f_2,f_1 \rangle,\langle u_2,u_1 \rangle$をjointly monic span$(T;f_2,f_1),(U;u_2,u_1)$と同一視することで、上の図式言語は次の図式言語を導くので、主張成立である。

普遍関係の普遍性と対応する射
composition-map-relで確認した通り、射のグラフを二項関係の前に合成する計算は引き戻しのみで事足りる。
$A$の左側には$1_A$が省略されており、この図式言語は関係合成$\ni_B \circ G_{\lambda f}$の計算に関する主張である。

対象$B$の普遍関係$\ni_B$の表示として$(U_B;u_1,u_2)$を選ぶものとする。このとき、$\ni_B \circ G_{\Lambda R}$の様子は次のように描かれる。

普遍関係と射のグラフの合成の恒等式
universalrel-universalityより、図中の$(C;l,u_2 \circ r)$は$R$の表示である。

univrel-counitより、$G_{1_A} = \ni_A \circ G_{\Lambda G_{1_A}} = \ni_A \circ G_{\{\cdot\}_A}$である。
いま正則圏で考えているから、二項関係の合成は結合律を満たす。よって次の式変形が成り立つ（第2の等号はunivrel-counitによる）。

$$ \begin{aligned} \ni_B \circ G_{\Lambda (R \circ \ni_A) \circ \{\cdot\}_A} &= \ni_B \circ G_{\Lambda (R \circ \ni_A)} \circ G_{\{\cdot\}_A} &&(G\text{は関手})\\ &= (R \circ \ni_A) \circ G_{\{\cdot\}_A}\\ &= R \circ G_{1_A}\\ &= R \end{aligned} $$

対応$f \mapsto \ni_B \circ G_f$は全単射であるから、$\Lambda(R \circ \ni_A)\circ \{\cdot\}_A = \Lambda R$が従う。

$\Lambda(R \circ \ni_A) \circ \eta_A = \Lambda R$で$R = G_{1_A}$の場合を考えることにより、$\Lambda(G_{1_A}\circ \ni_A)\circ \eta_A = 1_{PA}\circ \eta_A = \Lambda G_{1_A}$が成立。一方定義より$\{\cdot\}_A = \Lambda G_{1_A}$であったから、$\eta_A = \{\cdot\}_A$が従う。

定義より任意の$f \in \mathcal{B}(GA,B),g \in \mathcal{A}(A,HB)$に対して次の図式が成り立つ。

単位射と余単位射による随伴の同型
よって以下が従う。

$$ \Phi_{A,B}(f) = Hf \circ \eta_A,\quad \Phi_{A,B}^{-1}(g) = \varepsilon_B \circ Gg $$

$G,H$が仮定のように与えられたとする。このとき、自然同型$\mathcal{B}(G-,B)\simeq \mathcal{A}(-,HB)$を与える全単射の族を$(\Phi_{A,B} \colon \mathcal{B}(GA,B) \to \mathcal{A}(A,HB))_{A \in |\mathcal{A}|}$と書くことにして、
$\eta_A \overset{\mathrm{def}}{=} \Phi_{A,GA}(1_{GA}),\varepsilon_B \overset{\mathrm{def}}{=} \Phi_{HB,B}^{-1}(1_{HB})$と表記を定める。
そして任意の$f\colon B \to B'$に対し、$Hf \overset{\mathrm{def}}{=} \Phi_{HB,B'}(f \circ \varepsilon_B)$と定義する。

右随伴の射への作用の定義
まず、任意の$f \colon A \to HB$に対し、$\Phi_{A,B}^{-1}(f) = \varepsilon_B \circ Gf$が成り立つ：これは第一変数に関する自然同型$\mathcal{A}(-,HB)\simeq \mathcal{B}(G-,B)$より、

$$ \Phi_{A,B}(\varepsilon_B \circ Gf) = \Phi_{HB,B}(\varepsilon_B) \circ f = 1_{HB} \circ f = f $$

が成り立つこと、および$\Phi_{A,B}$は全単射であることから従う。よって特に$f = \eta_A$の場合を考えて、$\varepsilon_{GA} \circ G\eta_A = 1_{GA}$が成り立つ。

次に$(\varepsilon_B)_{B \in |\mathcal{B}|}$は、任意の$f \colon B \to B'$に対し、$\varepsilon_{B'}\circ GHf = f \circ \varepsilon_B$を満たす：
第一変数に関する自然同型より

$$ \Phi_{HB,B'}(\varepsilon_{B'}\circ GHf) = \Phi_{HB',B'}(\varepsilon_{B'}) \circ Hf = 1_{HB'}\circ Hf = Hf $$

であるから、先に定義した$Hf = \Phi_{HB,B'}(f \circ \varepsilon_B)$および$\Phi_{HB,B'}$が全単射であることから、$\varepsilon_{B'} \circ GHf= f \circ \varepsilon_B$でなければならない。
特に、$\varepsilon_{B'}\circ GHf = f \circ \varepsilon_B$を満たす$Hf$は$f$に対して一意に定まる。

$Hf$の定義が関手の公理を満たすことを確かめよう。
まず$H1_B = 1_{HB}$については、$H1_B = \Phi_{HB,B}(1_B \circ \varepsilon_B) = \Phi_{HB,B}(\varepsilon_B) = 1_{HB}$が$\varepsilon_B$の定義から従う。
次に$H(g \circ f) = Hg \circ Hf$については、任意の$f_1\colon B_1\to B_2,f_2 \colon B_2 \to B_3 \in \mathcal{B}$に対し、

$$ \begin{aligned} \Phi_{HB_1,B_3}^{-1}(Hf_2 \circ Hf_1) &= \varepsilon_{B_3} \circ G(Hf_2 \circ Hf_1)\\ &= \varepsilon_{B_3} \circ (GHf_2) \circ (GHf_1) \\ &= f_2 \circ \varepsilon_{B_2} \circ GHf_1 \\ &= f_2 \circ f_1 \circ \varepsilon_{B_1} \\ &= \Phi_{HB_1,B_3}^{-1}(H(f_2 \circ f_1)) \end{aligned} $$

であるから、$\Phi_{HB_1,B_3}$が全単射であることにより$H(f_2 \circ f_1) = Hf_2 \circ Hf_1$が一般に成立する。

合成射に関する関手の公理の成立
したがって$H$は関手の定義を満たすので、$A \in |\mathcal{A}|$を任意に固定したとき、任意の$f \colon B \to B',x \colon A \to HB$に対し

$$ \begin{aligned} \Phi_{A,B'}^{-1}(Hf \circ x) &= \varepsilon_{B'} \circ G(Hf \circ x)\\ &= \varepsilon_{B'} \circ GHf \circ Gx\\ &= f \circ \varepsilon_B \circ Gx\\ &= f \circ \Phi_{A,B}^{-1}(x) \end{aligned} $$

が成立する。これは任意に$A \in |\mathcal{A}|$を固定したときに自然同型$\mathcal{A}(A,H-) \simeq \mathcal{B}(GA,-)$が成り立つことを示しており、$G \dashv H$が帰結する。

$\mathcal{A}$は正則圏なので引き戻しと終対象を持つ。
$G \dashv P$の単位射を$\eta$、余単位射を$\varepsilon$で書くことにする。
また随伴の自然同型$\mathcal{A}(A,PB) \simeq \mathrm{Rel}(\mathcal{A})(GA,B) = \mathrm{Rel}(\mathcal{A})(A,B)$の全単射を次のように表記する。

$$ \begin{aligned} \mathcal{A}(A,PB) &\simeq \mathrm{Rel}(\mathcal{A})(A,B)\\ f &\leftrightarrow \overline f\\ \Lambda R &\leftrightarrow R \end{aligned} $$

naturality-conditionより、任意の$R \in \mathrm{Rel}(\mathcal{A})(A,B)$に対し$R = \varepsilon_B \circ G_{\Lambda R}$が成り立つ。
これは$\varepsilon_B$が普遍関係$\ni_B$の普遍性を満たすことを表している。実際、二項関係$\varepsilon_B$の表示を$(E_B;e_1,e_2)$と書くとき、次が成り立つ。

余単位射は普遍関係の特徴を持つ
このとき$\varepsilon_1 \in \mathrm{Rel}(\mathcal{A})(P1,1)$の表示$(E_1;e_1,e_2)$は、部分対象分類子$P1,e_1$を与える。
実際、任意の対象$A$に対し、任意に$R \in \mathrm{Rel}(\mathcal{A})(A,1)$を取り、その表示を$(M;m,p_M)$とする。これはjointly monic spanであるから、任意の$x,y$に対し$m \circ x = m \circ y$かつ$p_M \circ x = p_M \circ y$ならば$x = y$であるが、
終対象の普遍性より、この主張は$m \circ x = m \circ y$ならば$x = y$と同値である。よって$m$はmonicでなければならない。
これにより、$e_1 \colon E_1 \to P1$はmonicである。

終対象上の普遍関係になる
そして特に、任意の$A \in |\mathcal{A}|$に対して$[(A;1_A,p_A)] \in \mathrm{Rel}(\mathcal{A})(A,1)$を考えたとき、射$A \to E_1$は一意に存在する：
存在性は普遍関係の普遍性から従う。一意性について、次の二つの図式はいずれも引き戻し図式である。

$f \circ p = g \circ q$で$g$がmonic、$p$が同型ならば引き戻し図式
よって普遍関係$\ni_1$の普遍性より、任意の$x,y \colon A \to E_1$に対し、$e_1 \circ x = e_1 \circ y$でなければならない。
$e_1$はmonicであったから、$x=y$。よって$E_1$は終対象の定義を満たす。

部分対象分類子の存在より、$\mathrm{Rel}(\mathcal{A})(GA,B) = \mathrm{Rel}(\mathcal{A})(A,B) \simeq \mathrm{Sub}_{\mathcal{A}}(A \times B) \simeq \mathrm{Sub}_{\mathcal{A}}(B \times A) \simeq \mathcal{A}(B \times A,P1) \simeq \mathcal{A}(A,PB)$が従い、
この自然同型で$\ni_B(=\varepsilon_B)$と対応する射$x \colon B \times PB \to \Omega(\Omega = P1)$が$\in_B$の定義を満たすことは、universalrel-universalityの証明の逆を辿れば分かる。
以上より、$\mathcal{A}$は初等トポスの定義を満たす。

対象$A$にpower object$PA$を割り当てる操作を、対象のクラス間写像$P \colon |\mathcal{A}| \to |\mathcal{A}|$と見做す。
初等トポスの定義より、対象$B$を固定したとき、任意の$A \in |\mathcal{A}|$に対し$\mathrm{Rel}(\mathcal{A})(GA,B) \simeq \mathcal{A}(A,PB)$が自然に成り立つことから、map-becomes-functorより$P$は共変関手へと自然に拡張できる：任意の$R \in \mathrm{Rel}(\mathcal{A})(GA,B) = \mathrm{Rel}(\mathcal{A})(A,B)$に対し、$PR \overset{\mathrm{def}}{=} \Lambda(R \circ \ni_A)$と定めることで、$G\dashv P$となる関手を得る。
singleton-unit、univrel-counitより、singleton mapの族と普遍関係の族がそれぞれ単位射、余単位射となることが分かる。