Steve Awodey の Category Theory を読む : Chapter 9

Steve Awodey の Category Theory を読むシリーズトップ

9.1 Preliminary definition
- Example 9.3
9.2 Hom-set definition
9.4 Order adjoints
- Example 9.12
9.5 Quantifiers as adjoints
9.6 RAPL
- Proposition 9.16
9.7 Locally cartesian closed categories
- Proposition 9.20
- Lemma 9.23
9.8 Adjoint functor theorem
- Theorem 9.29
参考書籍

9.1 Preliminary definition

Example 9.3

$F \colon {\bf{Pos}} \to \mathcal{C}{\bf{Pos}}$ を $F_{0}(P) = \left\{ U \subseteq P \ \middle| \ p' \leq p \in U \text{ implies } p' \in U \right\}$ で定義した時、 $F$ が forgetful functor $U$ の left adjoint となることを証明します。はじめに $F_{0}$ の定義が well-defined であることを証明します。

$Lemma$
$F_{0} \text{ is well-defined}.$

$Proof.$
任意の $P \in {\bf{Pos}}$ に対して $F_{0}(P)$ が cocomplete poset となることを示せばよい。 $F_{0}(P)$ に $\subseteq$ を順序として入れると poset になることは明らかであるから、 $F_{0}(P)$ が cocomplete になることを示す。
任意の index set $I$ に対して $\bigcup_{i \in I} U_{i} \in F_{0}(P)$ となることを示せばよい。任意の $a \in \bigcup_{i \in I} U_{i}$ と任意の $a' \leq a$ に対して $a \in \bigcup_{i \in I} U_{i}$ より $\exists i \in I,\ a \in U_{i}$ が成り立つ。 $U_{i} \in F_{0}(P)$ であるから、 $F_{0}(P)$ の定義より $a' \in U_{i}$ が成り立つ。よって $a' \in \bigcup_{i \in I} U_{i}$ が成り立つので $\bigcup_{i \in I} U_{i} \in F_{0}(P)$ が成り立つ。

$\square$

次に、任意の $f \colon P \to Q \in {\bf{Pos}}$ に対して $F_{1}(f)$ を定義する必要があります。その前に、任意の $p \in P$ に対して $p\!\downarrow$ を $p\!\downarrow \,= \left\{ p' \in P \ \middle|\ p' \leq p \right\}$ と定義するとき、次のことが成り立つことを証明します。

$Lemma$
$U \in F_{0}(P) \Rightarrow U = \bigcup_{p \in U} p\!\downarrow$

$Proof.$
任意の $a \in U$ に対して $a \in a\!\downarrow$ であるから $a \in \bigcup_{p \in U} p\!\downarrow$ が成り立つ。
逆に $a \in \bigcup_{p \in U} p\!\downarrow$ とすると $\exists p,\ a \in p\!\downarrow$ が成り立つので $a \leq p$ が成り立つ。すると $U \in F_{0}(P)$ であることから $a \in U$ が成り立つ。

$\square$

上の事実をもとに、任意の $f \colon P \to Q \in {\bf{Pos}}$ と任意の $U \in F_{0}(P)$ に対して $F_{1}(f)$ を $F_{1}(f)(U) = F_{1}(f)\left( \bigcup_{p \in U} p\!\downarrow \right) = \bigcup_{p \in U} f(p)\!\downarrow$ で定義します。このとき $F_{1}$ が well-defined であることを証明します。

$Lemma$
$F_{1} \text{ is well-defined}.$

$Proof.$
任意の $f \colon P \to Q$ と任意の $U \in F_{0}(P)$ に対して $F_{1}(f)(U) = \bigcup_{p \in U} f(p)\!\downarrow \in F_{0}(Q)$ となることを示せばよい。
任意の $q \in \bigcup_{p \in U} f(p)\!\downarrow$ と任意の $q' \leq q$ に対して、 $\exists p \in U,\ q \in f(p)\!\downarrow$ が成り立つから、 $q' \leq q$ なら $q' \in f(p)\!\downarrow$ となり $q' \in \bigcup_{p \in U} f(p)\!\downarrow$ が成り立つ。よって $\bigcup_{p \in U} f(p)\!\downarrow \in F_{0}(Q)$ である。

$\square$

このとき、証明は省略しますが $F \colon {\bf{Pos}} \to \mathcal{C}{\bf{Pos}}$ は functor の条件 (a), (b), (c) を満たすので functor となります。

次に $F$ が forgetful functor $U$ の left adjoint となることを証明します。はじめに、任意の $f \colon P \to U(\mathcal{C})$ に対して $\overline{f} \colon F(P) \to \mathcal{C}$ を任意の $U \in F(P)$ に対して $\overline{f}(U) = \bigvee_{p \in U} f(p)$ で定義します。このとき $\overline{f}$ が monotone かつ cocontinuous であることを証明します。

$Lemma$
$\overline{f} \text{ is monotone and cocontinuous}.$

$Proof.$

monotone であること

