必要があって、今日の午前中スターバックスで絵算。長谷川真人（はせがわ・まさひと）さん等による定理を確認しただけですが、なんか疲れましたねー。
なんに必要か？とか背景とかは全部割愛。スンマセン。以下に予備知識あるいは関連するエントリー。
- ホップ代数の絵算 2：割り算と逆元
- こんな簡単なトレース付きモノイド圏があったなんて
- やっぱりこれからはフローチャートだな
- 双モノイドの簡単な例 -- 自然数の足し算と余足し算
- フローチャートからマゾ・テストまで
トレース、ダガー、スター
C = (C, +, 0, σ) を対称モノイド圏として、対称なモノイド積+（足し算の形に書きました）に関してトレースTrもあるとします。つまり、(C, +, 0, σ, Tr) がトレース付き対称モノイド圏です*1。
f:A+X→B+X に対して、Tr(f) = TrA,BX(f) :A→B となります。トレースについて今は説明しませんが、次のような公理で特徴付けられます。
fのトレースTr(f)を、f← とも書くことにします。
さらに、圏Cには余対角∇があるとします。この状況で、f:X→A+X のエルゴット（Calvin C. Elgot）のダガー f†:X→A は次のように定義されます。
- f† := [∇;f]←
[追記]以下で「クリーネスター」と書いているところは、スターじゃなくてプラス、つまり1回以上の繰り返しでした。*を+に直すとダガー†と区別が付きにくいので、*>0 と訂正することにします。また、クリーネプラスって用語も一般的じゃないので、クリーネスター（1回以上）としておきます。絵の方はそのままです。[/追記]
圏Cに対角Δもあると、f:A→A のクリーネスター（1回以上） f*>0:A→A も定義できます。
- f*>0 := [f;Δ]† = [∇;(f;Δ)]←
トレース（←）からエルゴットダガー（†）、エルゴットダガーからクリーネスター（1回以上）（*>0）が定義できます。これは逆も成立します。
- 単位iと余対角∇を持つ対称モノイド圏では、トレースとエルゴットダガーは1：1に対応する。
- 上の条件に加えて、余単位!と対角Δを持つ対称モノイド圏では、エルゴットダガーとクリーネスター（1回以上）は1：1に対応する。
単位iと余対角∇を持つ対称モノイド圏とは余デカルト圏のことで、余単位!と対角Δを持つ対称モノイド圏とはデカルト圏のことです。単位、余対角、余単位、対角を全部備えていて、さらに若干の条件を満たす圏は双デカルト圏で、すべての対象が双モノイド（双代数）構造を持ちます。これらの概念・用語を使えば、上の命題は次のように言い換えられます。
余デカルト圏の双対はデカルト圏で、エルゴットダガーの双対はコンウェイダガーとも呼ばれる不動点演算子です。トレースは自己双対的な概念なので、トレースの双対はトレースです。よって次が成立します。
このような事実は、1980年代末にカザネスク／ステファネスク（Cazanescu, Stefanescu）により認識されていました。ハイランド（Hyland）も同じことを述べているようです。一般的かつ完全な記述は、長谷川真人（はせがわ・まさひと）さんにより与えられました。
絵算
f† := [∇;f]← と f*>0 := [f;Δ]† に対して、逆向きの公式を絵で与えます。
- 定義：f† := [∇;f]←
- 逆向き：f← := (A+iX);[(f+iA);(B+σX,A)]†
- 定義：f*>0 := [f;Δ]†
- 逆向き： f† := (iA+X);[(!A+X);f]*>0;(A+!X)
赤い斜線は打ち消し線で、打ち消された部分はナカッタコトにされます。ほんとに消してしまうと、自明な絵になります。
定義：f† := [∇;f]←
逆向き：f← := (A+iX);[(f+iA);(B+σX,A)]†
定義：f*>0 := [f;Δ]†
逆向き： f† := (iA+X);[(!A+X);f]*>0;(A+!X)
