日記 (2021 年 6 月 7 日)

Girard†4 によって線型論理が導入されて以来、その圏論的意味論も様々な点から研究されてきた。その最も基本的な結果として、 (指数的演算子を除いた) 古典線型論理に対応する圏論的構造はスター自律圏であるということが知られている。すると、そこから自然に生まれるのが、スター自律圏はどのような場面で現れるのか、すなわちスター自律圏の具体例やスター自律圏の構成方法にはどんなものがあるのかという疑問がある。

スター自律圏を構成する一般的な方法はいくつか知られており、その中で代表的なものとして、 Chu†1 による Chu 構成と de Paiva†3 によるダイアレクティカ圏がある。 Chu 構成は、名前の通り Chu†1 によって導入された構成方法で、まさにスター自律圏を構成する方法として考えられた。ダイアレクティカ圏は、 de Paiva†3 によって導入された構成方法で、 Gödel†5 が考案したダイアレクティカ解釈を圏論的に再構築することで得られたものである。この 2 つの構成方法は様々な点で似通ってはいるものの、モノダイル構造の定義が両者で少し異なっており、両者を統一して扱うことはそれほど単純ではなかった。

Shulman†7 は、 Chu 構成とダイアレクティカ圏が特殊な場合として出現するような非常に一般的な枠組みを構築することで、この問題を解決した。この研究における主なアイデアは、モノイダル構造が異なるのが難点なのだから、モノイダル構造が存在する必要のない一般的な状況の上でまずは考え、モノイダル構造をそこから何らかの普遍性によって取り出そうというものである。そこで Shulman が用いたのが、 Szabo†8 の多圏である。多圏とは、通常の圏における射の始域と終域を単一の対象ではなく対象の有限列に一般化したものである。

この日記シリーズでは、 Shulman によるこの結果の概略を何回かに分けてまとめるつもりである。なお、一部の記号類は、このサイトの他のページで使われているものとの整合性をとるため、オリジナルのものから変更してある。

今回は、多圏の定義を復習し、それ上のテンソル積や内部冪を定義し、モノイダル閉圏やスター自律圏との関係を見る。以下、単に列と言ったら有限列のことを指し、要素を列挙するときは山括弧で囲んで表すことにする。また、複数の有限列の連結は単にコンマで繋げて書くことで表す。

定義 1.1.

以下のデータが定まっているとする。

集まり Ob(󰒚) が定まっている。この元を 󰒚 の対象 (object) という。
󰒚 の対象列 ⟨Γ⟩,⟨Δ⟩ に対し、集合 Hom󰒚(Γ∣Δ) が定まっている。この元を 󰒚 の多射 (polymorphism) といい、 f:⟨Γ⟩→⟨Δ⟩ のように表す。
󰒚 の対象 A に対し、元 idA∈Hom󰒚(A∣A) が定まっている。これを 󰒚 における A 上の恒等射 (identity) という。
󰒚 の対象列 ⟨Γ⟩,⟨Δ⟩,⟨Δ󰎘⟩,⟨Λ⟩,⟨Λ󰎘⟩,⟨Σ⟩ および対象 A に対し、写像 Hom󰒚(Γ∣Δ,A,Δ󰎘)×Hom󰒚(Λ,A,Λ󰎘∣Σ) ⟶ Hom󰒚(Λ,Γ,Λ󰎘∣Δ,Σ,Δ󰎘) (f,g) ⟼ f󰖡Ag が定まっている。これを 󰒚 の合成 (composition) という。
󰒚 の対象列の置換 σ:⟨Γ󰎘⟩→⟨Γ⟩,τ:⟨Δ⟩→⟨Δ󰎘⟩ に対し、写像 Hom󰒚(Γ∣Δ) ⟶ Hom󰒚(Γ󰎘∣Δ󰎘) f ⟼ σ·f·τ が定まっている。これを 󰒚 の交換 (exchange) という。

これらのデータは、次の条件を満たすとする。

