代数的構造による圏論(8) - エレファント・ビジュアライザー調査記録

第5章まで読めばろいろできると思われるのですが、数学的帰納法について考えるには第7章まで読んだほうが良いようなのでさらに引用していきます。そこまでは少し図式を描いていきます。

第6章冪：プログラムの本質

①冪

定義 6.1 (冪) 積を持つ圏 $\mathcal{C}$ の対象 $A, B$ について、コンマ圏(一般射圏) $(A \times () \to B)$ の終対象を $A$ から $B$ への冪(exponential)と呼びます。

積を持つ圏 $\mathcal{C}$ の対象 $A$ に対して $\mathcal{C}$ から $\mathcal{C}$ への関手 $A \times ()$ は、

任意の対象 $X$ に対して対象 $A \times X$
任意の射 $X \xrightarrow{f} Y$ に対して射 $A \times X \xrightarrow{1_A \times f} A \times Y$

を対応させるものです。

対象 $B$ は圏 $\mathbf{1}$ から $\mathcal{C}$ への関手 $\bar{B}$ と同一視します。 $\bar{B}$ は

圏 $\mathbf{1}$ のただ一つの対象 $X$ に対して対象 $B$
圏 $\mathbf{1}$ のただ一つの射 $1_X$ に対して射 $1_B$

を対応させるものとなります。自然変換 $\bar{B} \overset{t}{\Longrightarrow} \bar{B}$ の成分 $t_X$ は

対象 $B$ に対して対象 $B$
射 $1_B$ に対して射 $1_B$

を対応させるものとなります。

すると $(A \times () \to B)$ の対象は $\mathcal{C}$ の対象 $X$ を用いて $A \times X \to B$ と書ける射となります。終対象は射 $A \times P \xrightarrow{p} B$ で、他に射 $A \times X \xrightarrow{x} B$ があれば、射 $X \xrightarrow{\tilde{x}}P$ で $\require{AMScd}$ \begin{CD}
A \times X @> x >> B \\
@V 1_A \times \tilde{x} VV @| \\
A \times P @>> p > B
\end{CD} を可換にするものが一意に存在するものとなります。このとき対象 $P$ のことも冪と呼び、 $B^A$ と書きます。また射 $p$ は評価射(evalution morphism)と呼び、 $\mathrm{eval}$ と書きます。

「二つの入力を持つ関数」 $X \times Y \xrightarrow{f} Z$ を考えると、冪の普遍性から $X \xrightarrow{\tilde{f}} Z^Y$ で上の図式を可換にするもの、つまり $\mathrm{eval} \circ (1_X \times \tilde{f}) = f$ を満たすものが一意に存在します。このようなことを繰り返して「多変数関数」をただ一つの入力をもつ「一変数関数」の連鎖に変換することをカリー化(currying)と呼びます。また、カリー化された射を元の射に戻すことアンカリー化(uncurrying)と呼びます。

②CCC

定義 6.2 (CCC) 圏が

終対象
任意の対象 $X, Y$ に対しての積 $X \times Y$
任意の対象 $X, Y$ に対しての冪 $Y^X$

を持つとき、カルテジアン閉圏(cartesian closed category)、略して CCC と呼びます。

定義 (点全射) 射 $A \xrightarrow{f} X$ が点全射であるとは、任意の $1 \xrightarrow{x} X$ に対して $1 \xrightarrow{a} A$ で $x = f \circ a$ なるものが存在することをいいます。

定義 (広義の点全射) 射 $A \times B \xrightarrow{g}X$ について、そのカリー化 $B \xrightarrow{\tilde{g}} X^A$ が広義の点全射(weakly point-surjective)であるとは、任意の $A \xrightarrow{h} X$ に対して $1 \xrightarrow{b} B$ で、すべての $1 \xrightarrow{a} A$ に対して $g \circ \binom{a}{b} = h \circ a$ であるようなものが存在することをいいます。\begin{CD}
1 @> a >> A \\
@V \binom{a}{b} VV @VV h V \\
A \times B @>> g > X
\end{CD}

定理 6.3 (Lawvere の不動点定理) 圏 $\mathcal{C}$ は CCC であるとします。射 $A \times A \xrightarrow{f} X$ で、そのカリー化 $A \xrightarrow{\tilde{f}} X^A$ が広義の点全射であるようなものが存在すれば、 $X$ から $X$ 自身への任意の射 $g$ について $1 \xrightarrow{x} X$ で $g \circ x = x$ となるものが存在します。このような射 $1 \xrightarrow{x} X$ を $g$ の不動点(fixed point)と呼びます。

[証明]【 $\tilde{f}$ が広義の点全射だから、どんな射 $A \xrightarrow{h} X$ に対しても射 $1 \xrightarrow{b} A$ で任意の射 $1 \xrightarrow{a} A$ に対して $f \circ \binom{a}{b} = h \circ a$ となるものが存在します。\begin{CD}
1 @> a >> A \\
@V \binom{a}{b} VV @VV h V \\
A \times A @>> f > X
\end{CD} $h$ として特に $A \xrightarrow{\Delta_A} A \times A \xrightarrow{f} X \xrightarrow{g} X$ ( $\Delta_A = \binom{1_A}{1_A}$ )をとれば $f \circ \binom{a}{b} = g \circ f \circ \Delta_A \circ a = g \circ f \circ \binom{1_A}{1_A} \circ a = g \circ f \circ \binom{a}{a}$ となるから、 $a = b$ とすれば $f \circ \binom{b}{b}$ が $g$ の不動点となります。】

$X$ としてちょうど二つの要素からなる集合 $2$ を考え、その二つの要素を True および False と呼びます。 $A$ の部分集合は $A$ から $2$ への写像と同一視することができます。

