読者です 読者をやめる 読者になる 読者になる

Steve Awodey の Category Theory を読む : Chapter 9

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

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}
となります。

こちらの条件でないと、Theorem 9.29 の証明の中で Lemma 9.30 を使用することができません。

参考書籍

Category Theory (Oxford Logic Guides)

Category Theory (Oxford Logic Guides)

圏論 原著第2版

圏論 原著第2版