日記 (2020 年 10 月 11 日)
4 月 8 日には Chu 構成を導入し、 それがスター自律圏になること、 すなわち線型論理の否定演算子に対応する演算を定められることを示した。
したがって、 さらにこれが線型圏の構造をもってくれれば非常に嬉しいのだが、 実は Chu 構成のベースとなる圏に多少の条件を課せばそれが可能であることが Barr†1 によって知られている。
この証明は以下の 3 ステップから成る。
- ベースとなる圏上に余自由前コモノイドが存在することを示す。
さらに、 自由前コモノイドによるスライス圏上に (特定の演算を入れると) 自由前モノイドが存在することを示す。
- 上記の結果を組み合わせることで、 Chu 構成上に余自由前コモノイドを構成する。
- 余自由前コモノイドの部分対象として余自由コモノイドを構成する。
定理 3.4 によって余自由コモノイドが存在すれば線型圏になるので、 これによって Chu 構成に線型圏の構造が定められたことになる。
今日は、 この 2 ステップ目の詳細をまとめようと思う。
まず、 上記の説明で出てきた前コモノイドを定義する。
これは普通のコモノイドから結合性や単位性の条件を除いたもので、 以下のように定義される。
定義 5.1.
圏 に関手 ⊗:×→ と対象 ⊤ が定まっているとする。
対象 A に 2 つの射 d:A→A⊗A,e:A→⊤ が単に定まっているとき、 組 (A,d,e) を 「前コモノイド (precomonoid)」 という。
前モノイドはこの双対概念である。
上の前コモノイドが成す圏を PComon() と書き、 前モノイドが成す圏を PMon() と書くことにする。
さて、 Chu 構成を考えるため、 引き戻しをもつモノイダル閉圏 とその対象 ⫫ を固定する。
上の前コモノイド (A,d,e) をとり、 記号の簡単のため A⫫:=A⊸⫫ と書くことにする。
このとき、 Chu(,⫫) に定まっているテンソル積を使うことで、 スライス圏 /A⫫ 上に新たな演算を定義することができる。
Chu(,⫫) の 2 つの対象で第 1 成分が A のもの (A,A,a),(A,B,b) をとる。
この 2 つの対象のテンソル積を考えると、 その第 1 成分は単純に A⊗A であり、 その第 2 成分は A∗AB と書くことにすれば、
A∗ABA⊸AA⊸B(A⊗A)⊸⫫ab
という引き戻しによって定まるのであった。
この図式の等しい合成を x♯:A∗AB→(A⊗A)⊸⫫ と書く。
さて、 今は A に前コモノイドの構造 (A,d,e) が定まっているとしているので、 特に射 d:A→A⊗A が定まっている。
すると、 合成
A∗AB(A⊗A)⊸⫫A⊸⫫x♯d⊸⫫
が考えられる。
さて、 Chu(,⫫) の対象 (A,A,a) とは、 の 2 つの対象 A,A と射 a:A⊗A→⫫ の組であった。
テンソル積の転置によって、 この射 a はその転置 a♯:A→A⊸⫫ と 1 対 1 に対応する。
すなわち、 これによって Chu(,⫫) の対象 (A,A,a) は /A⫫ の対象 (A,a♯) と 1 対 1 に対応する。
以上のことを踏まえると、 上記の議論は全て /A⫫ における話に言い換えることができる。
すなわち、 /A⫫ の 2 つの対象 (A,a♯),(B,b♯) をとると、 ここから別の /A⫫ の対象 (A∗AB,(d⊸⫫)∘x♯) を定義できるということである。
これは、 /A⫫ の対象上に二項演算
∗A: /A⫫×/A⫫ ⟶ /A⫫ ((A,a♯),(B,b♯)) ⟼ (A∗AB,(d⊸⫫)∘x♯)
が定まったということであり、 さらに定義からこれは自然に関手になる。
さらに、 射 e:A→⊤ も定まっているから、 合成
⫫⊤⊸⫫A⊸⫫e⊸⫫
を考えることができ、 これによって /A⫫ の対象 (⫫,e⊸⫫) が得られる。
以上によって、 /A⫫ 上には演算 ∗A と対象 (⫫,e⊸⫫) が定まっていることになるので、 これらに関する前モノイドを考えることができる。
なお、 ここで注意しなければならないのは、 この演算 ∗A が一般には結合的でも単位的でもないという点である。
したがって、 ∗A に関する前モノイドを考えることはできるが、 ∗A に関するモノイドを考えることはできない。
次に、 Chu(,⫫) 上の前コモノイドについて考えよう。
これは、 Chu(,⫫) の対象 (A,A,a) に対し、 Chu(,⫫) における 2 つの射
d: (A,A,a) → (A,A,a)⊗(A,A,a) e: (A,A,a) → (⊤,⫫,λ⫫)
が定まったものであった。
Chu(,⫫) の射の定義によって、 これらを与えることは、 における 4 つの射
d: A → A⊗A m: A∗AA → A e: A → ⊤ u: ⫫ → A
であって、
A⊗(A∗AA)A⊗A(A⊗A)⊗(A∗AA)⫫d⊗idid⊗maxA⊗⫫A⊗A⊤⊗⫫⫫e⊗idid⊗ua
を可換にするものを与えることと同値である。
テンソル積の転置によって、 この 2 つの可換性は、
A∗AAA(A⊗A)⊸⫫A⊸⫫mx♯d⊸⫫a♯⫫A⊤⊸⫫A⊸⫫ue⊸⫫a♯
の可換性と同値である。
ここで、 A∗AA はこの左側の図式の左側の射によって /A⫫ の対象と見なしていたことを思い出すと、 左側の図式の可換性は m:(A,a♯)∗A(A,a♯)→(A,a♯) が /A⫫ の射になっていることを意味している。
同様にして、 右側の図式の可換性は u:(⫫,e⊸⫫)→(A,a♯) が /A⫫ の射になっていることを意味する。
すなわち、 ((A,a♯),m,u) は /A⫫ の前モノイドである。
以上の観察から、 次の命題が得られる。
命題 5.2.
引き戻しをもつモノイダル閉圏 とその対象 ⫫ をとり、 忘却関手 Z:PComon(Chu(,⫫))→PComon() を考える。
このとき、 任意の PComon() の対象 (A,d,e) に対し、 圏同型
Z−1(A,d,e)≅PMon(/A⫫)∘
が成立する。
これは次のように初等的に述べることもできる。
すなわち、 対象について、
- 上の前コモノイド (A,d,e) および /A⫫ 上の前モノイド ((A,a♯),m,u) の組を 1 つ与える。
- Chu(,⫫) 上の前コモノイド ((A,A,a),(d,m),(e,u)) を 1 つ与える。
は同じことである。
また、
- 上の前コモノイド (A,d,e) に対し、 /A⫫ 上の前モノイドの射 f:((B,b♯),m,u)→((A,a♯),m,u) を 1 つ与える。
- Chu(,⫫) 上の射 (id,f):((A,A,a),(d,m),(e,u))→((A,B,b),(d,m),(e,u)) を 1 つ与える。
は同じことである。
さて、 我々の目標は、 忘却関手 U:PComon(Chu(,⫫))→Chu(,⫫) の右随伴関手を構成することである。
実は今までの議論によって、 これを構成するという作業は、 忘却関手 V:PComon()→ の右随伴関手を構成するという作業と、 の各前コモノイド (A,d,e) に対して忘却関手 WA:PMon(/A⫫)→/A⫫ の左随伴関手を構成するという作業の、 2 ステップに分割することができる。
実際、 次の定理が成り立つ。
定理 5.3.
引き戻しをもつモノイダル閉圏 とその対象 ⫫ をとり、 2 条件
- 忘却関手 V:PComon()→ の右随伴関手 R:→PComon() が存在する。
- の各前コモノイド (A,d,e) に対し、 忘却関手 WA:PMon(/A⫫)→/A⫫ の左随伴関手 LA:/A⫫→PMon(/A⫫) が存在する。
が成り立っているとする。
このとき、 忘却関手 U:PComon(Chu(,⫫))→Chu(,⫫) の右随伴関手が存在する。
証明.
以降、 :=Chu(,⫫) とおき、 の対象 (A,A,a) を任意にとる。
まず RA=:(X,d,e) と書けば、 随伴 V⊣R の余単位から の射 ξ:X→A がとれる。
さらにこれを用いて LRA(A,ξ⫫∘a♯)=:((X,x♯),m,u) と書けば、 同様に随伴 LRA⊣WRA の単位から /X⫫ の射 ξ:(A,ξ⫫∘a♯)→(X,x♯) がとれる。
任意に PComon() の対象 ((B,B,b),(d,m),(e,u)) および の射 (f,f):(B,B,b)→(A,A,a) をとる。
このとき、
(B,B,b)(X,X,x)(A,A,a)(f,f)(ξ,ξ)(g,g)
を可換にするような PComon() の射 (g,g):((B,B,b),(d,m),(e,u))→((X,X,x),(d,m),(e,u)) が唯一存在することを示せば良い。
実際、 そうすれば
Ω: Chu(,⫫) ⟶ PComon(Chu(,⫫)) (A,A,a) ⟼ ((X,X,x),(d,m),(e,u))
が求めたい右随伴関手を与える。
まず、 の射 f:B→A があるから、 ξ の普遍性によって、
BXAfξg
を可換にする PComon() の射 g:(B,d,e)→(X,d,e) が唯一存在する。
ここで、 での引き戻し
YX⫫BB⫫py♯g⫫b♯
を計算すると、 での押し出し
(B,B⫫,εB)(B,B,b)(X,X⫫,εX)(X,Y,y)(g,g⫫)(id,b♯)(g,p)(id,y♯)
が得られる。
ところが、
(g,g⫫): ((B,B⫫,εB),(d,d⫫),(e,e⫫)) ⟶ ((X,X⫫,εX),(d,d⫫),(e,e⫫)) (id,b♯): ((B,B⫫,εB),(d,d⫫),(e,e⫫)) ⟶ ((B,B,b),(d,m),(e,u))
はともに PComon() の射でもある。
忘却関手 U:PComon()→ は余極限を生成することは容易に分かるから、 これより上の図式が PComon() の可換図式になるような (X,Y,y) 上の前コモノイドの構造が唯一定まる。
その構造を ((X,Y,y),(d,m),(e,u)) と書く。
すなわち、 PComon() での押し出し
((B,B⫫,εB),(d,d⫫),(e,e⫫))((B,B,b),(d,m),(e,u))((X,X⫫,εX),(d,d⫫),(e,e⫫))((X,Y,y),(d,m),(e,u))(g,g⫫)(id,b♯)(g,p)(id,y♯)
を得た。
ここで、 この下側の水平な射に注目すると、 その第 1 成分は恒等写像だから、 d=d および e=e が分かる。
さて、 引き戻しの普遍性によって、
AA⫫YX⫫BB⫫py♯g⫫b♯fa♯ξ⫫q
を可換にする の射 q:A→Y が存在する。
この図式の平行四辺形部分の可換性によって、 これは /X⫫ の射 q:(A,ξ⫫∘a♯)→(Y,y♯) とも見なせる。
すると、 ξ の普遍性によって、
(A,ξ⫫∘a♯)(X,x♯)(Y,y♯)ξqr
を可換にする PMon(/X⫫) の射 r:((X,x♯),m,u)→((Y,y♯),m,u) が存在する。
命題 5.2 によって、 これは PComon() の射
(id,r):((X,Y,y♯),(d,m),(e,u))⟶((X,X,x♯),(d,m),(e,u))
がとれたということである。
すると、 PComon() の射
(id,r)∘(g,p):((B,B,b),(d,m),(e,u))⟶((X,X,x),(d,m),(e,u))
が得られ、 この合成を (g,g) と書くことにすれば、
(B,B,b)(X,X,x)(A,A,a)(f,f)(ξ,ξ)(g,g)
は可換である。
このような射の一意性は、 議論の途中でとった射の一意性から従う。
参考文献
- M. Barr (1990) 「Accessible categories and models of linear logic」 『Journal of Pure and Applied Algebra』 69:219–232