Steve Awodey の Category Theory を読む : Chapter 6

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

6.2 Cartesian closed categories

Example 6.5

 \omegaCPO はプログラミング言語の Denotational Semantics で使用される重要な代数構造なのでここでは詳しく証明しておきます。

 Q^{P} is an  \omegaCPO

任意の  f_{0} \leq f_{1} \leq \cdots に対して、 \varinjlim_{i} f_{i} を任意の  p \in P に対して  \left( \varinjlim_{i} f_{i} \right)(p) = \varinjlim_{i} f_{i}(p) で定義します。この  \varinjlim_{i} f_{i} が monotone かつ  \omega-continuous であることを証明します。

 Lemma
\[ \varinjlim_{i} f_{i} \text{ is monotone}. \] Proof.
任意の  p, p' \in P と任意の  i \in N に対して、 f_{i} が monotone であることより、 f_{i}(p) \leq f_{i}(p') \leq \varinjlim_{i} f_{i}(p') が成り立つ。よって colimit の UMP より  \left( \varinjlim_{i} f_{i} \right)(p) = \varinjlim_{i} f_{i}(p) \leq \varinjlim_{i} f_{i}(p') = \left( \varinjlim_{i} f_{i} \right)(p') が成り立つ。

 \square

次に  \varinjlim_{i} f_{i} \omega-continuous であることを証明するのですが、その前に準備として任意の  f_{0} \leq f_{1} \leq \cdots と任意の  p_{0} \leq p_{1} \leq \cdots に関して次の事柄を証明しておきます。

 Lemma
\[ \exists \varinjlim_{j} f_{0}(p_{j}) \leq \varinjlim_{j} f_{1}(p_{j}) \leq \cdots ,\, \exists \varinjlim_{i} \left( \varinjlim_{j} f_{i}(p_{j}) \right) ,\, \forall i,\, \varinjlim_{j} f_{i}(p_{j}) \leq \varinjlim_{i} \left( \varinjlim_{j} f_{i}(p_{j}) \right) \] Proof.
任意の  i に対して  \varinjlim_{j} f_{i}(p_{j}) \leq \varinjlim_{j} f_{i+1}(p_{j}) を示せば、 \varinjlim_{j} f_{0}(p_{j}) \leq \varinjlim_{j} f_{1}(p_{j}) \leq \cdots \omega chain となる。すると  Q \omegaCPO であることから残りの性質は明らかである。
 f_{i}, f_{i+1} \omega-continuous であることから、 f_{i}(\varinjlim_{j} p_{j}) \leq f_{i+1}(\varinjlim_{j} p_{j}) を示せばよいが、  f_{i} \leq f_{i+1} であるからこれは成り立つ。

 \square

 Lemma
\[ \exists \varinjlim_{i} f_{i}(p_{0}) \leq \varinjlim_{i} f_{i}(p_{1}) \leq \cdots ,\, \exists \varinjlim_{j} \left( \varinjlim_{i} f_{i}(p_{j}) \right) ,\, \forall j,\, \varinjlim_{i} f_{i}(p_{j}) \leq \varinjlim_{j} \left( \varinjlim_{i} f_{i}(p_{j}) \right) \] Proof.
任意の  j に対して  \varinjlim_{i} f_{i}(p_{j}) \leq \varinjlim_{i} f_{i}(p_{j+1}) を示せば、 \varinjlim_{i} f_{i}(p_{0}) \leq \varinjlim_{i} f_{i}(p_{1}) \leq \cdots \omega chain となる。すると  Q \omegaCPO であることから残りの性質は明らかである。
 \varinjlim_{i} f_{i} が monotone であることより  \varinjlim_{i} f_{i}(p_{j}) = \left( \varinjlim_{i} f_{i} \right) (p_{j}) \leq \left( \varinjlim_{i} f_{i} \right) (p_{j+1}) = \varinjlim_{i} f_{i}(p_{j+1}) が成り立つ。

 \square

 Lemma
\[ \varinjlim_{i} \left( \varinjlim_{j} f_{i}(p_{j}) \right) = \varinjlim_{j} \left( \varinjlim_{i} f_{i}(p_{j}) \right) \] Proof.

  •  \varinjlim_{i} \left( \varinjlim_{j} f_{i}(p_{j}) \right) \leq \varinjlim_{j} \left( \varinjlim_{i} f_{i}(p_{j}) \right)

任意の  i と任意の  j に対して  f_{i} \leq \varinjlim_{i} f_{i} と上で示したことより  f_{i}(p_{j}) \leq \varinjlim_{i} f_{i}(p_{j}) \leq \varinjlim_{j} \left( \varinjlim_{i} f_{i}(p_{j}) \right) が成り立つ。
すると  \omega chain  f_{i}(p_{0}) \leq f_{i}(p_{1}) \leq \cdots に対する colimit の UMP より  \varinjlim_{j} f_{i}(p_{j}) \leq \varinjlim_{j} \left( \varinjlim_{i} f_{i}(p_{j}) \right) が成り立つ。
さらに上で示した  \omega chain  \varinjlim_{j} f_{0}(p_{j}) \leq \varinjlim_{j} f_{1}(p_{j}) \leq \cdots に対する colimit の UMP より  \varinjlim_{i} \left( \varinjlim_{j} f_{i}(p_{j}) \right) \leq \varinjlim_{j} \left( \varinjlim_{i} f_{i}(p_{j}) \right) が成り立つ。

  •  \varinjlim_{j} \left( \varinjlim_{i} f_{i}(p_{j}) \right) \leq \varinjlim_{i} \left( \varinjlim_{j} f_{i}(p_{j}) \right)

任意の  j と任意の  i に対して  f_{i} が monotone であることと上で示したことより  f_{i}(p_{j}) \leq \varinjlim_{j} f_{i}(p_{j}) \leq \varinjlim_{i} \left( \varinjlim_{j} f_{i}(p_{j}) \right) が成り立つ。
すると  \omega chain  f_{0}(p_{j}) \leq f_{1}(p_{j}) \leq \cdots に対する colimit の UMP より  \varinjlim_{i} f_{i}(p_{j}) \leq \varinjlim_{i} \left( \varinjlim_{j} f_{i}(p_{j}) \right) が成り立つ。
さらに上で示した  \omega chain  \varinjlim_{i} f_{i}(p_{0}) \leq \varinjlim_{i} f_{i}(p_{1}) \leq \cdots に対する colimit の UMP より  \varinjlim_{j} \left( \varinjlim_{i} f_{i}(p_{j}) \right) \leq \varinjlim_{i} \left( \varinjlim_{j} f_{i}(p_{j}) \right) が成り立つ。

 \square

以上の準備を元に  \varinjlim_{i} f_{i} \omega-continuous であることを証明します。

 Lemma
\[ \varinjlim_{i} f_{i} \text{ is } \omega \text{-continuous}. \] Proof.
\[
\begin{align*}
\left( \varinjlim_{i} f_{i} \right) (\varinjlim_{j} p_{j}) &\underset{\text{def}}{=} \varinjlim_{i} f_{i} \left( \varinjlim_{j} p_{j} \right) \\
&\underset{f_{i} \text{ is continuous}}{=} \varinjlim_{i} \left( \varinjlim_{j} f_{i}(p_{j}) \right) \\
&= \varinjlim_{j} \left( \varinjlim_{i} f_{i}(p_{j}) \right) \\
&\underset{\text{def}}{=} \varinjlim_{j} \left( \left( \varinjlim_{i} f_{i} \right) (p_{j}) \right)
\end{align*}
\]

 \square

 \epsilon is  \omega-continuous

まず任意の  \omega chain  (f_{0}, p_{0}) \leq (f_{1}, p_{1}) \leq \cdots に関して以下の事柄を証明します。

 Lemma
\[ \varinjlim_{i} (f_{i}, p_{i}) = \left( \varinjlim_{j} f_{j}, \varinjlim_{k} p_{k} \right) \] Proof.
任意の  i に対して  f_{i} \leq \varinjlim_{j} f_{j} かつ  p_{i} \leq \varinjlim_{k} p_{k} が成り立つ。よって  (f_{i}, p_{i}) \leq \left( \varinjlim_{j} f_{j}, \varinjlim_{k} p_{k} \right) が成り立つ。
任意の  (x,y) と任意の  i に対して  (f_{i}, p_{i}) \leq (x, y) が成り立つとする。すると  \omega chain  f_{0} \leq f_{1} \leq \cdots に対する colimit の UMP より  \varinjlim_{j} f_{j} \leq x が成り立つ。同様に  \varinjlim_{k} p_{k} \leq y が成り立つ。よって  \left( \varinjlim_{j} f_{j}, \varinjlim_{k} p_{k} \right) \leq (x, y) が成り立つので、 \varinjlim_{i} (f_{i}, p_{i}) = \left( \varinjlim_{j} f_{j}, \varinjlim_{k} p_{k} \right) である。

 \square

 Lemma
\[ \epsilon \left( \varinjlim_{i} (f_{i}, p_{i}) \right) = \varinjlim_{i} \epsilon( f_{i}, p_{i}) \] Proof.
上で証明したことと  \epsilon の定義より、証明するべきことは  \left( \varinjlim_{j} f_{j} \right) \left( \varinjlim_{k} p_{k} \right) = \varinjlim_{i} f_{i}(p_{i}) である。

  •  \varinjlim_{i} f_{i}(p_{i}) \leq \left( \varinjlim_{j} f_{j} \right) \left( \varinjlim_{k} p_{k} \right)

任意の  i に対して、
\[
\begin{align*}
f_{i}(p_{i}) &\underset{f_{i} \text{ is monotone}}{\leq} f_{i} \left( \varinjlim_{k} p_{k} \right) \\
&\leq \varinjlim_{j} \left( f_{j} \left( \varinjlim_{k} p_{k} \right) \right) \\
&\underset{\text{def}}{=} \left( \varinjlim_{j} f_{j} \right) \left( \varinjlim_{k} p_{k} \right)
\end{align*}
\]
 \omega chain  f_{0}(p_{0}) \leq f_{1}(p_{1}) \leq \cdots に対する colimit の UMP より  \varinjlim_{i} f_{i}(p_{i}) \leq \left( \varinjlim_{j} f_{j} \right) \left( \varinjlim_{k} p_{k} \right) が成り立つ。

  •  \left( \varinjlim_{j} f_{j} \right) \left( \varinjlim_{k} p_{k} \right) \leq \varinjlim_{i} f_{i}(p_{i})

任意の  j と任意の  k に対して、 f_{j} (p_{k}) \leq \varinjlim_{i} f_{i}(p_{i}) を示す。
 j \leq k のとき、
 f_{j}(p_{k}) \leq f_{k}(p_{k}) \leq \varinjlim_{i} f_{i}(p_{i}) が成り立つ。
 k \leq j のとき、
 f_{j}(p_{k}) \leq f_{j}(p_{j}) \leq \varinjlim_{i} f_{i}(p_{i}) が成り立つ。
よって  \omega chain  f_{j}(p_{0}) \leq f_{j}(p_{1}) \leq \cdots に対する colimit の UMP より  \varinjlim_{k} f_{j}(p_{k}) \leq \varinjlim_{i} f_{i}(p_{i}) が成り立つ。これは  f_{j} が continuous であることより  f_{j} \left( \varinjlim_{k} p_{k} \right) \leq \varinjlim_{i} f_{i}(p_{i}) と同値である。
すると  \omega chain  f_{0} \left( \varinjlim_{k} p_{k} \right) \leq f_{1} \left( \varinjlim_{k} p_{k} \right) \leq \cdots に対する colimit の UMP より  \varinjlim_{j} f_{j} \left( \varinjlim_{k} p_{k} \right) \leq \varinjlim_{i} f_{i}(p_{i}) が成り立つ。定義より  \left( \varinjlim_{j} f_{j} \right) \left( \varinjlim_{k} p_{k} \right) \leq \varinjlim_{i} f_{i}(p_{i}) である。

 \square

 \tilde{f} is  \omega-continuous if  f is so

任意の  \omega chain  x_{0} \leq x_{1} \leq \cdots に対して、以下の事柄を証明します。

 Lemma
\[ \tilde{f} \left( \varinjlim_{i} x_{i} \right) = \varinjlim_{i} \tilde{f}(x_{i}) \] Proof.
任意の  p \in P に対して  \tilde{f} \left( \varinjlim_{i} x_{i} \right)(p) = \left( \varinjlim_{i} \tilde{f}(x_{i}) \right)(p) を示せばよいが、これは  \tilde{f} の定義より  f \left( \varinjlim_{i} x_{i}, p \right) = \varinjlim_{i} f(x_{i}, p) と同値である。
 \omega chain  (x_{0},p) \leq (x_{1}, p) \leq \cdots に対して、上で証明したことより  \varinjlim_{i} (x_{i}, p) = \left( \varinjlim_{i} x_{i}, p \right) が成り立つ。
よって  f \omega-continuous であることより  f \left( \varinjlim_{i} x_{i}, p \right) = f \left( \varinjlim_{i} (x_{i}, p) \right) = \varinjlim_{i} f(x_{i}, p) が成り立つ。

 \square

Example 6.6

初めにテキストの通りに定義された  \epsilon が graph homomorphism であることを証明します。

 Lemma
\[ \epsilon \colon H^{G} \times G \to H \text{ is a graph homomorphism}. \] Proof.
f:id:hitotakuchan:20160516120426p:plain
上の diagram が可換になることを示せばよい。
任意の  \theta \colon \phi \to \psi \in {H^{G}}_{e} と任意の  e \in G_{e} に対して、 (s \circ \epsilon_{e})(\theta, e) = s(\theta(e)) = \phi(s(e)) が成り立つ。さらに、 (\epsilon_{v} \circ s)(\theta, e) = \epsilon_{v}(s(\theta), s(e)) = \epsilon_{v}(\phi, s(e)) = \phi(s(e)) が成り立つ。よって  s \circ \epsilon_{e} = \epsilon_{v} \circ s が成り立つ。
同様に  t \circ \epsilon_{e} = \epsilon_{v} \circ t が成り立つ。

 \square

次に  H^{G} が exponential object in  \bf{Graphs} であることを証明します。

 Lemma
\[ H^{G} \text{ is an exponential object in } \bf{Graphs}. \] Proof.
初めに、任意の  f \colon F \times G \to H に対してテキストの通りに定義される  \tilde{f} \colon F \to H^{G} が graph homomorphism となることを証明する。それには次の diagram が可換となることを示せばよい。
f:id:hitotakuchan:20160516122209p:plain
これは任意の  c \colon a \to b \in F_{e} に対して、 \tilde{f}_{e}(c) \colon \tilde{f}_{v}(a) \to \tilde{f}_{v}(b) \colon \in H^{G}_{e} となることと同値であり、さらに  H^{G} の定義より以下の diagram が可換になることと同値である。
f:id:hitotakuchan:20160516123743p:plain
任意の  e \in G_{e} に対して、 \left( s \circ \tilde{f}_{e}(c) \right)(e) = s(f_{e}(c,e)) = f_{v}(s(c,e)) = f_{v}(a,s(e)) = \left( \tilde{f}_{v}(a) \right)(s(e)) = \left( \tilde{f}_{v}(a) \circ s \right)(e) が成り立つ。同様に  \left( t \circ \tilde{f}_{e}(c) \right)(e) = \left( \tilde{f}_{v}(b) \circ t \right)(e) が成り立つ。よって  \tilde{f} は graph homomorphism である。
この  \tilde{f} に対して  \epsilon \circ \left( \tilde{f} \times 1 \right) = f が成り立つことは明らかである。
次に任意の  f' \colon F \to H^{G} \epsilon \circ (f' \times 1) = f を満たすとする。
任意の  a \in F_{v} と任意の  u \in G_{v} に対して  f'_{v}(a)(u) = (\epsilon \circ (f' \times 1))(a, u) = f_{v}(a, u) = \tilde{f}_{v}(a)(u) が成り立つ。
また、任意の  c \in F_{e} と任意の  e \in G_{e} に対して  f'_{e}(c)(e) = (\epsilon \circ (f' \times 1))(c, e) = f_{e}(c, e) = \tilde{f}_{e}(c)(e) が成り立つ。よって  f' = \tilde{f} が成り立つ。

 \square

