セリンガーのND補題

セリンガー（Peter Selinger）が"Categorical Structure of Asynchrony"（→http://www.mathstat.dal.ca/~selinger/papers/catasynch.pdf）で示しているのだが、面白い補題がある。

(C, ×, Tr, Δ)を対角付きトレース付き（対称モノイド）圏だとして、そのベキ構成（木下の定義と同じだが、空集合は除く）をC^ndとする。ndは非決定性を表す。×、Tr、Δを自明に拡張する。その結果である(C, ×, Tr, Δ)もまたC^ndと書く。

• F×G = {f×g | f∈F, g∈G}
• Tr(F) = {Tr(f) | f∈F}
• Δ_X = {Δ_X}

セリンガー曰く：

Surprisingly, this simple-minded construction actually preserves the structure of C.

次が成立する。

1. C^ndは対角付きトレース付き圏である。
2. 標準的な埋め込みC→C^ndによりC⊆C^ndと考えるとして、(C^nd)^# = C^# である。(-)^#は焦点部分圏。つまり、焦点は不変となる。
3. Cがデカルトのとき、C^ndの射はすべてトータル射（破棄可能）となる。
4. Cがデカルトであり一様性を持つ（uniformly traced）のとき、C^ndも一様性を持ち、一様射のクラスはCのそれと一致する。

一様トレース（trace with uniformity, uniform trace）を持つデカルト圏（Uniformly traced Cartesian category）Cでは、ベキ構成をしても、焦点（C自身）は不変で、一様射（uniform morphism）のクラスも不変であり、非決定性（コピー不可）が導入されるが全域性（トータリティ）は保存される。

ついでに、引用によってセリンガーの用語法を示す。

For a given traced monoidal category C, fix a monoidal subcategory of uniform morphisms. This subcategory should include at least all isomorphisms, the diagonals, and the weak initial and terminal morphisms. Uniformity of the trace operator is defined with respect to this notion of uniform morphism:

Definition 3.8 (Hasegawa [7]) Given a traced monoidal category with diagonals, we say that the trace is uniform if for all morphisms f ...[省略]

... uniform traces correspond to uniform fixpoint operators.

参考：

• セリンガーの論文 - 檜山正幸のキマイラ飼育記 メモ編
• トレース付きモノイド圏の対角、一様性など - 檜山正幸のキマイラ飼育記 メモ編