多射 f:⟨Γ,A,Γ󰎘⟩→⟨Δ⟩ に対し、 idA󰖡Af=f
多射 f:⟨Γ⟩→⟨Δ,A,Δ󰎘⟩ に対し、 f󰖡AidA=f が成り立つ。
多射 f:⟨Γ⟩→⟨Δ⟩ に対し、 id⟨Γ⟩·f·id⟨Γ⟩=f が成り立つ。
多射 f:⟨Γ⟩→⟨Δ⟩ および対象列の置換 σ:⟨Γ󰎘⟩→⟨Γ⟩, σ󰎘:⟨Γ󰎙⟩→⟨Γ󰎘⟩, τ:⟨Δ⟩→⟨Δ󰎘⟩, τ󰎘:⟨Δ󰎘⟩→⟨Δ󰎙⟩ に対し、 σ󰎘·(σ·f·τ)·τ󰎘=(σ󰎘󰖡σ)·f·(τ󰖡τ󰎘) が成り立つ。
多射 f:⟨Γ⟩→⟨Δ,A,Δ󰎘⟩, g:⟨Λ,A,Λ󰎘⟩→⟨Σ,B,Σ󰎘⟩, h:⟨Φ,B,Φ󰎘⟩→⟨Ψ⟩ に対し、 (f󰖡Ag)󰖡Bh=f󰖡A(g󰖡Bh) が成り立つ。
多射 f:⟨Γ⟩→⟨Δ,A,Δ󰎘,B,Δ󰎙⟩, g:⟨Λ,A,Λ󰎘⟩→⟨Σ⟩, h:⟨Φ,B,Φ󰎘⟩→⟨Ψ⟩ および対象列の置換 σ:⟨Φ,Λ,Γ,Λ󰎘,Φ󰎘⟩→⟨Λ,Φ,Γ,Φ󰎘,Λ󰎘⟩ に対し、 (f󰖡Ag)󰖡Bh=σ·((f󰖡Bh)󰖡Ag) が成り立つ。
多射 f:⟨Γ⟩→⟨Δ,A,Δ󰎘⟩, g:⟨Λ⟩→⟨Σ,B,Σ󰎘⟩, h:⟨Φ,A,Φ󰎘,B,Φ󰎙⟩→⟨Ψ⟩ および対象列の置換 σ:⟨Σ,Δ,Ψ,Δ󰎘,Σ󰎘⟩→⟨Δ,Σ,Ψ,Σ󰎘,Δ󰎘⟩ に対し、 f󰖡A(g󰖡Bh)=(g󰖡B(f󰖡Ah))·σ が成り立つ。
多射 f:⟨Γ⟩→⟨Δ,A,Δ󰎘⟩, g:⟨Λ,A,Λ󰎘⟩→⟨Σ⟩ および対象列の置換 σ:⟨Γ󰎘⟩→⟨Γ⟩, τ:⟨Δ,A,Δ󰎘⟩→⟨Φ,A,Φ󰎘⟩, λ:⟨Ψ,A,Ψ󰎘⟩→⟨Λ,A,Λ󰎘⟩, μ:⟨Σ⟩→⟨Σ󰎘⟩ に対し、 (σ·f·τ)󰖡A(λ·g·μ)=(σ∥λ)·(f󰖡Ag)·(τ∥μ) が成り立つ。ここで、 σ∥λ:⟨Ψ,Γ󰎘,Ψ󰎘⟩→⟨Λ,Γ,Λ󰎘⟩, τ∥μ:⟨Δ,Σ,Δ󰎘⟩→⟨Φ,Σ󰎘,Φ󰎘⟩ はそれぞれ自然に定まる置換である。

このとき、 󰒚 を対称多圏 (symmetric polycategory) という。

上記定義で課されている条件により、ある多射から交換によって得られる多射はその始域と終域によってのみ決まり、交換は合成と両立している。したがって、交換によって移り変わる多射は全て同一視しても良く、置換は全て省略することにする。

対称多圏の間の射は、通常の圏の間の関手と同様に、以下のように定義される。