6.3 Heyting Algebras

Definition 6.10

lattice に関しては complete であることと cocomplete であることが同値であることを証明します。
さらっと書かれていますが、その前の poset  P がすべての set-indexed meets を持てば、圏論的な意味で complete となるということの証明はできますか?
set-indexed meets を持つというのは、任意の集合  I を離散圏とみなした場合に任意の diagram  D \colon I \to P が limit を持つことと言い換えられます。一方で、圏論的な意味で complete になるためには任意の diagram に対して limit を持たないといけません。
poset を圏とみなした場合、任意の対象間にはただ一つしか arrow が存在しないということから証明できます。

 Lemma
\[ \text{A lattice } (L, \leq) \text{ is complete} \Rightarrow (L, \leq) \text{ is cocomplete}. \] Proof.
任意の  I-index 集合  \left\{ a_{i} \in L \right\} に対して、集合  I' I' = \left\{ b \in L \, \middle| \, \forall i \in I,\, a_{i} \leq b \right\} で定義する。すると、 L が complete であることから、 I' の limit  \bigwedge_{b \in I'} b が存在する。これが  \left\{ a_{i} \right\} の colimit  \bigvee_{i \in I} a_{i} であることを示す。
任意の  i \in I と任意の  b \in I' に対して  I' の定義より  a_{i} \leq b が成り立つ。すると、 \bigwedge_{b \in I'} b I' の limit であるから limit の UMP より  a_{i} \leq \bigwedge_{b \in I'} b が成り立つ。
次に、任意の  x \in L が任意の  i \in I に対して  a_{i} \leq x を満たすとする。すると  I' の定義より  x \in I' が成り立つ。よって limit の定義より  \bigwedge_{b \in I'} b \leq x が成り立つ。
poset の anti-symmetricity より  \bigvee_{i \in I} a_{i} = \bigwedge_{b \in I'} b である。

 \square

6.7 Variable sets

6.7.1 において証明が省略されている事柄は exercise 15 としてまとめられているので、そちらの証明をしておきます。

Exercise 15(a)

 Lemma
\[ {\bf{2}}^{I} \text{ is a Heyting algebra}. \] Proof.

  •  {\bf{2}}^{I} has a terminal object  1

 1 を任意の  i \in I に対して  1(i) = \top で定義すると、任意の  f \in {\bf{2}}^{I} と任意の  i \in I に対して、 f(i) \leq 1(i) が成り立つので  f \leq 1 が成り立つ。

  •  {\bf{2}}^{I} has products

任意の  f,g \in {\bf{2}}^{I} に対して  f \land g を任意の  i \in I に対して  (f \land g)(i) = f(i) \land g(i) で定義する。すると  f \land g \leq f かつ  f \land g \leq g が成り立つ。このとき  f \land g が product となることを示す。
任意の  h \in {\bf{2}}^{I} に対して  h \leq f かつ  h \leq g が成り立つとすると、任意の  i \in I に対して  h(i) \leq f(i) \land g(i) が成り立つので、 h \leq f \land g が成り立つ。 {\bf{2}}^{I} が poset であることより、これはただ一つに決まる。

  •  {\bf{2}}^{I} has an initial object  0

 0 を任意の  i \in I に対して  0(i) = \bot で定義すれば、任意の  f \in {\bf{2}}^{I} に対して  0 \leq f が成り立つ。

  •  {\bf{2}}^{I} has coproducts

任意の  f,g \in {\bf{2}}^{I} に対して  f \lor g を任意の  i \in I に対して  (f \lor g)(i) = f(i) \lor g(i) で定義する。すると product の場合と同様に  f \lor g は coproduct となる。

  •  {\bf{2}}^{I} has exponentials

任意の  f, g \in {\bf{2}}^{I} に対して  f \Rightarrow g を任意の  i \in I に対して  (f \Rightarrow g)(i) = \top \iff \forall j \leq i,\, f(j) \leq g(j) で定義する。

 f \land g \leq h ならば  f \leq g \Rightarrow h が成り立つこと。
任意の  i \in I に対して  f(i) \leq (g \Rightarrow h)(i) を示せばよい。 f(i) = \bot ならば  f(i) \leq (g \Rightarrow h)(i) は明らかである。 f(i) = \top とすると、任意の  j \geq i に対して  g(j) \leq h(j) を示せばよいが、仮定より  f(j) \land g(j) \leq h(j) が成り立つ。また  f が monotone であることより  f(j) = \top が成り立つ。よって  g(j) \leq h(j) が成り立つ。

 f \leq g \Rightarrow h ならば  f \land g \leq h が成り立つこと。
任意の  i \in I に対して  f(i) \land g(i) \leq h(i) を示せばよい。 f(i) = \bot ならば  f(i) \land g(i) \leq h(i) は明らかである。 f(i) = \top とすると  g(i) \leq h(i) が成り立つことを示せばよい。仮定より  f(i) \leq g(i) \Rightarrow h(i) が成り立つが、 f(i) = \top より  g(i) \Rightarrow h(i) = \top である。よって exponential の定義より  g(i) \leq h(i) が成り立つ。

 \square

Exercise 15(b)

 Lemma
\[ y(a) \text{ is monotone}. \] Proof.
任意の  x \leq y \in A^{op} に対して  y(a)(x) \leq y(a)(y) \in {\bf{2}} を示せばよい。 y(a)(x) = \top の場合を考えれば十分である。このとき  x \leq a \in A が成り立つ。また  x \leq y \in A^{op} ならば  y \leq x \in A が成り立つので  y \leq a \in A が成り立つ。よって  y(a)(y) = \top となるので  y(a)(x) \leq y(a)(y) が成り立つ。

 \square

 Lemma
\[ y \text{ is monotone}. \] Proof.
任意の  a \leq b \in A に対して  y(a) \leq y(b) \in {\bf{2}}^{I} を示す。任意の  x \in A^{op} に対して  y(a)(x) = \top とすると  x \leq a \in A が成り立つ。 a \leq b \in A より  x \leq b \in A が成り立つので  y(b)(x) = \top となる。よって  y(a) \leq y(b) \in {\bf{2}}^{I} が成り立つ。

 \square

 Lemma
\[ y \text{ is injective}. \] Proof.
任意の  a,b \in A に対して  y(a) = y(b) が成り立つとする。このとき任意の  x \in A^{op} に対して  y(a)(x) = y(b)(x) が成り立つ。 x = a とすると  y(a)(a) = \top より  y(b)(a) = \top が成り立ち  a \leq b \in A が成り立つ。同様に  x = b とすると  b \leq a \in A が成り立つので  a = b となる。

 \square

 Lemma
\[ y \text{ preserves CCC structure}. \] Proof.

  • preserves terminal object  1

任意の  x \in A^{op} に対して  y(1)(x) = \top が成り立つので  y(1) = 1 \in {\bf{2}}^{I} である。

  • preserves products

任意の  a,b \in A と任意の  x \in A^{op} に対して  y(a \land b)(x) = \left( y(a) \land y(b) \right)(x) を示せばよい。つまり  x \leq a \land b \iff x \leq a \land x \leq b \in A を示せばよいが、これは  a \land b が product であることより明らかである。

  • preserves exponentials

任意の  a,b \in A と任意の  x \in A^{op} に対して  y(a \Rightarrow b)(x) = \left( y(a) \Rightarrow y(b) \right)(x) を示せばよい。つまり  x \leq a \Rightarrow b \iff \forall y \geq x \in A^{op},\, y(a)(y) \leq y(b)(y) を示せばよい。

only if case
 y \leq a \in A とすると  x \leq y \in A^{op} より  y \leq x \in A であるから、 y \leq x \land a が成り立つ。一方、仮定より  x  \leq a \Rightarrow b であるから  x \land a \leq b が成り立つ。よって  y \leq b \in A となるので  y(a)(y) \leq y(b)(y) が成り立つ。

if case
 x \land a \leq x \in A が成り立つことから  x \leq x \land a \in A^{op} が成り立つ。すると仮定より  y(a)(x \land a) \leq y(b)(x \land a) が成り立つ。 x \land a \leq a \in A は常に成り立つので、 y(a)(x \land a) = \top となるから  y(b)(x \land a) = \top つまり  x \land a \leq b \in A が成り立つ。よって  x \leq a \Rightarrow b が成り立つ。

 \square

参考書籍

Category Theory (Oxford Logic Guides)

Category Theory (Oxford Logic Guides)

圏論 原著第2版

圏論 原著第2版