任意の $U' \subseteq U$ に対して $\bigvee_{p' \in U'} f(p') \leq \bigvee_{p \in U} f(p)$ を示せばよい。任意の $p' \in U'$ に対して $p' \in U$ であるから、 $f(p') \leq \bigvee_{p \in U} f(p)$ が成り立つので colimit の UMP より $\bigvee_{p' \in U'} f(p') \leq \bigvee_{p \in U} f(p)$ が成り立つ。

cocontinuous であること

任意の index set $I$ に対して $\overline{f}\left( \bigcup_{i \in I} U_{i} \right) = \bigvee_{i \in I} \overline{f}(U_{i})$ が成り立つことを示せばよい。定義よりこれは $\bigvee_{a \in \bigcup_{i \in I} U_{i}} f(a) = \bigvee_{i \in I} \bigvee_{a \in U_{i}} f(a)$ と同値である。
任意の $a \in \bigcup_{i \in I} U_{i}$ に対して $f(a) \leq \bigvee_{i \in I} \bigvee_{a \in U_{i}} f(a)$ が成り立つので、colimit の UMP より $\bigvee_{a \in \bigcup_{i \in I} U_{i}} f(a) \leq \bigvee_{i \in I} \bigvee_{a \in U_{i}} f(a)$ が成り立つ。
一方、任意の $i \in I$ と任意の $a \in U_{i}$ に対して $f(a) \leq \bigvee_{a \in \bigcup_{i \in I} U_{i}} f(a)$ が成り立つので、colimit の UMP より $\bigvee_{i \in I} \bigvee_{a \in U_{i}} f(a) \leq \bigvee_{a \in \bigcup_{i \in I} U_{i}} f(a)$ が成り立つ。

$\square$

次に $\eta \colon 1_{\bf{Pos}} \to U \circ F$ を $\eta_{P}(p) = p\!\downarrow$ で定義します。このとき $\eta$ が natural transformation になることを証明します。

$Lemma$
$\eta \text{ is a natural transformation}.$

$Proof.$
任意の $f \colon P \to Q$ に対して以下の diagram が可換になることを示せばよい。
f:id:hitotakuchan:20160902093405p:plain
これは任意の $p \in P$ に対して $f(p)\!\downarrow\, = \bigcup_{p' \in p\downarrow} f(p')\!\downarrow$ が成り立つことと同値である。

only if case

$q \in f(p)\!\downarrow$ とすると、 $q \leq f(p)$ が成り立つ。すると $p \in p\!\downarrow$ であるから $q \in \bigcup_{p' \in p\downarrow} f(p)\!\downarrow$ となる。

if case

$q \in \bigcup_{p \in p\downarrow} f(p)\!\downarrow$ とすると、ある $p' \in p\!\downarrow$ が存在して $q \in f(p')\!\downarrow$ が成り立つ。 $f$ は monotone であるから $q \leq f(p') \leq f(p)$ が成り立つので、 $q \in f(p)\!\downarrow$ が成り立つ。

$\square$

$Lemma$
$U(\overline{f}) \circ \eta_{P} = f$

$Proof.$
任意の $p \in P$ に対して $\bigvee_{p' \in p\downarrow} f(p') = f(p)$ となることを示せばよい。
$p \in p\!\downarrow$ より $f(p) \leq \bigvee_{p' \in p\downarrow} f(p')$ となることは明らかである。逆に、任意の $p' \in p\!\downarrow$ とすると $p' \leq p$ であり、 $f$ が monotone であるから $f(p') \leq f(p)$ が成り立つ。よって colimit の UMP より $\bigvee_{p' \in p\!\downarrow} f(p') \leq f(p)$ が成り立つ。

$\square$

最後に $\overline{f}$ の唯一性について証明する。

$Lemma$
$\forall g \colon F(P) \to \mathcal{C},\ U(g) \circ \eta_{P} = f \Rightarrow g = \overline{f}$

$Proof.$
任意の $U \in F(P)$ に対して $U = \bigcup_{p \in U} p\!\downarrow$ が成り立つことと $g$ が cocontinuous であることに注意すると、
\begin{align*}
g(U) &= g\left( \bigcup_{p \in U} p\!\downarrow \right) \\
&= \bigvee_{p \in U} g(p\!\downarrow) \\
&= \bigvee_{p \in U} f(p) \\
&= \overline{f}(U)
\end{align*}
が成り立つ。

$\square$

9.2 Hom-set definition

$\eta_{C} = \phi(1_{FC})$ で定義された $\eta \colon 1_{\bf{C}} \to U \circ F$ が natural transformation であることを証明します。

$Lemma$
$\eta \text{ is a natural transformation}.$

$Proof.$
任意の $h \colon C' \to C$ に対して以下の diagram が可換になることを示せばよい。
f:id:hitotakuchan:20160905110844p:plain
$\phi$ が natural であることから以下の diagram が可換になることに注意すると、
f:id:hitotakuchan:20160905112152p:plain
\begin{align*}
UF(h) \circ \eta_{C'} &= UF(h) \circ \phi_{C', FC'}(1_{FC'}) \\
&= \left( UF(h)_{\ast} \circ \phi_{C', FC'} \right)(1_{FC'}) \\
&= \left( \phi_{C', FC} \circ F(h)_{\ast} \right)(1_{FC'}) \\
&= \phi_{C', FC}\left( F(h) \right) \\
&= \phi_{C', FC} \left( 1_{FC} \circ F(h) \right) \\
&= \left( \phi_{C', FC} \circ F(h)^{\ast} \right)(1_{FC}) \\
&= \left( h^{\ast} \circ \phi_{C, FC} \right)(1_{FC}) \\
&= \phi_{C, FC}(1_{FC}) \circ h \\
&= \eta_{C} \circ h
\end{align*}
が成り立つ。

$\square$

9.4 Order adjoints

この節で出てくる例は、adjoint functor の domain も codomain も Preorder set を圏と見なしたものなので、任意の対象間には高々一つの写像しか存在しません。
よって同型射が natural になることは自明に成り立つのでその証明は省略されています。

Example 9.12

こちらの記事でも言及したのですが、ここの記述は正確ではありません。ただし位相空間に詳しくない方は飛ばして構いません。

書籍にあるように dual image function を $f_{\ast}(U) = \left\{ b \in B \,\middle|\, f^{-1}(b) \subseteq U \right\}$ と定義した場合、 $f_{\ast} \colon \mathcal{P}(A) \to \mathcal{P}(B)$ は確かに $f^{-1}$ の right adjoint になります。これは、 $f^{-1}(V) \subseteq U \Rightarrow V \subseteq f_{\ast}(U)$ かつ $V \subseteq f_{\ast}(U) \Rightarrow f^{-1}(V) \subseteq U$ が成り立つことを確認すればいいです。

問題はその次で、 $f^{-1}$ を開集合に制限して $f^{-1} \colon \mathcal{O}(B) \to \mathcal{O}(A)$ とした場合にも $f_{\ast}$ が $f^{-1}$ の right adjoint になるという記述です。というのも $U$ を任意の $A$ の開集合とした時に $f_{\ast}(U)$ は必ずしも $B$ の開集合とはならないからです。よって $f_{\ast}$ は $f^{-1}$ の right adjoint にはなり得ません。

そこで ${\it{Sheaves\ in\ Geometry\ and\ Logic}}$ という書籍を参照すると、そこでは dual image function を以下のように定義しています。
$f_{\ast}(U) = \bigcup \left\{ V \in \mathcal{O}(B) \,\middle|\, f^{-1}(V) \subseteq U \right\}$
この定義を用いると、任意の $A$ の開集合 $U$ に対して $f_{\ast}(U)$ は $B$ の開集合になり $f^{-1}$ の right adjoint になることが証明できます。一方で開集合に制限しない $f^{-1} \colon \mathcal{P}(B) \to \mathcal{P}(A)$ に対しては right adjoint になりません。

以上の二つの定義とその結果が、ここの記述ではごちゃ混ぜになっています。上で述べたことを是非自分で確認してみてください。

9.5 Quantifiers as adjoints

Figure 9.1 の説明がわかりにくいかもしれないので補足しておきます。ちなみに Figure 9.1 にある $\phi$ は $\psi$ の誤りです。
Figure 9.1 の左下を原点として、水平方向を $x$ 軸、垂直方向を $y$ 軸とします。また $x$ 上の任意の領域 $R$ に対して $\pi^{-1}(R)$ によって生成される長方形をそのまま $\pi^{-1}(R)$ と書くことにします。さらに斜線で塗られた領域を、領域 $\psi$ と呼ぶことにします。

$\frac{\exists y. \psi(x,y) \dashv \phi(x)}{\psi(x,y) \dashv \phi(x)}$

上から下に読む場合

$\phi(x)$ を満たす $x$ 軸上の領域 $R$ が $\exists y. \psi(x,y)$ を満たす $x$ 軸上の領域、つまり Figure 9.1 の $\exists \psi$ と書かれた領域を含むのであれば、 $\pi^{-1}(R)$ は領域 $\psi$ を含むと読みます。

下から上に読む場合

$\psi(x)$ を満たす $x$ 軸上の領域 $R$ に対して $\pi^{-1}(R)$ が領域 $\psi$ を含むのであれば、 $R$ は $\exists \psi$ を含むと読みます。

同様に
$\frac{\phi(x) \dashv \psi(x,y)}{\phi(x) \dashv \forall y. \psi(x,y)}$

上から下に読む場合

$\phi(x)$ を満たす $x$ 軸上の領域 $R$ に対して $\pi^{-1}(R)$ が領域 $\psi$ に含まれるならば、 $R$ は $\forall \psi$ に含まれると読みます。

下から上に読む場合

$\phi(x)$ を満たす $x$ 軸上の領域 $R$ が $\forall \psi$ に含まれるのであれば、 $\pi^{-1}(R)$ は領域 $\psi$ に含まれると読みます。

9.6 RAPL

Proposition 9.16

ここでは ${F_{!}}_{1}$ の定義と $F_{!}$ が functor になることの証明、 ${F^{\ast}}_{1}$ の定義と $F^{\ast}$ が functor になることの証明が省略されています。
さらに natural isomorphism であることを示すところで、isomorphism であることは示されていますが、natural であることの証明が省略されています。 $E$ に関して natural になることは Chapter 8 で確認しましたが $P$ に関して natural になることは確認していないので、ここで確認しておきます。

$Lemma$
$F_{!} \text{ is a functor}.$

$Proof.$

${F_{!}}_{1}$ の定義

任意の natural transformation $\theta \colon P \to Q$ に対して次の diagram を考える。
f:id:hitotakuchan:20160915131833p:plain
ここで任意の $h \colon (x', C') \to (x, C) \in \int\!P$ に対して $\phi_{P} \circ i_{h} = i_{(x', C')}$ 、 $\psi_{P} \circ i_{h} = i_{(x, C)} \circ F(h)$ である。
$i_{\left( \theta_{C}(x), C \right)}$ は $F \circ \pi(x,C) \overset{1_{FC}}{\to} F \circ \pi \left( \theta_{C}(x), C \right) \overset{i_{\left( \theta_{C}(x), C \right)}}{\to} \coprod_{\int\!Q} F \circ \pi(z,C)$ の合成である。
また $\theta$ が natural であるから $\left( Q(h) \circ \theta_{C} \right)(x) = \left( \theta_{C'} \circ P(h) \right)(x) = \theta_{C'}(x')$ が成り立つことから $h$ は $h \colon \left( \theta_{C'}(x'), C' \right) \to \left( \theta_{C}(x), C \right) \in \int\!Q$ となることに注意する。すると
\begin{align*}
c_{Q} \circ \left[ i_{\left( \theta_{C}(x), C \right)} \right] \circ \phi_{P} \circ i_{h} &= c_{Q} \circ i_{\left( \theta_{C'}(x'), C' \right)} \\
&= c_{Q} \circ \phi_{Q} \circ i_{h} \\
&= c_{Q} \circ \psi_{Q} \circ i_{h} \\
&= c_{Q} \circ i_{\left( \theta_{C}(x), C \right)} \circ F(h) \\
&= c_{Q} \circ \left[ i_{\left( \theta_{C}(x), C \right)} \right] \circ \psi_{P} \circ i_{h}
\end{align*}
が成り立つ。よって coproduct の UMP と colimit の UMP より diagram を可換にする写像 ${F_{!}}_{1}(\theta) \colon \varinjlim_{\int\!P} F \circ \pi(x,C) \to \varinjlim_{\int\!Q} F \circ \pi(z, C)$ がただ一つ存在する。これを ${F_{!}}_{1}(\theta)$ と定義する。

$F_{!}$ が functor であること

${F_{!}}_{1}(\theta \colon P \to Q) \colon {F_{!}}_{0}(P) \to {F_{!}}_{0}(Q)$ となるから $F_{!}$ は functor の条件 (a) を満たす。
${F_{!}}_{1}(1_{P})$ は上の diagram の $\theta$ を $1_{P}$ で置き換えると、colimit の UMP より ${F_{!}}_{1}(1_{P}) = 1_{{F_{!}}_{0}(P)}$ が成り立つことがわかる。よって $F_{!}$ は functor の条件 (b) を満たす。
${F_{!}}_{1}(\theta' \circ \theta)$ は $\left[ i_{\left( \theta'_{C}(z), C \right)} \right] \circ \left[ i_{\left( \theta_{C}(x), C \right)} \right] = \left[ i_{\left( (\theta' \circ \theta)_{C}(x), C \right)} \right]$ が成り立つので colimit の UMP より ${F_{!}}_{1}(\theta' \circ \theta) = {F_{!}}_{1}(\theta') \circ {F_{!}}_{1}(\theta)$ が成り立つ。よって $F_{!}$ は functor の条件 (c) を満たす。

$\square$

次に $F^{\ast}$ が functor であることを証明します。

$Lemma$
$F^{\ast} \text{ is a functor}.$

$Proof.$

任意の $E \in \mathcal{E}$ に対して $F^{\ast}(E)$ が functor であること

任意の $h \colon C' \to C$ に対して ${F^{\ast}(E)}_{1}(h) \colon \text{Hom}(FC, E) \to \text{Hom}(FC', E)$ を ${F^{\ast}(E)}_{1}(h) = F(h)^{\ast}$ で定義する。
${F^{\ast}(E)}_{1}(h \colon C' \to C) \colon {F^{\ast}(E)}_{0}(C) \to {F^{\ast}(E)}_{0}(C')$ となるので $F^{\ast}(E)$ は functor の条件 (a) を満たす。
${F^{\ast}(E)}_{1}(1_{C}) = F(1_{C})^{\ast} = 1_{F(C)}^{\ast} = 1_{\text{Hom}(FC, E)} = 1_{{F^{\ast}(E)}_{0}(C)}$ が成り立つので $F^{\ast}(E)$ は functor の条件 (b) を満たす。
${F^{\ast}(E)}_{1}(h \circ h') = F(h \circ h')^{\ast} = F(h')^{\ast} \circ F(h)^{\ast} = {F^{\ast}(E)}_{1}(h') \circ {F^{\ast}(E)}_{1}(h)$ が成り立つ。よって $F^{\ast}(E)$ は functor の条件 (c) を満たす。

$F^{\ast}$ が functor であること

任意の $f \colon E \to E'$ に対して ${F^{\ast}}_{1}(f)$ を任意の $C \in {\bf{C}}$ に対して ${F^{\ast}}_{1}(f)_{C} = f_{\ast}$ で定義する。
f:id:hitotakuchan:20160916132529p:plain
任意の $h \colon C' \to C$ と任意の $g \colon FC \to E$ に対して $\left( F^{\ast}(E')(h) \circ f_{\ast} \right)(g) = f \circ g \circ F(h) = \left( f_{\ast} \circ F^{\ast}(E)(h) \right)(g)$ が成り立つので、上の diagram は可換になる。よって ${F^{\ast}}_{1}(f)$ は natural transformation である。
このとき ${F^{\ast}}_{1}(f \colon E \to E') \colon {F^{\ast}}_{0}(E) \to {F^{\ast}}_{0}(E')$ が成り立つので $F^{\ast}$ は functor の条件 (a) を満たす。
${F^{\ast}}_{1}(1_{E}) = 1_{{F^{\ast}}_{0}(E)}$ は定義より明らか。よって $F^{\ast}$ は functor の条件 (b) を満たす。
${F^{\ast}}_{1}(f' \circ f)_{C} = (f' \circ f)_{\ast} = f'_{\ast} \circ f_{\ast} = {F^{\ast}}_{1}(f')_{C} \circ {F^{\ast}}_{1}(f)_{C} = \left( {F^{\ast}}_{1}(f') \circ {F^{\ast}}_{1}(f) \right)_{C}$ が成り立つので、 $F^{\ast}$ は functor の条件 (c) を満たす。

$\square$

最後に $\text{Hom}(P, F^{\ast}(E)) \cong \text{Hom}(F_{!}(P), E)$ が $P$ に関して natural であることを証明します。
$\text{Hom}(\varinjlim_{j \in J} yC_{j}, F^{\ast}(E)) \cong \varprojlim_{j \in J} \text{Hom}(yC_{j}, F^{\ast}(E))$ の場合は $\text{Hom}(\varinjlim_{j \in J} FC_{j}, E) \cong \varprojlim_{j \in J} \text{Hom}(FC_{j}, E)$ の場合と同様に示せるので、 $\eta \colon \text{Hom}(\varinjlim_{j \in J} FC_{j}, E) \cong \varprojlim_{j \in J} \text{Hom}(FC_{j}, E)$ が natural であることの証明のみを示します。それ以外の箇所は Chapter 8 で示した証明と同様に証明できるので省略します。 $\eta$ の定義は Chapter8 の 8.7 節の証明を参照してください。

$Lemma$
$\eta \text{ is a natural transformation}.$

$Proof.$
任意の $\theta \colon Q \to P$ について考える。 $\eta$ が natural であるためには以下の diagram が可換になることを示す必要がある。
f:id:hitotakuchan:20160916140213p:plain
しかし diagram の右の写像がどのような写像なのか明らかではない。そこで以下の diagram を考える。
f:id:hitotakuchan:20160916141840p:plain
ここで $\theta$ が natural であることから、任意の $h \colon (z', C') \to (z, C) in \int\!Q$ は $h \colon \left( \theta_{C'}(z'),C' \right) \to \left( \theta_{C}(z), C \right)$ となることに注意しておく。すると
\begin{align*}
\pi_{h} \circ \phi_{Q} \circ \left< \pi_{\left( \theta_{C}(z), C \right)}(-) \right>_{(z,C) \in \int\!Q} \circ e_{P} &= \pi_{(z',C')} \circ \left< \pi_{\left( \theta_{C}(z), C \right)}(-) \right>_{(z,C) \in \int\!Q} \circ e_{P} \\
&= \pi_{\left( \theta_{C'}(z'), C' \right)} \circ e_{P} \\
&= \pi_{h} \circ \phi_{P} \circ e_{P} \\
&= \pi_{h} \circ \psi_{P} \circ e_{P} \\
&= F(h)^{\ast} \circ \pi_{\left( \theta_{C}(z), C \right)} \circ e_{P} \\
&= F(h)^{\ast} \circ \pi_{(z,C)} \circ \left< \pi_{\left( \theta_{C}(z), C \right)}(-) \right>_{(z,C) \in \int\!Q} \circ e_{P} \\
&= \pi_{h} \circ \psi_{Q} \circ \left< \pi_{\left( \theta_{C}(z), C \right)}(-) \right>_{(z,C) \in \int\!Q} \circ e_{P}
\end{align*}
が成り立つので、product の UMP と limit の UMP より diagram を可換とする唯一つの $\overline{\theta}$ が存在する。

次に $\pi_{(z,C)} \circ e_{Q} \circ \overline{\theta} \circ \eta_{P} = \pi_{(z,C)} \circ e_{Q} \circ \eta_{Q} \circ F_{!}(\theta)^{\ast}$ を示す。すると product の UMP と $e_{Q}$ が monic であることから $\overline{\theta} \circ \eta_{P} = \eta_{Q} \circ F_{!}(\theta)^{\ast}$ が成り立つ。
任意の $f \colon \varinjlim_{(x,C)} F \circ \pi(x,C) \to E$ に対して
\begin{align*}
\left( \pi_{(z,C)} \circ e_{Q} \circ \overline{\theta} \circ \eta_{P} \right)(f) &= \left( \pi_{\left( \theta_{C}(z), C \right)} \circ e_{P} \circ \eta_{P} \right)(f) \\
&= \left( \pi_{\left( \theta_{C}(z), C \right)} \circ \left< - \circ i_{(x,C)} \right>_{(x,C) \in \int\!P} \circ c_{P}^{\ast} \right)(f) \\
&= f \circ c_{P} \circ i_{\left( \theta_{C}(z), C \right)} \\
&= f \circ c_{P} \circ \left[ i_{\left( \theta_{C}(z), C \right)} \right] \circ i_{(z,C)}
\end{align*}
が成り立つ。一方、
\begin{align*}
\left( \pi_{(z,C)} \circ e_{Q} \circ \eta_{Q} \circ F_{!}(\theta)^{\ast} \right)(f) &= \left( \pi_{(z,C)} \circ \left< - \circ i_{(z,C)} \right>_{(z,C) \in \int\!Q} \circ c_{Q}^{\ast} \circ F_{!}(\theta)^{\ast} \right)(f) \\
&= f \circ F_{!}(\theta) \circ c_{Q} \circ i_{(z,C)}
\end{align*}
が成り立つ。これは $F_{!}(\theta)$ の定義より等しい。よって $\eta$ は natural isomorphism である。

$\square$

最後にこのように定義した $F_{!}$ に対して $F_{!}(yC) \cong FC$ が成り立つことを証明します。

$Lemma$
$F_{!}(yC) \cong FC$

$Proof.$
$\int\!yC$ において $(1_{C},C)$ は terminal object になるので、任意の $(f, C') \in \int\!yC$ に対して $F(f) \colon F \circ \pi(f, C') \to F \circ \pi(1_{C},C)$ が存在する。このことに注意すると、任意の natural transformation $\phi \colon F \circ \pi \to \Delta E$ に対して次の左の diagram は可換となる。
f:id:hitotakuchan:20161005121121p:plain
また任意の $\psi \colon F \circ \pi(1_{C},C) \to E$ が存在して同様に diagram を可換にするとすると、上の右の diagram が可換になることより $\psi = \phi_{(1_{C}, C)}$ が成り立つ。
よって colimit の UMP より $F_{!}(yC) = \varinjlim_{(f,C) \in \int\!yC} F \circ \pi(f,C) \cong F \circ \pi(1_{C}, C) = FC$ が成り立つ。

$\square$

9.7 Locally cartesian closed categories

Proposition 9.20

はじめに、任意の $f \colon A \to B$ に対して $\sum_{f} \dashv f^{\ast} \dashv \prod_{f}$ が成り立つとき、 $\sum_{f} \circ\, f^{\ast} \dashv \prod_{f} \circ\, f^{\ast}$ が成り立つことを確認してください。
$\sum_{f} \dashv f^{\ast} \dashv \prod_{f}$ の二つの natural isomorphism を合成すればいいです。

次に $!_{A} \colon A \to \ast$ に対して $\sum_{!_{A}} \circ\, !_{A}^{\ast}$ が $A \times -$ となることは Proposition 5.14 で確認しました。すると $A \times -$ の right adjoint は $(-)^{A}$ に unique up to isomorphism で決まるので、 $B^{A} = (\prod_{!_{A}} \circ\, !_{A}^{\ast})(B)$ で定義すればよいことがわかります。

次に証明なしに出てくる "a slice of a slice is a slice" の確認をしておきます。

$Lemma$
$\text{a slice of a slice is a slice}.$

$Proof.$
f:id:hitotakuchan:20161021121200p:plain
任意の $X,Y \in \mathcal{E}$ と任意の $f \colon X \to Y$ について $\left( \mathcal{E} / Y \right) /\, f \cong \mathcal{E} / X$ となることを示す。
はじめに functor $\Phi \colon \left( \mathcal{E} / Y \right) /\, f \to \mathcal{E} / X$ を定義する。
任意の $a' \colon a \to f \in \left( \mathcal{E} / Y \right) /\, f$ に対して $\Phi_{0}(a') = a'$ と定義すると、 $a' \colon A \to X$ であるから $a \in \mathcal{E} / X$ となる。
また任意の $h \colon a' \to b' \in \left( \mathcal{E} / Y \right) /\, f$ に対して $\Phi_{1}(h) = h$ と定義すると、 $h$ は $b' \circ h = a'$ を満たすので $h \in \mathcal{E} / X$ となる。
このとき、 $\Phi_{1} \left(h \colon (a' \colon a \to f) \to (b' \colon b \to f) \right) = h \colon (a' \colon A \to X) \to (b' \colon B \to X) = h \colon \Phi_{0}(a') \to \Phi_{0}(b')$ が成り立つので、 $\Phi$ は functor の条件 (a) を満たす。
次に $\Phi_{1}(1_{a'}) = 1_{a'} = 1_{\Phi_{0}(a')}$ が成り立つので $\Phi$ は functor の条件 (b) を満たす。
最後に $\Phi_{1}(h' \circ h) = h' \circ h = \Phi_{1}(h') \circ \Phi_{1}(h)$ が成り立つので $\Phi$ は functor の条件 (c) を満たす。

次に functor $\Psi \colon \mathcal{E} / X \to \left( \mathcal{E} / Y \right) /\, f$ を定義する。
任意の $a' \colon A \to X \in \mathcal{E} / X$ に対して $\Psi_{0}$ を $\Psi_{0}(a') = a' \colon (f \circ a') \to f$ で定義する。明らかに $\Psi_{0}(a') \in \left( \mathcal{E} / Y \right) /\, f$ である。
また任意の $h \colon a' \to b' \in \mathcal{E} / X$ に対して $\Psi_{1}(h) = h$ と定義すると、 $h$ は $f \circ b' \circ h = f \circ a'$ を満たすので、 $\Psi_{1}(h) = h \colon \Psi_{0}(a') \to \Psi_{0}(b')$ となり functor の条件 (a) を満たす。
次に $\Psi_{1}(1_{a'}) = 1_{a'} = 1_{\Psi_{0}(a')}$ が成り立つので $\Psi$ は functor の条件 (b) を満たす。
最後に $\Psi_{1}(h' \circ h) = h' \circ h = \Psi_{1}(h') \circ \Psi_{1}(h)$ が成り立つので $\Psi$ は functor の条件 (c) を満たす。

以上のように定義した $\Phi$ 、 $\Psi$ に対して $\Psi \circ \Phi = 1$ かつ $\Phi \circ \Psi = 1$ が成り立つことは明らかであるから、 $\left( \mathcal{E} / Y \right) /\, f \cong \mathcal{E} / X$ が成り立つ。

$\square$

任意の $f \colon (a \colon A \to X) \to (b \colon B \to X) \in \mathcal{E}/X$ に対して composition functor $\sum_{f} \colon (\mathcal{E}/X)/\,a \to (\mathcal{E}/X)/\,b$ を考えます。
上の同型射を用いると $\sum_{f}' \colon \mathcal{E}/A \to \mathcal{E}/B$ が構成できます。 $\mathcal{E}$ が locally cartesian category なら、 $\sum_{f}'$ に対して right adjoint ${f^{\ast}}'$ 、 $\prod_{f}'$ が構成できます。よって再び同型射を用いることで $\sum_{f}$ に対して right adjoint を構成できるので $\mathcal{E}/X$ も locally cartesian category になります。

逆の $\text{2} \Rightarrow \text{1}$ の証明は exponential が突然出てきて難しいですね。 $\mathcal{F}$ を使った置き換えがなぜ必要なのかもよくわかりません。また1対1に対応するとは書かれていますが、それが $Y$ と $p$ に対して natural であることの証明は省略されています。

$Lemma$
$F^{\ast} \dashv \prod_{F}$

$Proof.$
f:id:hitotakuchan:20161021133911p:plain
任意の $F \colon A \to B$ の composition functor の right adjoint $F^{\ast}$ は pullback functor である。よって上の図のように任意の $Y \colon C \to B \in \mathcal{E}/B$ に対して $F^{\ast}(Y) = \pi_{2} \in \mathcal{E}/A$ となる。 $Y$ 、 $F$ は $\mathcal{E}$ における射であるから $Y \times F$ を $\mathcal{E}$ の object のように記述するのはおかしいが、 $\mathcal{E}/B$ においては $F \circ \pi_{2} = Y \circ \pi_{1}$ は確かに $Y \times F$ となるのでこのように記述している。このとき $\pi_{1}$ 、 $\pi_{2}$ は実際に $\mathcal{E}/B$ において projection function になっている。

以上の注意を元に、任意の $Y \colon C \to B$ と $p \colon X \to A$ に対して $\theta_{Y,p} \colon \text{Hom} \left( F^{\ast}(Y), p \right) \to \text{Hom}\left(Y, \prod_{F}(p) \right)$ を定義する。
任意の $l \colon F^{\ast}(Y) \to p$ に対して以下の diagram を考える。
f:id:hitotakuchan:20161021135558p:plain
$l$ は $l \colon F \circ \pi_{2} \to F \circ p \in \mathcal{E}/B$ と考えると $l \colon Y \times F \to F \circ p$ と見なせる。 $\mathcal{E}/B$ は cartesian closed であるので exponential の UMP より $\exists !\, \widetilde{l} \colon Y \to {F \circ p}^{F}$ が存在する。 $p$ が $p \colon F \circ p \to F \in \mathcal{E}/B$ と見なせることに注意して以下の pullback diagram in $\mathcal{E}/B$ を考える。
f:id:hitotakuchan:20161021141034p:plain
すると、 $\epsilon \circ (p^{F} \times 1) \circ (\widetilde{l} \times 1) = p \circ \epsilon \circ (\widetilde{l} \times 1) = p \circ l = \pi_{2}$ が成り立つ。一方、
$\epsilon \circ ( \widetilde{\pi_{2}} \times 1) \circ (! \times 1) = \pi_{2} \circ (! \times 1) = \pi_{2}$ が成り立つので exponential の UMP より $p^{F} \circ \widetilde{l} = \widetilde{\pi_{2}} \circ !$ が成り立つ。よって pullback の UMP より $\exists !\, m \colon Y \to \prod_{F}(p)$ が存在する。そこで $\theta_{Y,p}(l) = m$ で定義する。これは各 UMP により well-defined である。

次に $\theta^{-1}_{Y,p} \colon \text{Hom}\left(Y, \prod_{F}(p) \right) \to \text{Hom} \left( F^{\ast}(Y), p \right)$ を定義する。
任意の $m \colon Y \to \prod_{F}(p) \in \mathcal{E}/B$ に対して、上の diagram において $n \circ m$ を考える。すると exponential の UMP より $\exists !\, \overline{n \circ m} \colon Y \times F \to F \circ p$ が存在する。この $\overline{n \circ m}$ を $\overline{n \circ m} \colon \pi_{2} \to p \in \mathcal{E}/A$ とみなして、 $\theta^{-1}_{Y,p}(m) = \overline{n \circ m}$ で定義する。
f:id:hitotakuchan:20161021143437p:plain

$\theta^{-1}_{Y,p}$ は $\theta_{Y,p}$ の逆射になるので、 $\theta_{Y,p}$ は isomorphism である。次に natural であることを示す。

$\theta_{Y,p}$ が $Y$ に関して natural であること

任意の $h \colon Y' \to Y \in \mathcal{E}/B$ に対して Two-pullback Lemma より以下の diagram が可換になる。
f:id:hitotakuchan:20161024130748p:plain
すると $h'$ は $h' \in \mathcal{E}/A$ とみなすことができる。そこで次の左の diagram を考える。
f:id:hitotakuchan:20161024140733p:plain
任意の $l \colon F^{\ast}(Y) \to p$ に対して、 $(h^{\ast} \circ \theta_{Y,p})(l) = \theta_{Y,p}(l) \circ h$ が成り立つ。一方、 $(\theta_{Y',p} \circ h'^{\ast})(l) = \theta_{Y', p}(l \circ h')$ が成り立つ。
$\theta_{Y,p}(l) \circ h$ に対して $\theta$ の定義より、 $\epsilon \circ \left( n \circ \theta_{Y,p}(l) \circ h \times 1 \right) = \epsilon \circ \left( n \circ \theta_{Y,p}(l) \times 1 \right) \circ ( h \times 1) = l \circ (h \times 1)$ が成り立つ。同様に $\theta_{Y', p}(l \circ h')$ に対して $\epsilon \circ n \circ \theta_{Y', p}(l \circ h') = l \circ h'$ が成り立つ。
Two-pullback Lemma による diagram より上の右の diagram は可換になる。よって $h \times 1 = h'$ が成り立つので、exponential の UMP と pullback の UMP より $\theta_{Y,p}(l) \circ h = \theta_{Y', p}(l \circ h')$ が成り立つ。

$\theta_{Y,p}$ が $p$ に関して natural であること

任意の $h \colon (p \colon X \to A) \to (p' \colon X' \to A) \in \mathcal{E}/A$ に対して Two-pullback Lemma より以下の diagram が可換になる。
f:id:hitotakuchan:20161024140052p:plain
そこで次の diagram を考える。
f:id:hitotakuchan:20161024140723p:plain
任意の $l \colon F^{\ast}(Y) \to p$ に対して、 $( {h^{F}}'_{\ast} \circ \theta_{Y,p})(l) = {h^{F}}' \circ \theta_{Y,p}(l)$ が成り立つ。一方、 $(\theta_{Y,p'} \circ h_{\ast})(l) = \theta_{Y,p'}(h \circ l)$ が成り立つ。
上の Two-pullback Lemma による diagram と $\theta$ の定義より
\begin{align*}
\epsilon \circ \left( n' \circ {h^{F}}' \circ \theta_{Y,p}(l) \times 1 \right) &= \epsilon \circ \left( h^{F} \circ n \circ \theta_{Y,p}(l) \times 1 \right) \\
&= h \circ \epsilon \circ \left( n \circ \theta_{Y,p}(l) \times 1 \right) \\
&= h \circ l
\end{align*}
が成り立つ。一方、 $\epsilon \circ \left( n' \circ \theta_{Y, p'}(h \circ l) \times 1 \right) = h \circ l$ が成り立つ。よって exponential の UMP と pullback の UMP より ${h^{F}}' \circ \theta_{Y,p}(l) = \theta_{Y,p'}(h \circ l)$ が成り立つ。

以上より $\theta$ は natural isomorphism である。

$\square$

Lemma 9.23

ここでは $\Psi \colon {\bf{Sets}}^{(y/P)^{\text{op}}} \to {\bf{Sets}}^{{\bf{C}}^{\text{op}}}/P$ を定義し、 $1 \simeq \Psi \circ \Phi$ かつ $1 \simeq \Phi \circ \Psi$ を示す必要があります。
はじめに $\Psi$ を定義するために、任意の $G \in {\bf{Sets}}^{(y/P)^{\text{op}}}$ に対して functor $\coprod G \colon {\bf{C}}^{\text{op}} \to {\bf{Sets}}$ を定義します。

$Lemma$
$\coprod G \text{ is a functor}.$

$Proof.$
任意の $C \in {\bf{C}}$ に対して1つ目の成分が $C$ であるような $\int_{\bf{C}} P$ の object の集合を $\mathcal{L}_{C}$ と表す。このとき $(\coprod G)(C) = \coprod_{(C,x) \in \mathcal{L}_{C}} G( (C,x))$ で定義する。
次に任意の $f \colon C' \to C$ に対して、 $yf \colon yC' \to yC$ は任意の $x \colon yC \to P$ に対して $yf \colon x \circ yf \to x \in \int_{\bf{C}} P$ となる。すると $G(yf)$ は $G(yf) \colon G( (C,x)) \to G( (C', x \circ yf))$ となることに注意して、 $(\coprod G)(f) = \left[ i \circ G(yf) \right]_{(C,x) \in \mathcal{L}_{C}} \colon \coprod_{(C,x) \in \mathcal{L}_{C}} G( (C,x)) \to \coprod_{(C',x') \in \mathcal{L}_{C'}} G( (C',x'))$ で定義する。
このとき $\coprod G$ が functor の条件をみたすことは coproduct の UMP により明らかである。

$\square$

本当に $\coprod G$ が functor の条件を満たすか確認してください。
次にこの $\coprod G$ を用いて $\Psi(G)$ を $\Psi(G) \colon \coprod G \to P$ で定義する。このとき $\Psi$ が functor となることを示す。

$Lemma$
$\Psi \text{ is a functor}.$

$Proof.$
任意の $(C,x) \in \int_{\bf{C}} P$ と任意の $l \in G( (C,x))$ に対して $(\coprod G)(C)$ の要素を $( (C,x), l)$ で表すとすると、 $\Psi(G)$ を $(\Psi(G))_{C}( (C,x), l) = x_{C}(1_{C})$ で定義する。このとき $\Psi(G)$ が natural transformation であることを示す。
f:id:hitotakuchan:20161027142513p:plain
任意の $f \colon C' \to C \in {\bf{C}}$ と任意の $( (C,x), l) \in (\coprod G)(C)$ に対して $\left( P(f) \circ \Psi(G)_{C} \right)( (C,x), l) = P(f)(x_{C}(1_{C}))$ が成り立つ。一方米田の補題より
\begin{align*}
\left( \Psi(G)_{C'} \circ (\coprod G)(f) \right)( (C,x), l) &= \Psi(G)_{C'}\left( (C', x \circ yf), G(yf)(l) \right) \\
&= (x \circ yf)_{C}(1_{C}) \\
&= P(f)(x_{C}(1_{C}))
\end{align*}
が成り立つので、上の diagram は可換となり $\Psi(G) \in {\bf{Sets}}^{{\bf{C}}^{\text{op}}}/P$ となる。

次に、任意の $\theta \colon G \to G'$ に対して ${\Psi(\theta)}_{C} \colon (\coprod G)(C) \to (\coprod G')(C)$ を ${\Psi(\theta)}_{C} = \left[ i \circ \theta_{(C,x)} \right]_{(C,x) \in \mathcal{L}_{C}}$ で定義する。このとき $\Psi(\theta)$ が natural であることを示す。
f:id:hitotakuchan:20161028105839p:plain
任意の $f \colon C' \to C$ と任意の $( (C,x), l) \in (\coprod G)(C)$ に対して
$\left( (\coprod G')(f) \circ \Psi(\theta)_{C} \right) \left( ( (C,x), l) \right) = (\coprod G')(f)\left( ( (C, x), \theta_{(C,x)}(l)) \right) = \left( (C', x \circ yf), \left( G'(yf) \circ \theta_{(C,x)} \right)(l) \right)$
一方
$\left( \Psi(\theta)_{C'} \circ (\coprod G)(f) \right)\left( ( (C,x), l) \right) = \Psi(\theta)_{C'} \left( ( (C', x \circ yf), G(yf)(l) ) \right) = \left( ( C', x \circ yf), \left( \theta_{(C',x \circ yf)} \circ G(yf) \right)(l) \right)$
が成り立つ。これらは $\theta$ が natural であることより等しい。上の左の diagram は可換であるので $\Psi(\theta)$ は natural である。

また任意の $( ( C,x), l) \in (\coprod G)(C)$ に対して
$\left( \Psi(G')_{C} \circ \Psi(\theta)_{C} \right)\left( ( (C,x), l) \right) = x_{C}(1_{C}) = \Psi(G)_{C} \left( ( (C,x), l) \right)$
が成り立つので、 $\Psi(\theta) \colon \Psi(G) \to \Psi(G') \in {\bf{Sets}}^{{\bf{C}}^{\text{op}}}/P$ となる。

$\Psi$ が functor の条件をみたすことは coproduct の UMP 等により明らかである。

$\square$

$Lemma$
$1 \simeq \Psi \circ \Phi$

$Proof.$
natural isomorphism $\phi \colon 1 \to \Psi \circ \Phi$ を構成すればよい。
任意の $q \colon Q \to P$ と任意の $C \in {\bf{C}}$ に対して $(\Psi \circ \Phi)(q)(C) \colon \coprod_{(C,x) \in \mathcal{L}_{C}} \text{Hom}(x,q) \to PC$ となることに注意して、 ${\phi_{q}}_{C} \colon QC \to \coprod_{(C,x) \in \mathcal{L}_{C}} \text{Hom}(x,q)$ を任意の $l \in QC$ に対して ${\phi_{q}}_{C}(l) = ( ( C, q \circ \widetilde{l}), \widetilde{l})$ で定義する。ただし $\widetilde{l} \colon yC \to Q$ は米田の補題により一意に定まる $\widetilde{l}_{C}(1_{C}) = l$ を満たす natural transformation とする。

任意の $( (C, x), m) \in \coprod_{(C,x) \in \mathcal{L}_{C}} \text{Hom}(x,q)$ に対して ${\phi_{q}}_{C}^{-1}\left( ( (C,x), m) \right) = m_{C}(1_{C})$ で ${\phi_{q}}_{C}^{-1}$ を定義すれば、明らかに ${\phi_{q}}_{C}$ は isomorphism となる。

$\phi_{q}$ が $C$ に関して natural であることを示す。
任意の $f \colon C' \to C$ に対して以下の diagram を考える。
f:id:hitotakuchan:20161028121845p:plain
任意の $l \in QC$ に対して
$\left( \left( \coprod \Phi(q) \right)(f) \circ {\phi_{q}}_{C} \right)(l) = ( (C', q \circ \widetilde{l} \circ yf), \widetilde{l} \circ yf)$
が成り立つ。一方、 $\left( {\phi_{q}}_{C'} \circ Q(f) \right)(l) = ( (C', q \circ \widetilde{Q(f)(l)}), \widetilde{Q(f)(l)})$ が成り立つ。 $(\widetilde{l} \circ yf)_{C}(1_{C}) = Q(f)(l)$ が成り立つので両者は等しい。よって diagram は可換となる。

この $\phi_{q}$ に対して以下の diagram が可換になることは明らかなので、
f:id:hitotakuchan:20161028123226p:plain
$\phi_{q} \colon q \to (\Psi \circ \Phi)(q) \in {\bf{Sets}}^{{\bf{C}}^{\text{op}}}/P$ となる。

最後に任意の $\theta \colon q \to q'$ に対して以下の diagram を考える。
f:id:hitotakuchan:20161028124537p:plain
任意の $l \in QC$ に対して
$\left( (\Psi \circ \Phi)(\theta)_{C} \circ {\phi_{q}}_{C} \right)(l) = ( \Psi \circ \Phi)(\theta)_{C}( ( (C, q \circ \widetilde{l}), \widetilde{l}) ) = ( ( C, q \circ \widetilde{l}), \theta \circ \widetilde{l})$
が成り立つ。一方、 $( {\phi_{q'}}_{C} \circ \theta_{C})(l) = ( (C, q' \circ \widetilde{\theta_{C}(l)}), \widetilde{\theta_{C}(l)})$ が成り立つ。
ところが $(\theta \circ \widetilde{l})_{C}(1_{C}) = \theta_{C}(l)$ が成り立つので、両者は等しい。よって上の diagram は可換となる。

以上より $\phi$ は natural isomorphism である。

$\square$

$Lemma$
$1 \simeq \Phi \circ \Psi$

$Proof.$
natural isomorphism $\psi \colon 1 \to \Phi \circ \Psi$ を構成すればよい。
任意の $G \in {\bf{Sets}}^{(y/P)^{\text{op}}}$ と任意の $(C,x) \in y/P$ に対して ${\psi_{G}}_{(C,x)} \colon G(C,x) \to \text{Hom}\left( x, \Psi(G) \right)$ を次のように定義する。
任意の $l \in G(C,x)$ に対して $( (C,x), l)$ は $( (C,x), l) \in \coprod_{(C,x) \in \mathcal{L}_{C}} G(C,x)$ つまり $( (C,x), l) \in (\coprod G)(C)$ であるから米田の補題より一意に対応した $\widetilde{l} \colon yC \to \coprod G$ が得られる。

この $\widetilde{l}$ に対して以下の diagram を考える。
f:id:hitotakuchan:20161028144902p:plain
任意の $f \colon C' \to C$ に対して米田の補題と $\coprod G$ の定義より、
\begin{align*}
\left( \Psi(G)_{C'} \circ \widetilde{l}_{C'} \right)(f) &= \Psi(G)_{C'}( (C', x \circ yf), G(yf)(l)) \\
&= (x \circ yf)_{C'}(1_{C'}) \\
&= P(f) \left( x_{C'}(1_{C'}) \right) \\
&= x_{C'}(f)
\end{align*}
が成り立つので、上の diagram は可換になる。よって $\widetilde{l} \colon x \to \Psi(G)$ となるので ${\psi_{G}}_{(C,x)}(l) = \widetilde{l}$ と定義する。

次に $\psi_{G}$ が isomorphism であることを示す。
${\psi_{G}}_{(C,x)}^{-1} \colon \text{Hom}\left( x, \Psi(G) \right) \to G(C,x)$ を次のように定義する。
任意の $m \colon x \to \Psi(G)$ に対して、 $m$ は $m \colon yC \to \coprod G$ と見なせるので米田の補題より $( (C, x'), \overline{m})$ が一意に存在して $m_{C}(1_{C}) = ( ( C, x'), \overline{m})$ を満たす。このとき $m$ が $x = \Psi(G) \circ m$ をみたすことから $x = x'$ が成り立つ。よって $\overline{m} \in G(C,x)$ である。
そこで ${\psi_{G}}_{(C,x)}^{-1}(m) = \overline{m}$ と定義すると、米田の補題より ${\psi_{G}}_{(C,x)}$ の逆射となり ${\psi_{G}}_{(C,x)}$ は isomorphism となる。

次に $\psi_{G}$ が natural であることを示す。
任意の $yf \colon (C',x') \to (C,x)$ に対して次の diagram を考える。
f:id:hitotakuchan:20161028195553p:plain
任意の $l \in G( (C,x))$ に対して $(yf^{\ast} \circ {\psi_{G}}_{(C,x)})(l) = \widetilde{l} \circ yf$ が成り立つ。一方 $\left( {\psi_{G}}_{(C',x')} \circ G(yf) \right)(l) = \widetilde{G(yf)(l)}$ が成り立つ。
今、 $(\widetilde{l} \circ yf)_{C'}(1_{C'}) = \widetilde{l}(f) = ( ( C', x \circ yf), G(yf)(l))$ 、 $\widetilde{G(yf)(l)}_{C'}(1_{C'}) = ( (C', x'), G(yf)(l))$ が成り立ち両者は等しいので、米田の補題より diagram は可換となる。よって $\psi_{G}$ は natural である。

最後に $\psi$ が natural であることを示す。
任意の $\theta \colon G \to G'$ と任意の $(C,x)$ に対して次の diagram を考える。
f:id:hitotakuchan:20161028195604p:plain
任意の $l \in G( (C,x))$ に対して $\left( (\Phi \circ \Psi)(\theta)_{(C,x)} \circ {\psi_{G}}_{(C,x)} \right)(l) = (\Phi \circ \Psi)(\theta)_{(C,x)}(\widetilde{l}) = \Psi(\theta) \circ \widetilde{l}$ が成り立つ。一方 $\left( {\psi_{G'}}_{(C,x)} \circ \theta_{(C,x)} \right)(l) = \widetilde{\theta_{(C,x)}(l)}$ が成り立つ。
今 $\left( \Psi(\theta) \circ \widetilde{l} \right)_{C}(1_{C}) = \Psi(\theta)_{C}( ( (C,x), l)) = ( (C,x), \theta_{(C,x)}(l))$ 、 $\widetilde{\theta_{(C,x)}(l)}_{C}(1_{C}) = ( (C,x), \theta_{(C,x)}(l))$ が成り立つので、米田の補題より上の diagram は可換となる。

以上より $\psi$ は natural isomorphism である。

$\square$

9.8 Adjoint functor theorem

Theorem 9.29

書籍にある Solution set condition が微妙に間違ってます。書籍にある通り論理式で表現すると
$\forall X \in {\bf{X}},\ \exists I,\ \exists (S_{i})_{i \in I},\ \forall C \in {\bf{C}},\ \forall f \colon X \to UC,\ \exists i \in I,\ \exists \phi \colon X \to US_{i},\ \exists \overline{f} \colon S_{i} \to C,\ f = U(\overline{f}) \circ \phi$
となりますが、正しくは
$\forall X \in {\bf{X}},\ \exists I,\ \exists (S_{i})_{i \in I},\ \exists (\phi_{i} \colon X \to US_{i})_{i \in I},\ \forall C \in {\bf{C}},\ \forall f \colon X \to UC,\ \exists i \in I,\ \exists \overline{f} \colon S_{i} \to C,\ f = U(\overline{f}) \circ \phi_{i}$
となります。