Cartesian Category 上での NNO の定義 (元 RIMS 出願用レポート)
はじめに。
タイトルの通り、RIMS 出願のために書きかけたものの、結局出願しなくてお蔵入りになったレポートを再利用したものです。「こいつはこんな怪文書を提出するつもりだったのか・・・」くらいの気持ちでお読みください。
途中で Kleisli category なんかが出てくるので、そこで読むのを諦めてしまう人がいるかも知れません。が、「定義の妥当性を考える」というのは既に綺麗にまとまった数学書を読んでいるだけではあまり触れる機会のないタイプの議論だと思うので、「ほーーんなんかわからんこと言ってるわこいつ」くらいの気分で眺めるのも悪くないと思います。
証明は省略します。やっぱり Mathlog でがっつり証明を書くのは大変だし、手間なだけで難しくはないものばかりなので。
あと Mathlog の XY-pic は一部のブラウザではちゃんと表示されないので気をつけてください。Safari はダメ、Chrome は大丈夫、他は知りません。
はじまりはじまり。
自然数の構造の圏論的一般化である natural numbers object (以下NNO) は、その定義に terminal object しか用いないにも関わらず、通常 cartesian closed category (以下CCC) 上でしか定義されない。それがどうしてなのか、そしてより一般に cartesian category (以下CC) 上での NNO はどのように定義されるべきなのかを考えたい。そこで CCC 上では NNO と同値ないくつかの条件について、その CC 上での振る舞いを調べよう。
以下、structured category とは equipped specified structure のことを言い、その structure を保存する関手とは specified structure を strict に保存するものとして考える。
例えば category with terminal とは、台となる category $\mathcal{C}$, $\mathcal{C}$の object T, $\mathcal{C}$の射の族$(o_A:A\rightarrow T)_{A\in ob(\mathcal{C})}$の組$(\mathcal{C},T,o)$であって$o_A=f$ for all $f:A\rightarrow T$を満たすもののことを言うのであって、単にいずれかの object が terminal になっているだけの category $\mathcal{C}$のことを言うのではない。
(とはいえやはり面倒なので、$T$や$o$を省略して単に「$\mathcal{C}$を category with terminal とする」などと書いたりもする。)
CC について。
CCとは category with terminal and all binary products のことを言う。
terminal への unique な射を$o_A:A\rightarrow T$、
binary product からの射影をそれぞれ $p_{A,B}:A\times B\rightarrow A$, $q_{A,B}:A\times B\rightarrow B$と書くことにする。
また略記として、$\langle fp,gq\rangle:A\times B\rightarrow C\times D$を$f\times g$と書くことにする。
CC 上の object A,Bに対し、$A$による$B$の exponential とは object $B^A$と射$e_{B,A}:B^A\times A\rightarrow B$の組であって、任意の射$f:C\times A\rightarrow B$に対し unique $f^*:C\rightarrow B^A$が存在し、$e_{B,A}(f^*\times\mathsf{id}_A)=f$を満たすものとする。
CCC とは CC with all exponentials のことを言う。(cf. 私の過去記事 )
今回の道具。
CC $\mathcal{C}$とそのobject Aに対し、$\mathcal{C}$上の comonad が次で定まる。
- $-\times A:\mathcal{C}\rightarrow\mathcal{C}$
- $p_{-,A}:-\times A\rightarrow\mathsf{Id}_{\mathcal{C}}$
- $\langle\mathsf{id}_{-\times A},q_{-,A}\rangle :-\times A\rightarrow (-\times A)\times A$
この comonad の Kleisli category とその cofree functor を$H_A:\mathcal{C}\rightarrow\mathcal{C}_A$と書くことにすれば、$\mathcal{C}_A$には$\mathcal{C}$から自然に CC の構造が入り、$H_A$は CC structure を保存する。
突然よくわからないものが出てきたと思われるかもしれませんが、この子はCCやCCCにおいて極めて基本的な概念です。基本的すぎて力を借りなくてもゴリ押せちゃうから Kleisli category イヤイヤ人類のせいで廃れちゃった。すごくいい子なのに。人類は愚か。
この子がどう基本的なのかは次を見てください。
$\mathcal{C}_A$の射$q_{T,A}:T\rightarrow A$を考えれば、組$(\mathcal{C}_A,H_A,q_{T,A})$は同様の組のなかで始普遍的である。
つまり CC $\mathcal{B}$, CC structure を保つ functor $F:\mathcal{C}\rightarrow B$, 射$b:FT\rightarrow FA$の組が与えられたとき、unique な CC structure を保つ functor $F_b:\mathcal{C}_A\rightarrow B$が存在して$F_bH_A=F$かつ$F_b(q_{T,A})=b$を満たす。
$ \xymatrix{ \mathcal{C} \ar[rrd]_{F} \ar[rr]^{H_A} & & \mathcal{C}_A \ar@{.>}[d]^{F_b} & T \ar[rr]^{q_{T,A}} & \ar@{|->}[d] & A \\ \ar@{}[rrru]^{\circlearrowright} & & \mathcal{B} & FT \ar[rr]_b & & FA } $
この定理から、$\mathcal{C}_A$は$\mathcal{C}$に indeterminate arrow $T\rightarrow A$を付け加えて自由生成した CC であると考えることができる。多項式環の類似物と言えば身近に感じてもらえるだろうか。
$\mathcal{C}_A$は$\mathcal{C}$の CC structure だけに注目して自由生成されているのだから、CC structure とは関係のないはずの構造、例えば initial object などは必ずしも保存されない ($Group$を考えよ) 。しかし、CC structure と関わりの深い構造であったり、適切に CC structure と関わるような状況を考えれば、やはり保存されるのである。ほら、次のように。
$\mathcal{C}$が CCC なら、$\mathcal{C}_A$には$\mathcal{C}$から自然に CCC の構造が入り、$H_A$は CCC structure を保存する。
$\mathcal{C}$における colimit が$H_A$によって保存されるための必要十分条件は、その colimit が$-\times A$で保存されることである。
よって特に$\mathcal{C}$が CCC with initial and all binary coproducts なら、$\mathcal{C}_A$には$\mathcal{C}$から自然に CCC with initial and all binary coproducts の構造が入り、$H_A$はその structure を保存する。
逆に、$\mathcal{C}_A$に自然に、$H_A$によって保たれるような形で誘導される構造こそが、CC structure と相性の良い構造であると言えるだろう。
これから何をしたいのか頭が動いている読者ならもうわかっただろうが、NNO あるいは類似の構造がこの$H_A$によって保存されるか否かを見ることで、それが CC と相性が良いかを見るのである。
NNO とその仲間たち。
$
\xymatrix{
T \ar@{->}[r]^{z} & N \ar@{->}[r]^{S} & N
}
$
CC 上の上のような図式について、以下の (N1) から (N4) の条件を考える。ただし、いずれも「任意の$g$, $h$に対しある$f$が一意に存在して可換図式を満たす」という条件である。また、それぞれ$f$の一意性を外した条件を (WN1) から (WN4) とする。
- (N1) NNO である。
$ \xymatrix{ T \ar@{->}[d]^{\mathsf{id}} \ar@{->}[r]^{z} & N \ar@{->}[d]^{f} \ar@{->}[r]^{S} & N \ar@{->}[d]^{f} \\ T \ar@{}[ru]|{\circlearrowright} \ar@{->}[r]^{g} & A \ar@{}[ru]|{\circlearrowright} \ar@{->}[r]^{h} & A \\ } $ - (N2) parametrized NNO である。
$ \xymatrix{ T\times A \ar@{->}[d]^{q} \ar@{->}[r]^{z\times\mathsf{id}} & N\times A \ar@{->}[d]^{f} \ar@{->}[r]^{S\times\mathsf{id}} & N\times A \ar@{->}[d]^{f} \\ A \ar@{}[ru]|{\circlearrowright} \ar@{->}[r]^{g} & B \ar@{}[ru]|{\circlearrowright} \ar@{->}[r]^{h} & B \\ } $ - (N3) recursion in a parameter が実行できる。
$ \xymatrix{ T\times A \ar@{->}[d]^{q} \ar@{->}[r]^{z\times\mathsf{id}} & N\times A \ar@{->}[d]^{f} & N\times A \ar@{->}[d]_{\langle f,q\rangle} \ar@{->}[r]^{S\times\mathsf{id}} & N\times A \ar@{->}[d]^{f} \\ A \ar@{}[ru]|{\circlearrowright} \ar@{->}[r]^{g} & B & B\times A \ar@{}[ru]|{\circlearrowright} \ar@{->}[r]^{h} & B \\ } $ - (N4) primitive recursion が実行できる。
$ \xymatrix{ T\times A \ar@{->}[d]^{q} \ar@{->}[r]^{z\times\mathsf{id}} & N\times A \ar@{->}[d]^{f} & N\times A \ar@{->}[d]_{\langle f,\mathsf{id}\rangle} \ar@{->}[r]^{S\times\mathsf{id}} & N\times A \ar@{->}[d]^{f} \\ A \ar@{}[ru]|{\circlearrowright} \ar@{->}[r]^{g} & B & B\times (N\times A) \ar@{}[ru]|{\circlearrowright} \ar@{->}[r]^{h} & B \\ } $
$ \xymatrix{ \mbox{(N4)} \ar@{=>}[d] \ar@{=>}[r] & \mbox{(N3)} \ar@{=>}[d] \ar@{=>}[r] & \mbox{(N2)} \ar@{=>}[d] \ar@{=>}[r] & \mbox{(N1)} \ar@{=>}[d] \\ \mbox{(WN4)} \ar@{=>}[r] & \mbox{(WN3)} \ar@{=>}[r] & \mbox{(WN2)} \ar@{=>}[r] & \mbox{(WN1)} \\ } $
上向きの矢印は当然ながら成り立たない ($Set$を考えよ) 。
ではいつ左向きが成り立ち、あるいは成り立たないのか、そしていつ$H_A$で保たれるのかを見ていこう。
CCC 上では(1箇所を除いて)非常に明快である。
$ \xymatrix{ \mbox{(N4)} \ar@{=>}[d] \ar@{<=>}[r] & \mbox{(N3)} \ar@{=>}[d] \ar@{<=>}[r] & \mbox{(N2)} \ar@{=>}[d] \ar@{<=>}[r] & \mbox{(N1)} \ar@{=>}[d] \\ \mbox{(WN4)} \ar@{=>}[r] & \mbox{(WN3)} \ar@{<=>}[r] & \mbox{(WN2)} \ar@{<=>}[r] & \mbox{(WN1)} \\ } $
- (N3) in $\mathcal{C}$ $\iff$ (N1) in $\mathcal{C}_A$ for all $A\in ob(\mathcal{C})$
- (WN3) in $\mathcal{C}$ $\iff$ (WN1) in $\mathcal{C}_A$ for all $A\in ob(\mathcal{C})$
$\mathcal{C}$が CCC なら、(N1), (WN1) は$H_A$で保存される。
よって、CCC 上では (N1) は非常に良い振る舞いをすることがわかる。
しかし一般の CC 上では次の通り、嬉しくない例が存在する。
CC with zero object であって、自明な1点圏とは圏同値ではない圏 ($Relation$や$Group$など) を考える。
このとき $0\rightarrow 0\rightarrow 0$ は (N1) だが、(WN2) ではない。よって特に、(N1) であることが$H_A$で保存されない。
なるほど、(N1) は CCC 上では振る舞いが良い一方で、CC 上では必ずしもそうでない。だから普段 NNO を考える際は CCC を課すわけだ。
では CC 上で NNO を考えたい際には、どのような定義を用いるべきか？これにはもう結論が出せて、次の通りである。
- (N3) in $\mathcal{C}$ $\iff$ (N3) in $\mathcal{C}_A$ for all $A\in ob(\mathcal{C})$
- (WN3) in $\mathcal{C}$ $\iff$ (WN3) in $\mathcal{C}_A$ for all $A\in ob(\mathcal{C})$
NNO として当然成り立ってほしい (N1) を$\mathcal{C}_A$上で満たすためには、定理5から (N3) であれば必要かつ十分であったわけだが、さらに定理6が言うには (N3) は$H_A$で保存されるのである。
したがって、CC 上で NNO を考えるなら (N3) の定義を用いるのが筋が良いと言える。
(N4) まで用意したのに (N3) で結論出てしまったなぁ。とはいえ (N4) はいらない子というわけではなく、計算論的には重要な再帰法であり、CC + (N4) で扱える自然数関数のクラス (cf. 私の過去記事 ) がちょうど primitive recursive function に一致することが知られているなど、なかなか素敵な子なんですよ。CC structure ともほら、仲が良い。
(N4), (WN4) は$H_A$で保存される。
最後に CC 上での強弱関係を見たいのだが、weak 版がすこぶる厄介で、まだまだ証明あるいは反例を募集中である。(cf. 私の過去記事 )
- (N1) $\not\Rightarrow$ (N2)
- (WN1) $\not\Rightarrow$ (WN2)
- (N2) $\Rightarrow$ (N3)
- (N3) $\Rightarrow$ (N4)
- (WN2) $\Rightarrow$ (WN3)
- (WN3) $\Rightarrow$ (WN4)
- (WN3) $\Rightarrow$ (WN4) in CCC
思いついた方は是非教えてください。誰が喜ばなくても私はとても喜びます。
おわり。