トレース付きモノイド圏の対角、一様性など
セリンガー(Peter Selinger)の"Categorical Structure of Asynchrony"(→http://www.mathstat.dal.ca/~selinger/papers/catasynch.pdf)から、いくつかの概念:
対称モノイド圏Cが|C|でインデックスされた族ΔA:A→A×A、◇A:A→Iを持ち、Aに対してΔAと◇Aが対称(可換)コモノイドになっているとき、(C, Δ, ◇)を対角付き(対称)モノイド圏(monoidal category with diagonals)と呼ぶ。◇を弱終射(weak terminal morphism)と呼ぶことがある。
f;Δ = Δ;(f×f)を満たす射fをコピー可能(copyable)、f;◇= ◇を満たす射を破棄可能(discardable)と呼ぶ。コピー可能射、破棄可能射の全体はそれぞれ部分圏をなす。コピー可能かつ破棄可能な射からなる部分圏を対角付きモノイド圏の焦点(focus)と呼ぶ。焦点に入る射は焦点的(focal)と呼ぶ。焦点部分圏は、対角付きモノイド圏に対してのみ定義できる。
トレース付きモノイド圏でありかつ対角を持つ圏Cを考える。Tr(ΔA)を弱始射(weak initial morphism)と呼び、□Aと書く。□;f = □である射を厳密射(strict)と呼ぶ。厳密射の全体も部分圏となる。
トレース付き対角付きモノイド圏Cに部分(対称)モノイド圏Uが指定されていて、Uは次に性質を持つとする。
- |U| = |C|
- すべての同型はUに属する。
- すべての対角、弱終射、弱始射はUに属する。
次に性質を持つとき、トレースは一様である、あるいは(C, U)が一様トレース付きモノイド圏(uniformly traced - )と呼ぶ。
- あるh∈Uに対して f;(id×h) = (id×h);g ならば、Tr(f) = Tr(g)
長谷川さんは、Uが圏になる必要はないし、圏にならない例もあることを強調している。よって、Uは単なる射の族としていいだろう。
また、長谷川さんのstrictの定義はセリンガーと違っていて、一様性原理が成立する射を厳密と呼んでいる。例えば、「同型は厳密」という定理がある。
セリンガーの意味の厳密は、保存的とか保守的と呼んで、長谷川さんの意味の厳密は一様または酵素的(enzymatic)がいいと思う。