しつこくKozen圏

また、ふとコゥゼン（Kozen）圏について考えた。最近、定義はほぼ安定していて：

• トレース付き・ベキ等・双デカルト 圏

である。デカルト性は、対称モノイド構造×, 1と対角（余加法）Δ、放電（discharger；余単位）!で決まる。これは、すべての対象Aに可換余モノイド構造(A, Δ_A, !_A)を与える。余デカルト性はその双対で、余対角（加法）∇、単位（零）θで決まる。すべての対象Aに可換モノイド構造(A, ∇_A, θ_A)を与える。

デカルトかつ余デカルトであり双代数条件（bialgebra condition）∇;Δ = □ を満たすとき、双デカルトと呼ぶ。すべての対象Aが双モノイド（双代数）となる。さらに、Δ;∇ = 1 のとき（加法的）ベキ等と呼ぶ。以上で、ベキ等・双デカルト圏が定義できる。定義より、当然に対称モノイド圏である。定義より、双デカルト圏のモノイド積は双積である。

参考：

• 等式的双デカルト圏のための等式群 - 檜山正幸のキマイラ飼育記 メモ編
• トレース付きモノイド圏の対角、一様性など - 檜山正幸のキマイラ飼育記 メモ編

ベキ等・双デカルト圏が、その対称モノイド積＝双積に関してトレースを持っていると、これがコゥゼン（Kozen）圏である。コゥゼン圏の定義から、どれだけの事実が引き出せるか？ が課題。

とりあえず、コゥゼン圏のなかで行列スター公式を示したい。あと、トレースを使って、f^†、f⁺、f^*などに関する等式群を示したい。

参考：

• 圏のloopingと不動点 - 檜山正幸のキマイラ飼育記 メモ編
• Kleene代数の行列計算とトレース - 檜山正幸のキマイラ飼育記 メモ編

クリーネ・スターを*、第1行が(a, b)、第2行が(c, d)である2×2行列を[a b / c d]で示すことにする。行列A = [a b / c d]に対するスターの定義は、A* = [α β / γ δ] として：

• α = (a + bd*c)*
• β = αbd*
• γ = δca*
• δ = (d + ca*b)*

で与えられる。これが行列スター公式。