奇妙じゃなかった、これは役に立つ圏

奇妙だと思っていたのは僕の誤った印象だったようです。

• 役に立ちそうだが奇妙な圏
• 続報・役に立ちそうだが奇妙な圏： コレ、使えそう

基点付き集合（pinted set）を対象として、基点を基点に移す全域（total）な関係を射とする圏TotPtRelは、どうやら、良い構造を持った役に立つ圏のようです。

奇妙だと思った事情

TotPtRelのホムセット TotPtRel(A, B) は、AとBの直積のベキ集合である Pow(A×B) の部分集合になっています； つまり、TotPtRel(A, B)⊆Pow(A×B) 。べき集合 Pow(A×B) には集合の合併演算があるので、それをそのまま使ってホムセットに足し算を入れるのは「自然」だと思ったわけです。

ですが、実は、自然じゃなかったんですね。ホムセットを直接に豊饒化（enrichment）するのではなくて、すべての対象に可換ベキ等なモノイド構造が入ることを利用して足し算を定義すべきだったのです。

直和と2つのテンソル積

基点付き集合を A = (A, ⊥_A) と書きます。下付きのAは省略することがあります。また、A_○ := A - {⊥_A} とします（以前の記事で使った記法です）。+と×は、集合の直和と直積（圏の直和・直積になるとは限らない）です。

A # B := A_○ + A_○ + {⊥} と定義すると、#は圏TotPtResの直和になります。標準入射 A→(A # B)、B→(A # B) は自明な埋め込みです。f:A→X、g:B→X に対して余タプル [f, g]:(A # B)→X が構成できます。また、射に対しても#は定義できて、f:A→X、g:B→Y なら (f # g) : (A # B)→(X # Y) となります。

圏TotPtRelで特徴的なことは、直和以外に2つのテンソル積を持つことです。「テンソル積」という言葉に厳密な定義はありませんが、ここでは、直和・直積とは別なモノイド積という程度の意味で使っています。1つめのテンソル積は集合の直積（圏の直積にはなりません）、2つめのテンソル積は、A*B := A_○×A_○ + {⊥} として定義される積です。

積×はお馴染みの構成ですが、外の圏TotPtRelが集合圏ではないので圏の直積ではなく、直和に対して分配的でもありません。積*も圏の直積ではありませんが、直和に関して分配的になります。

3つのモノイド積 #、×、* の関係はあまりよく分かってないのですが、U_A,B:A×B→A*B という標準的な射はあります。次のように定義されます。

1. a∈A_○, b∈B_○ のとき、U(a, b) = {(a, b)}
2. a∈A_○ のとき、U(a, ⊥_B) = {⊥}
3. b∈B_○ のとき、U(⊥_A, b) = {⊥}
4. U(⊥_A, ⊥_B) = {⊥}

色々な射達

TotPtRelのメリットのひとつは、圏に組み込まれているともいえる標準的な射が豊富にあることです。それらを列挙します。

1. 直和の対角： Δ^#_A:A→(A # A) -- Aを2つのコピーに振り分ける。a |→ {a} + {a} 。
2. 直和の余対角： ∇^#_A:(A # A)→A -- 2枚のコピーを重ねる操作、余タプル [id_A, id_A] として書ける。
3. ×の対角： Δ^×_A:A→A×A -- (a, a) を作る。
4. *の対角： Δ^*_A:A→A*A -- これも (a, a) を作る。

×と*の余対角も定義できますが、その前に積から和への標準的な射を紹介します：

1. W^×_A,B:A×B→(A # B)
2. W^*_A,B:A*B→(A # B)

W^×_A,Bは、「続報・役に立ちそうだが奇妙な圏： コレ、使えそう」で述べた射です。もう1つの射 W^*_A,B:A×B→(A # B) は次のように定義します。

1. a∈A_○, b∈B_○ のとき、W^*(a, b) = {a} + {b}
2. a∈A_○ のとき、W^*(a, ⊥_B) = {⊥}
3. b∈B_○ のとき、W^*(⊥_A, b) = {⊥}
4. W^*(⊥_A, ⊥_B) = {⊥}

×と*の余対角は、W^×とW^*を用いて、次のように定義します。

1. ×の余対角： ∇^×_A := W^×;∇^# :A×A→A
2. *の余対角： ∇^*_A := W^*;∇^# :A*A→A

∇^×_Aは、「続報・役に立ちそうだが奇妙な圏： コレ、使えそう」ではw_Aと書いていた射です。

足し算とEnd半環

×の余対角∇^×_Aを使って、f, g:A→B の足し算を次のように定義できます*1。

• f + g := Δ^×_A;(f×g);∇^×_B

これは、足し算として期待される計算法則を満たします。

特に、f, g:{1, ⊥}→{1, ⊥} のとき、自己射からなるホムセット End({1, ⊥}) = TotPtRel({1, ⊥}, {1, ⊥}) は、今定義した足し算と射の結合を掛け算として半環となります。この半環は、「真、偽、不明」という三値の論理として自然に解釈できます。奇妙なところはありません。

変ではない

というわけで、圏TotPtRelは変な圏ではないようです。モノイド積が3つ（うち1つは直和）あるのが珍しい、というかあまり扱い慣れてないタイプの圏ですが、それぞれのモノイド積に固有の役割があるし、モノイド積のあいだの相互関係も調べればもっと分かるでしょう。この圏、無限走行する（non terminating）かもしれない非決定性計算のモデルにちゃんと使えますね。

*1:Δ^*_A;(f*g);∇^*_B という“足し算”も定義できます。これは論理ANDになるようです。