5

Cartesian Category 上での NNO の定義 (元 RIMS 出願用レポート)

597
0

はじめに。

タイトルの通り、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 C, Cの object T, Cの射の族(oA:AT)Aob(C)の組(C,T,o)であってoA=f for all f:ATを満たすもののことを言うのであって、単にいずれかの object が terminal になっているだけの category Cのことを言うのではない。
(とはいえやはり面倒なので、Toを省略して単に「Cを category with terminal とする」などと書いたりもする。)

CC について。

CC

CCとは category with terminal and all binary products のことを言う。

terminal への unique な射をoA:AT
binary product からの射影をそれぞれ pA,B:A×BA, qA,B:A×BBと書くことにする。

また略記として、fp,gq:A×BC×Df×gと書くことにする。

CCC

CC 上の object A,Bに対し、AによるBの exponential とは object BAと射eB,A:BA×ABの組であって、任意の射f:C×ABに対し unique f:CBAが存在し、eB,A(f×idA)=fを満たすものとする。

CCC とは CC with all exponentials のことを言う。(cf. 私の過去記事 )

今回の道具。

CC Cとそのobject Aに対し、C上の comonad が次で定まる。

  • ×A:CC
  • p,A:×AIdC
  • id×A,q,A:×A(×A)×A

この comonad の Kleisli category とその cofree functor をHA:CCAと書くことにすれば、CAにはCから自然に CC の構造が入り、HAは CC structure を保存する。

突然よくわからないものが出てきたと思われるかもしれませんが、この子はCCやCCCにおいて極めて基本的な概念です。基本的すぎて力を借りなくてもゴリ押せちゃうから Kleisli category イヤイヤ人類のせいで廃れちゃった。すごくいい子なのに。人類は愚か。

この子がどう基本的なのかは次を見てください。

functional completeness

CAの射qT,A:TAを考えれば、組(CA,HA,qT,A)は同様の組のなかで始普遍的である。
つまり CC B, CC structure を保つ functor F:CB, 射b:FTFAの組が与えられたとき、unique な CC structure を保つ functor Fb:CABが存在してFbHA=FかつFb(qT,A)=bを満たす。

CFHACAFbTqT,AABFTbFA

この定理から、CACに indeterminate arrow TAを付け加えて自由生成した CC であると考えることができる。多項式環の類似物と言えば身近に感じてもらえるだろうか。

CACの CC structure だけに注目して自由生成されているのだから、CC structure とは関係のないはずの構造、例えば initial object などは必ずしも保存されない (Groupを考えよ) 。しかし、CC structure と関わりの深い構造であったり、適切に CC structure と関わるような状況を考えれば、やはり保存されるのである。ほら、次のように。

Cが CCC なら、CAにはCから自然に CCC の構造が入り、HAは CCC structure を保存する。

Cにおける colimit がHAによって保存されるための必要十分条件は、その colimit が×Aで保存されることである。

よって特にCが CCC with initial and all binary coproducts なら、CAにはCから自然に CCC with initial and all binary coproducts の構造が入り、HAはその structure を保存する。

逆に、CAに自然に、HAによって保たれるような形で誘導される構造こそが、CC structure と相性の良い構造であると言えるだろう。

これから何をしたいのか頭が動いている読者ならもうわかっただろうが、NNO あるいは類似の構造がこのHAによって保存されるか否かを見ることで、それが CC と相性が良いかを見るのである。

NNO とその仲間たち。

NNO

TzNSN
CC 上の上のような図式について、以下の (N1) から (N4) の条件を考える。ただし、いずれも「任意のg, hに対しあるfが一意に存在して可換図式を満たす」という条件である。また、それぞれfの一意性を外した条件を (WN1) から (WN4) とする。

  • (N1) NNO である。
    TidzNfSNfTgAhA
  • (N2) parametrized NNO である。
    T×Aqz×idN×AfS×idN×AfAgBhB
  • (N3) recursion in a parameter が実行できる。
    T×Aqz×idN×AfN×Af,qS×idN×AfAgBB×AhB
  • (N4) primitive recursion が実行できる。
    T×Aqz×idN×AfN×Af,idS×idN×AfAgBB×(N×A)hB
明らかな強弱関係

(N4)(N3)(N2)(N1)(WN4)(WN3)(WN2)(WN1)

上向きの矢印は当然ながら成り立たない (Setを考えよ) 。
ではいつ左向きが成り立ち、あるいは成り立たないのか、そしていつHAで保たれるのかを見ていこう。

CCC 上では(1箇所を除いて)非常に明快である。

CCC 上では

(N4)(N3)(N2)(N1)(WN4)(WN3)(WN2)(WN1)

  • (N3) in C (N1) in CA for all Aob(C)
  • (WN3) in C (WN1) in CA for all Aob(C)

Cが CCC なら、(N1), (WN1) はHAで保存される。

よって、CCC 上では (N1) は非常に良い振る舞いをすることがわかる。
しかし一般の CC 上では次の通り、嬉しくない例が存在する。

CC with zero object であって、自明な1点圏とは圏同値ではない圏 (RelationGroupなど) を考える。
このとき 000 は (N1) だが、(WN2) ではない。よって特に、(N1) であることがHAで保存されない。

なるほど、(N1) は CCC 上では振る舞いが良い一方で、CC 上では必ずしもそうでない。だから普段 NNO を考える際は CCC を課すわけだ。

では CC 上で NNO を考えたい際には、どのような定義を用いるべきか?これにはもう結論が出せて、次の通りである。

  • (N3) in C (N3) in CA for all Aob(C)
  • (WN3) in C (WN3) in CA for all Aob(C)

NNO として当然成り立ってほしい (N1) をCA上で満たすためには、定理5から (N3) であれば必要かつ十分であったわけだが、さらに定理6が言うには (N3) はHAで保存されるのである。

したがって、CC 上で NNO を考えるなら (N3) の定義を用いるのが筋が良いと言える。

(N4) まで用意したのに (N3) で結論出てしまったなぁ。とはいえ (N4) はいらない子というわけではなく、計算論的には重要な再帰法であり、CC + (N4) で扱える自然数関数のクラス (cf. 私の過去記事 ) がちょうど primitive recursive function に一致することが知られているなど、なかなか素敵な子なんですよ。CC structure ともほら、仲が良い。

(N4), (WN4) はHAで保存される。

最後に CC 上での強弱関係を見たいのだが、weak 版がすこぶる厄介で、まだまだ証明あるいは反例を募集中である。(cf. 私の過去記事 )

私が分かっている部分。
  • (N1) (N2)
  • (WN1) (WN2)
  • (N2) (N3)
  • (N3) (N4)
証明あるいは反例を募集中。
  • (WN2) (WN3)
  • (WN3) (WN4)
  • (WN3) (WN4) in CCC

思いついた方は是非教えてください。誰が喜ばなくても私はとても喜びます。

おわり。

投稿日:202186
OptHub AI Competition

この記事を高評価した人

高評価したユーザはいません

この記事に送られたバッジ

バッジはありません。
バッチを贈って投稿者を応援しよう

バッチを贈ると投稿者に現金やAmazonのギフトカードが還元されます。

投稿者

うお。
うお。
21
2240
趣味の話をするマン。

コメント

他の人のコメント

コメントはありません。
読み込み中...
読み込み中
  1. はじめに。
  2. はじまりはじまり。
  3. CC について。
  4. NNO とその仲間たち。