代数的構造による圏論(4) - エレファント・コンピューティング調査報告

このブログでは、通常の論理プログラミングでは無限に動くプログラムを書くことができないので「極限」の考え方でなんとかできないか、ということでやっています。ある種の射影的極限、帰納的極限は外積の定義を書いたところで書いたように、構成的に定義することができるようなので、このやり方で書いてみるとプログラミング言語で書くことができるのではないかと考えています。

この本では、極限の説明の前に「コンマ圏」があるので、「コンマ圏」についても「構成的な書き方」ができるか考えてみたいと思います。この本では、さらにその前に自然変換の説明があり、自然変換をメインに説明されているようです。自然変換については、そのように書き方を変えることができるかどうかわかりませんが、できるならやってみます。その前に、自然変換の定義が間違っていたようなので、圏の定義から書き直しておきます。

圏の定義

圏 $\mathcal{C}$ というものは、以下の(集合とは限らない)類

対象の類 $\mathrm{ob}(\mathcal{C})$
対象の間の射の類 $\mathrm{hom}(\mathcal{C})$

で構成されて以下の条件が成り立つとき、 $\mathcal{C}$ を圏と呼びます。

射 $f \in \mathrm{hom}(\mathcal{C})$ には域と呼ばれる対象 $A \in \mathrm{ob}(\mathcal{C})$ および余域と呼ばれる対象 $B \in \mathrm{ob}(\mathcal{C})$ がただ一つ存在します。このとき「 $f$ は $A$ から $B$ への射である」と言い、 $f: A \to B$ (または $f: A \to B \ (\in \mathcal{C})$ )と書き、 $A$ を $\mathrm{dom}(f)$ 、 $B$ を $\mathrm{cod}(f)$ と書きます。
、であるとき、射の合成と呼ばれるが一意的に存在し、以下の結合律、単位律が成り立ちます。
- 結合律: $f: A \to B$ 、 $g: B \to C$ 、 $h: C \to D$ ならば $h \circ (g \circ f) = (h \circ g) \circ f$ が成り立ちます。
- 単位律: 任意の $A ∈ \mathrm{ob}(\mathcal{C})$ に対して $A$ の恒等射と呼ばれる射 $1_A: A \to A$ が存在して、任意の射 $f: A \to X$ および $g: X \to A$ に対して $1_A \circ f = f$ 、 $g \circ 1_A = g$ が成り立ちます。

関手の定義

圏 $\mathcal{C}$ から圏 $\mathcal{D}$ への対応 $F$ が、以下の条件を満たすとき $\mathcal{C}$ から $\mathcal{D}$ への関手と呼びます( $F: \mathcal{C} \to \mathcal{D}$ と書きます)。

$\mathcal{C}$ の各対象 $X$ を $\mathcal{D}$ の各対象 $F(X)$ に対応させる。
$\mathcal{C}$ の射 $f$ を $\mathcal{D}$ の射 $F(f)$ に対応させる。
$f: X \to Y \ (\in \mathcal{C})$ ならば $F(f): F(X) \to F(Y) \ (\in \mathcal{D})$ 。
$f: X \to Y \ (\in \mathcal{C})$ 、 $g: Y \to Z \ (\in \mathcal{C})$ ならば $F(g \circ f) = F(g) \circ F(f)$ 。
$\mathcal{C}$ の各対象 $X$ に対して $F(1_X) = 1_{F(X)}$ が成り立つ。

自然変換の定義

$\require{AMScd}$ $F$ 、 $G$ を圏 $\mathcal{C}$ から $\mathcal{D}$ への関手とします。以下の条件が成り立つものを $F$ から $G$ への自然変換 $t$ と呼び、 $F \overset{t}{\Longrightarrow} G$ (または $F \overset{t}{\Longrightarrow} G \ (: \mathcal{C} \to \mathcal{D})$ )と書きます。

$\mathcal{C}$ の各対象 $X$ に $\mathcal{D}$ の射 $t_X: F(X) → G(X)$ を対応させる。 $t_X$ を $t$ の $X$ 成分と呼ぶ。
$f: X → Y \ (\in \mathcal{C})$ に対して $G(f) \circ t_{X} = t_{Y} \circ F(f)$ が成り立つ。(以下の図式は可換)

\begin{CD}
F(X) @> t_{X} >> G(X) \\
@V F(f) VV @VV G(f) V \\
F(Y) @>> t_{Y} > G(Y)
\end{CD}

関手圏

$F$ 、 $G$ 、 $H$ を圏 $\mathcal{C}$ から圏 $\mathcal{D}$ への関手、 $F \overset{t}{\Longrightarrow} G$ 、 $G \overset{u}{\Longrightarrow} H$ を自然変換とするとき、これらの合成(垂直合成)を $(ut)_X := u_X \circ t_X$ ( $X$ は $\mathcal{C}$ の対象)と定義すると、自然変換 $F \overset{ut}{\Longrightarrow} H$ となります。すなわち

$ut$ は $\mathcal{C}$ の対象 $X$ に $(ut)_X: F(X) \to H(X)$ を対応させ
$f: X → Y \ (\in \mathcal{C})$ ならば $H(f) \circ (ut)_{X} = H(f) \circ u_{X} \circ t_{X} = u_{Y} \circ G(f) \circ t_{X} \\ = u_{Y} \circ t_{Y} \circ F(f) = (ut)_{Y} \circ F(f)$

が成り立ちます。(以下の図式は可換)
\begin{CD}
F(X) @> t_{X} >> G(X) @> u_{X} >> H(X) \\
@V F(f) VV @VV G(f) V @VV H(f) V \\
F(Y) @>> t_{Y} > G(Y) @>> u_{Y} > H(Y)
\end{CD}
この合成(垂直合成)は結合律、単位律を満たします。

(結合律) $F$ 、 $G$ 、 $H$ 、 $I$ を圏 $\mathcal{C}$ から圏 $\mathcal{D}$ への関手、 $F \overset{t}{\Longrightarrow} G$ 、 $G \overset{u}{\Longrightarrow} H$ 、 $H \overset{v}{\Longrightarrow} I$ を自然変換とすると、 $\mathcal{D}$ の射の結合律より $X$ が $\mathcal{C}$ の対象のとき $( (vu)t)_X = (vu)_X \circ t_X = (v_X \circ u_X) \circ t_X \\ = v_X \circ (u_X \circ t_X) = v_X \circ (ut)_X = (v(ut))_X$
(単位律) 、、を圏から圏への関手、、を自然変換とします。の対象に対してとすると以下の(1)よりは自然変換となり、(2-1)、(2-2)よりはこの合成(垂直合成)の単位元となります。
- (1) $f: X → Y \ (\in \mathcal{C})$ ならば $G(f) \circ t_{X} = t_{X} \circ G(f)$
- (2-1) 任意の $\mathcal{C}$ の対象 $X$ に対して $(ut)_X = u_X \circ t_X = 1_{G(X)} \circ t_X = t_X$ となることから $ut = t$ (任意の成分が一致)
- (2-2) 任意の $\mathcal{C}$ の対象 $X$ に対して $(vu)_X = v_X \circ u_X = v_X \circ 1_{G(X)} = v_X$ となることから $vu = v$ (任意の成分が一致)

圏 $\mathcal{C}$ から圏 $\mathcal{D}$ への関手を対象とし、それらの間の自然変換を射とする圏を、圏 $\mathcal{C}$ から圏 $\mathcal{D}$ への関手圏と呼び、 $\mathrm{Fun}(\mathcal{C}, \mathcal{D})$ と書きます。