定義 1.2.

対称多圏 󰒚,󰒛 に対し、以下のデータが定まっているとする。

󰒚 の対象 A に対し、 󰒛 の対象 FA が定まっている。
󰒚 の多射 f:⟨Γ⟩→⟨Δ⟩ に対し、 󰒛 の多射 Ff:F⟨Γ⟩→F⟨Δ⟩ が定まっている。ここで、 F⟨Γ⟩, F⟨Δ⟩ はそれぞれ ⟨Γ⟩, ⟨Δ⟩ の各要素を F で移して得られる列である。

これらのデータは、次の条件を満たすとする。

󰒚 の対象 A に対し、 FidA=idFA が成り立つ。
󰒚 の多射 f:⟨Γ⟩→⟨Δ,A,Δ󰎘⟩, g:⟨Λ,A,Λ󰎘⟩→⟨Σ⟩ に対し、 F(f󰖡Ag)=Ff󰖡FAFg が成り立つ。
󰒚 の多射 f:⟨Γ⟩→⟨Δ⟩ および 󰒚 の対象列の置換 σ:⟨Γ󰎘⟩→⟨Γ⟩,τ:⟨Δ⟩→⟨Δ󰎘⟩ に対し、 F(σ·f·τ)=Fσ·Ff·Fτ が成り立つ。ここで、 Fσ, Fτ はそれぞれ σ, τ の始域と終域の列を F で移したものに置き換えて得られる置換である。

このとき、 F を対称多関手 (symmetric polyfunctor) といい、 F:󰒚→󰒛 で表す。

今後のため、いくつか用語を用意しておく。

定義 1.3.

多圏 󰒚 の多射 f:⟨Γ⟩→⟨Δ⟩ について、 #⟨Δ⟩=1 のときは f を特に複射 (multimorphism) という。また、 #⟨Γ⟩=#⟨Δ⟩=1 のときは f を単に射 (morphism) という。

定義 1.4.

多圏 󰒚 をとる。任意の 󰒚 の対象列 ⟨Γ⟩,⟨Δ⟩ について、 #⟨Δ⟩≠1 ならば Hom󰒚(Φ∣Δ)=∅ が成り立っているとする。このとき、 󰒚 を複圏 (multicategory) という。

定義から、複圏とは複射しか存在しない多圏のことであり、 Lambek†6 が導入した複圏と同じものになっている。また、射しか存在しない多圏、すなわち任意の対象列 ⟨Γ⟩,⟨Δ⟩ について #⟨Γ⟩≠1 かつ #⟨Δ⟩≠1 ならば Hom(Γ∣Δ)=∅ であるような多圏は、通常の意味での圏と同じものになる。この同一視により、通常の圏を多圏と見なすことができる。

多圏上においてテンソル積などの各種演算は次のように定義される。

定義 1.5.

対称多圏 󰒚 の対象 A,B をとる。

