第11回 指数対象 デカルト閉圏
指数対象
指数対象\(B^A\)とは対象間の射の集合の一般化。\(\mathcal{Sets}\)では\(B^A=Hom_{\mathcal{Sets}}(A,B)\)。ただしHom集合では内部構造を使った定義であり、射の関係になっていない。
\(\mathcal{Sets}\)の射で考えると指数対象はカリー化になる。\(f:X\times A \rightarrow B\)という射はXとAの要素を引数にとりBの要素に対応させる。この\(f\)に対して、\(\widetilde{f}:X\rightarrow B^A\)という射を、Xの要素を引数にとり、\(A\)から\(B\)への射を対応させる。この射\(\widetilde{f}(x)\)に\(A\)の要素を引数として与えると\(B\)の要素が対応する。この対応を\(\epsilon\)と書くことにする。可換図式は以下の通り。
$$\xymatrix{
(x,a)\in X\times A \ar[rd]^f \ar[d]_{\widetilde{f}\times 1_A} & \\
(\widetilde{f}(x),a)\in B^A\times A \ar[r]_-{\epsilon}& B \ni \widetilde{f}(x)(a)=f(x,a)\\
}$$
ここで\(f\)に対応するカリー化\(\widetilde{f}\)は唯一に決まること、集合の要素の関係を忘れると次の定義と可換図式を得る。
指数対象の定義
任意の2つの対象について直積が定義できる圏において、指数対象とは\((B^A, \epsilon)\)の組で、任意の対象\(X\)と任意の射\(f:X\times A \rightarrow B\)について下記の図式を可換にする\(\widetilde{f}\)が唯一存在すること。
\(\epsilon\)を評価射(evaluation map)と呼ぶ。
$$\xymatrix{
X\times A \ar[rd]^f \ar@{.>}[d]_{\widetilde{f}\times 1_A} & \\
B^A\times A \ar[r]_-{\epsilon}& B
}$$
この時、\(f\)を\(\widetilde{f}\)に対応さることをカリー化\((\widetilde{-})\)、逆に\(\widetilde{f}\)を\(f\)に対応させることを逆カリー化\((\overline{-})\)と呼ぶ。すると次の同型対応が成り立つ。
$$ (\widetilde{-}):Hom_C(X\times A, B) \cong Hom_C(X,B^A) : (\overline{-}) $$
デカルト閉圏
デカルト閉圏は計算と射の対応がある、という話と関係する。デカルト閉圏とは大雑把には直積と指数対象がある圏として定義される。直積によりレコード型が定義でき、指数対象によって関数型と関数への引数の適用(評価射)が定義される、と見ることが出来る。
デカルト閉圏の定義
圏\(\mathcal{C}\)において、任意の有限個の対象に対して直積があり、任意の2つの対象に対して指数対象があれば、圏\(\mathcal{C}\)をデカルト閉圏(Cartesian Closed Category)という。
定理:デカルト閉圏では、
任意の対象\(A\)について\(A^1 \cong A\) 。
任意の対象\(A,B,C\)について\(C^(A\times B) \cong (C^B)^A\) 。
任意の対象\(A\)について\(1^A \cong 1\) 。
任意の対象\(A,B,C\)について\((B\times C)^A \cong B^A\times C^A\) 。
べたにも証明できるが、Hom集合を使った考え方。
$$ Hom_C(1,A)\cong A $$
$$ Hom_C(A\times B, C)\cong Hom_C(A, C^B) $$
$$ Hom_C(A,1)\cong 1 $$
$$ Hom_C(A,B\times C)\cong Hom_C(A,B)\times Hom_C(A,C) $$
などが成り立つことと、米田の補題を使うのが良いらしい。
デカルト閉圏の分配則
定理:デカルト閉圏で始対象と任意の対象\(A,B\)に余積\(A+B\)が存在する場合、以下が成り立つ。これを分配的という。
$$ A\times B + A\times C \cong A\times (B+C) $$
証明の概要:
$$ \begin{eqnarray}
\notag Hom_C(A\times (B+C),X) &\cong& Hom_C(B+C,X^A) \\
\notag &\cong& Hom_C(B,X^A) \times Hom_C(C,X^A) \\
\notag &\cong& Hom_C(A\times B, X) \times Hom_C(A\times C, X) \\
\notag &\cong& Hom_C(A\times B + A\times C, X)
\end{eqnarray}$$
講義ではこの後はカリー・ハワード・ランベック対応の解説となります。型付ラムダ計算と命題論理とデカルト閉圏は同型関係がある、という話です。ここは省略。