デカルト作用圏がどうにもオモロいわコレ。ヤバいわコレ。
で、作用圏の純部分圏*1をデカルト圏からデカルト半環圏にしたいな、と思ってます。「デカルト作用圏が面白い」に書いたように、「デカルト圏 → デカルト半環圏」の置き換えはたいして手間がかからず、御利益としては、if文やswitch/case文が扱えるようになります。デカルト積とは違い、デカルト和のほうは作用圏の全域に広げても対称モノイド積（「和」という名の「積」）なので、足し算は扱いやすいままであるのも素敵。
とりあえず、デカルト（Cartesian）とは限らない、掛け算の対称性も仮定しない一般的な半環圏の定義を確認しておきます。と思っても、この定義がけっこうみつけにくいのですよね； なかなかころがってない。シャイ・ハランの "Non-Additive Geometry" の ring category の定義を参考にします。
演算は掛け算×と足し算+ですが、掛け算記号は省略します。掛け算も足し算も原則は二項演算で、A+B+C のように書いたら (A+B)+C のことだとします。三項（一般にはn項）の公平演算（unbiased operation）てのもあるし、自然で便利なんだけど、今は二項演算の繰り返しということで。
計算法則に関係する同型（自然変換）を次の記号で表します。ギリシャ文字じゃなくて英小文字を使います。（これらの基本的な同型をCatyScript2.0で書くとどうなるかは http://d.hatena.ne.jp/m-hiyama-memo/20101229/1293583002 に書いておきました。）
| 計算法則 | 同型射 | 掛け算のとき | 足し算のとき |
|---|---|---|---|
| 結合律 | a | (AB)C → A(BC) | (A+B)+C → A+(B+C) |
| 単位律 | u | 1A → A | 0+A → A |
| 零律 | z | 0A → 0 | |
| 交換律 | c | A+B → B+A |
以下のごとくに横着します。
- 足し算と掛け算に関して同じ記号（aとか）を使う。
- 左右両方の法則と同型が必要だが、片一方しか書いてない。例えば、1A→A 以外に A1→A が要るが省略。
- 自然変換の添字はもちろん省略。
交換律に対応するcは対称同型で、足し算にだけ働きます。掛け算は対称性を仮定しません。掛け算だけ、足し算だけに関する一貫性（coherence）は省略します。
分配律を与える同型は次のとおり：
- d:A(B+C) → AB + BC
掛け算の対称性は仮定してないので、d':(A+B)C → AC + BC も必要ですが、横着して同じ記号 d で表します。
以下に、分配法則に関連する一貫性をアスキーアート風に書きます。要するに、中学校あたりで習った計算法則を保証するものです。（以下で、u'はuの逆射。）
A(B+C+D) ⇒ AB+(AC+AD)
A(B+C+D) -(Aa)-> A(B+(C+D)) | | (d) (d) v v A(B+C)+AD AB+A(C+D) | | (d+AD) (AB+d) v v (AB+AC)+AD -(a)-> AB+(AC+AD)
AB(C+D) ⇒ A(BC)+A(BD)
AB(C+D) -(a)-> A(B(C+D)) | | (d) (Ad) | v | A(BC+BD) | | | (d) v v ABC+ABD -(a+a)->A(BC)+A(BD)
1(A+B) ⇒ A+B
1(A+B) -(u)-> A+B | | (d) (=) v v 1A+1B -(u+u)->A+B
A(B+0) ⇒ AB+0
A(B+0) -(Au)-> AB | | (d) (u') v v AB+A0 -(AB+z)->AB+0
A(B+C) ⇒ AC+AB
A(B+C) -(Ac)->A(C+B) | | (d) (d) v v AB+AC -(c)-> AC+AB
これらの定義には、対象に対する掛け算／足し算と同型しか出てきません。モノイド積にはならない不純な積であっても、それぞれの同型が中心射であるという条件を付け加えれば、そのまま使えます。つまり、掛け算が対称とも純粋とも限らない不純なデカルト半環圏（ただし、足し算は純粋で対称）も、通常のデカルト半環圏と同じように定義できます。
デカルト半環作用圏は、外の圏Kが不純なデカルト半環圏*2で、その構造を純部分圏に制限するとデカルト半環圏になるようなものとして定義できるでしょう。まだ細部をチェックしてないので、僕がチョンボしている可能性はありますが。