$A$ から $2^A$ へは単射はあるが全射は存在しません。(対角線論法)

[証明]【 $A$ の各要素を、その要素のみからなる部分集合に対応させる写像は単射となります。全射があったとします。 $\mathbf{Set}$ では点全射と全射は同じことだから、これは上の定理における $\tilde{f}$ となり、言い換えればそのアンカリー化が $f$ となります。すると、 $2$ から自身への任意の写像 $g$ が不動点を持つことになります。「否定」、つまり True と False を入れ替える $2$ から $2$ への写像を考えると、これは不動点を持たないので矛盾となります。よって全射は存在しません。】

第7章圏論的集合論

①トポス (topos)

定義 7.1 (単射・全射) 圏 $\mathcal{C}$ の射 $X \xrightarrow{f} Y$ が単射(monomorphism)であるとは、 $Z \overset{g}{\underset{h}{\rightrightarrows}} X$ で $f \circ g = f \circ h$ なる任意の $g, h$ に対して $g = h$ であるときにいいます。 $f$ は左簡約可能(left cancellable)とも呼びます。双対圏 $\mathcal{C}^\mathrm{op}$ における単射は $\mathcal{C}$ で全射(epimorphism)と呼びます。

定義 7.2 (トポス) 圏 $\mathcal{C}$ が CCC であり、部分対象分類子を持つとき、初等トポス(elementary topos)あるいは単にトポスと呼びます。ここで部分対象分類子(subobject classifier)とは $\mathcal{C}$ の射 $1 \xrightarrow{t} \Omega$ で、任意の単射 $A \xrightarrow{m} B$ に対して射 $B \xrightarrow{\chi_m} \Omega$ で \begin{CD}
A @> !_A >> 1 \\
@V m VV @VV t V \\
B @>> \chi_m > \Omega
\end{CD} が引き戻しの図式となるようなものが一意に存在するものをいいます。このとき $\chi_m$ を $m$ の特性射(characteristic morphism)と呼びます。 $t$ は真(True)とも呼ばれ、また True とも書かれます。そして $\Omega$ は真理値対象(truth value object)と呼ばれます。

定理 7.3 トポスにおいて、単射かつ全射な射は同型射となります。

[証明]【上の図式(図式(1))に $B \xrightarrow{!_B}1$ を追加して図式(2) \begin{CD}
A @> m >> B @> !_B >> 1 \\
@| @. @VV t V \\
A @>> m > B @>> \chi_m > \Omega
\end{CD} とすると図式(1)が可換であることから図式(2)も可換となります。\begin{CD}
A' @> m' >> B @> !_B >> 1 \\
@| @. @VV t V \\
A' @>> m' > B @>> \chi_m > \Omega
\end{CD} が可換とすると、図式(1)が引き戻しの図式であることから、 $A' \xrightarrow{u} A$ が一意的に存在して $m \circ u = m'$ を満たします。\begin{CD}
A' @> m' >> B \\
@V u VV @| \\
A @>> m > B
\end{CD}
$1_B$ は単射なので図式 \begin{CD}
B @> !_B >> 1 \\
@V 1_B VV @VV t V \\
B @>> \chi_{1_B} > \Omega
\end{CD} は可換となります。 $\chi_{1_B} \circ m = \chi_{1_B} \circ 1_B \circ m = t \circ {!_B} \circ m = t \circ {!_A} = \chi_{m} \circ m$ となって、 $m$ が全射(右簡約可能)ならば $\chi_{1_B} = \chi_{m}$ となります。よって \begin{CD}
B @> !_B >> 1 \\
@V 1_B VV @VV t V \\
B @>> \chi_{m} > \Omega
\end{CD} は可換となります。図式(1)が引き戻しの図式であることから $B \xrightarrow{u} A$ で $m \circ u = 1_B$ を満たすものが一意的に存在します。

$m \circ u \circ m = 1_B \circ m = m = m \circ 1_A$ となり、 $m$ が単射(左簡約可能)なので $u \circ m = 1_A$ となります。よって $m$ は同型射となります。】

②圏論的集合論

定義 7.4 以下の条件を満たす圏を集合圏(category of sets)と呼び、 $\mathbf{Set}$ と書きます。

1. $\mathbf{Set}$ はトポスである。
2. $\mathbf{Set}$ の全射は切断を持つ。
3. $\mathbf{Set}$ は well-pointed である。
4. $\mathbf{Set}$ は自然数対象を持つ。

射 $X \xrightarrow{f} Y$ の切断(section)とは、射 $Y \xrightarrow{s} X$ で $f \circ s = 1_Y$ を満たすもののことを言います。条件 2 は選択公理(axiom of choice)と呼びます。

定義 7.5 終対象を持つ圏 $\mathcal{C}$ が well-pointed であるとは。 $1$ が始対象でなく、 $\mathcal{C}$ の任意の相異なる射 $X \overset{f}{\underset{g}{\rightrightarrows}} Y$ に対して射 $1 \xrightarrow{x} X$ で $f \circ x \ne g \circ x$ なるものが存在するときにいいます。

定義 7.6 終対象 $1$ を持つ圏 $\mathcal{C}$ において、自然数対象(natural number object)とは対象 $N$ 、射 $N \xrightarrow{s} N$ および $1 \xrightarrow{z} N$ の組 $\langle N, s, z \rangle$ で、他の同様な組 $\langle X, f, x \rangle$ に対して射 $N \xrightarrow{u} X$ で
\begin{CD}
1 @> z >> N @> s >> N \\
@| @VV u V @VV u V \\
1 @>> x > X @>> f > X \\
\end{CD}
を可換にするものが一意に存在するときにいいます。