タイトルの通り、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
(とはいえやはり面倒なので、
CCとは category with terminal and all binary products のことを言う。
terminal への unique な射を
binary product からの射影をそれぞれ
また略記として、
CC 上の object A,Bに対し、
CCC とは CC with all exponentials のことを言う。(cf. 私の過去記事 )
CC
この comonad の Kleisli category とその cofree functor を
突然よくわからないものが出てきたと思われるかもしれませんが、この子はCCやCCCにおいて極めて基本的な概念です。基本的すぎて力を借りなくてもゴリ押せちゃうから Kleisli category イヤイヤ人類のせいで廃れちゃった。すごくいい子なのに。人類は愚か。
この子がどう基本的なのかは次を見てください。
つまり CC
この定理から、
よって特に
これから何をしたいのか頭が動いている読者ならもうわかっただろうが、NNO あるいは類似の構造がこの
CC 上の上のような図式について、以下の (N1) から (N4) の条件を考える。ただし、いずれも「任意の
上向きの矢印は当然ながら成り立たない (
ではいつ左向きが成り立ち、あるいは成り立たないのか、そしていつ
CCC 上では(1箇所を除いて)非常に明快である。
よって、CCC 上では (N1) は非常に良い振る舞いをすることがわかる。
しかし一般の CC 上では次の通り、嬉しくない例が存在する。
CC with zero object であって、自明な1点圏とは圏同値ではない圏 (
このとき
なるほど、(N1) は CCC 上では振る舞いが良い一方で、CC 上では必ずしもそうでない。だから普段 NNO を考える際は CCC を課すわけだ。
では CC 上で NNO を考えたい際には、どのような定義を用いるべきか?これにはもう結論が出せて、次の通りである。
NNO として当然成り立ってほしい (N1) を
(N4) まで用意したのに (N3) で結論出てしまったなぁ。とはいえ (N4) はいらない子というわけではなく、計算論的には重要な再帰法であり、CC + (N4) で扱える自然数関数のクラス (cf. 私の過去記事 ) がちょうど primitive recursive function に一致することが知られているなど、なかなか素敵な子なんですよ。CC structure ともほら、仲が良い。
(N4), (WN4) は
最後に CC 上での強弱関係を見たいのだが、weak 版がすこぶる厄介で、まだまだ証明あるいは反例を募集中である。(cf. 私の過去記事 )
思いついた方は是非教えてください。誰が喜ばなくても私はとても喜びます。
おわり。