ある対象 A⊗B と多射 φAB:⟨A,B⟩→⟨A⊗B⟩ について、任意の対象列 ⟨Γ⟩,⟨Γ󰎘⟩,⟨Δ⟩ に対して、写像 Hom(Γ,A⊗B,Γ󰎘∣Δ) ⟶ Hom(Γ,A,B,Γ󰎘∣Δ) f ⟼ φAB󰖡A⊗Bf が同型射になるとする。このとき、 A⊗B を A と B のテンソル積 (tensor product) という。
ある対象 ⊤ と多射 φ⊤:⟨⟩→⟨⊤⟩ について、任意の対象列 ⟨Γ⟩,⟨Γ󰎘⟩,⟨Δ⟩ に対して、写像 Hom(Γ,⊤,Γ󰎘∣Δ) ⟶ Hom(Γ,Γ󰎘∣Δ) f ⟼ φ⊤󰖡⊤f が同型射になるとする。このとき、 ⊤ を単位 (unit) という。
ある対象 A⊕B と多射 ψAB:⟨A⊕B⟩→⟨A,B⟩ について、任意の対象列 ⟨Γ⟩,⟨Δ⟩,⟨Δ󰎘⟩ に対して、写像 Hom(Γ∣Δ,A⊕B,Δ󰎘) ⟶ Hom(Γ∣Δ,A,B,Δ󰎘) f ⟼ f󰖡A⊕BψAB が同型射になるとする。このとき、 A⊕B を A と B の余テンソル積 (cotensor product) という。
ある対象 ⊥ と多射 ψ⊥:⟨⊥⟩→⟨⟩ について、任意の対象列 ⟨Γ⟩,⟨Δ⟩,⟨Δ󰎘⟩ に対して、写像 Hom(Γ∣Δ,⊥,Δ󰎘) ⟶ Hom(Γ∣Δ,Δ󰎘) f ⟼ f󰖡⊥ψ⊥ が同型射になるとする。このとき、 ⊥ を余単位 (counit) という。
ある対象 A⊸B と多射 ξAB:⟨A⊸B,A⟩→⟨B⟩ について、任意の対象列 ⟨Γ⟩,⟨Δ⟩,⟨Δ󰎘⟩ に対して、写像 Hom(Γ∣Δ,A⊸B,Δ󰎘) ⟶ Hom(Γ,A∣Δ,B,Δ󰎘) f ⟼ f󰖡A⊸BξAB が同型射になるとする。このとき、 A⊸B を A と B の冪 (exponential) という。
ある対象 A⊥ と多射 ηA:⟨⟩→⟨A,A⊥⟩, εA:⟨A⊥,A⟩→⟨⟩ について、 ηA󰖡AεA=idA⊥ηA󰖡A⊥εA=idA がともに成り立つとする。このとき、 A⊥ を A の双対 (dual) という。

さらに、 󰒚 の任意の対象に対して上記の各演算が存在するとき、 󰒚 はその演算をもつ (has) という。

通常のモノイダル圏のモノイダル構造 (テンソル積と単位) は、台となる圏に対して追加の情報として与えられるものであり、台となる圏だけで定まるものではない。一方で、上で定義された対称多圏の各種演算は、存在すれば (同型の違いを除いて) 一意に定まるので、追加の情報というよりは性質である。

特定の演算をもつ対称複圏は、何らかの構造をもつ通常の圏と同一視できる。よく知られているのが、以下の対応である。

命題 1.6.

1 対 1 対応 {テンソル積, 単位をもつ対称複圏} ≅ {対称モノイダル圏} {テンソル積, 単位, 冪をもつ対称複圏} ≅ {対称モノイダル閉圏} {テンソル積, 単位, 余テンソル積, 余単位をもつ対称多圏} ≅ {線型分配圏} {テンソル積, 単位, 余テンソル積, 余単位, 双対をもつ対称多圏} ≅ {スター自律圏} が成立する。

証明.

Cockett–Seely†2 などを参照。

次回は、複圏上の加群を定義し、そこから新たな多圏が誘導されることを見る。

参考文献

P.-H. Chu (1978) 「Constructing ∗-autonomous categories」 Ph. D. thesis, McGill University
R. Cockett, R. Seely (1997) 「Weakly distributive categories」『Journal of Pure and Applied Algebra』 114(2):133–173
P. C. V. de Paiva (1991) 「The dialectica categories」 Ph. D. thesis, The University of Cambridge
J. Y. Girard (1987) 「Linear logic」『Theoretical Computer Science』 50:1–101
K. Gödel (1958) 「Über eine bisher noch nicht benützte Erweiterung des finiten Standpunktes」『Dialectica』 280–287
J. Lambek (1969) 「Deductive systems and categories II: standard constructions and closed categories」『Lecture Notes in Mathematics』 86:76–122
M. Shulman (2020) 「The 2-Chu-dialectica construction and the polycategory of multivariable adjunctions」『Theory and Applications of Categories』 35(4):89–136
M. E. Szabo (1975) 「Polycategories」『Communications in Algebra』 3(8):663–689