日記 (2020 年 4 月 6 日)
4 月 5 日の続き。
前回は、 Bierman による線型圏と Seely によるモデル (を修正したもの) の関係について述べたが、 今回は Lafont†2 によって提案されたモデルとの関係について述べる。
モデルの定義に入る前に、 コモノイドについて復習しておこう。
定義 3.1.
対称モノイダル圏 において、 対象 A に 2 つの射 dA:A→A⊗A,eA:A→⊤ が定まっていて、
A⊗AAA⊗A(A⊗A)⊗AA⊗(A⊗A)dA⊗iddAdAid⊗dA A⊤⊗AA⊗AA⊗⊤dAeA⊗idid⊗eAAA⊗AAA⊗AdAdA
が全て可換であるとき、 組 (A,dA,eA) を可換コモノイド (commutative comonoid) という。
なお、 最後の図式の右側の垂直な射は、 テンソル積の左右を入れ替える同型射である。
それ以外のラベルのない射は、 対称モノイダル圏に定まる構造射が誘導する同型射である。
定義 3.2.
対称モノイダル圏 において、 可換コモノイド (A,dA,eA),(B,dB,eB) をとる。
射 f:A→B が、
ABA⊗AB⊗BfdAdBf⊗fAB⊤⊤feAeB
をともに可換にするとき、 f を可換コモノイドの射 (commutative comonoid morphism) という。
対称モノイダル圏 上の可換コモノイドとその間の射は圏を成すので、 これを Comon() で表す。
すると、 忘却関手 U:Comon()→ が構成できる。
Lafont が提案した線型論理のモデルは、 この忘却関手に右随伴関手が存在することを課したものである。
定義 3.3.
対称モノイダル圏 について、 忘却関手 U:Comon()→ に右随伴関手 G:→Comon() が存在するとする。
このとき、 を Lafont 圏 (— category) という。
一般に、 忘却関手の右随伴関手の像は余自由対象と呼ばれるので、 Lafont 圏とは任意の対象が余自由可換コモノイドを生成する圏であると言い換えることができる。
さて、 今後の議論のため、 随伴 U⊣G の余単位 ε がもつ普遍性についてここに書き下しておく。
対象 A と可換コモノイド (B,dB,eB) をとり、 射 f:A→B を考える。
すると、
BGAAfεAg
を可換にするような可換コモノイドの射 g:B→GA が一意に存在する。
これは、 随伴による全単射
Hom(U(B,dB,eB),A)≅HomComon()((B,dB,eB),GA)
によって、 右辺の集合の元である f と対応する左辺の集合の元である。
Lafont 圏の定義は非常にシンプルだが、 これだけで線型圏に必要な構造が全て誘導される。
証明.
随伴 U⊣G の単位と余単位をそれぞれ η と ε で表し、 δ:=U∗η∗G とおく。
また、 !:=U∘G とおく。
各対象 A に対し、 GA は定義から可換コモノイドであり、 その台対象は UGA すなわち !A である。
したがって、 そこに定まっている 2 つの構造射は dA:!A→!A⊗!A,eA:!A→⊤ で表せる。
対象 A,B に対し、
d!A⊗!B := ❲!A⊗!B(!A⊗!A)⊗(!B⊗!B)(!A⊗!B)⊗(!A⊗!B)dA⊗dB❲ e!A⊗!B := ❲!A⊗!B⊤⊗⊤⊤eA⊗eB❲
とおくと、 (!A⊗!B,d!A⊗!B,e!A⊗!B) は可換コモノイドになる。
したがって、 余単位の普遍性により、
!A⊗!B!(A⊗B)A⊗BεA⊗εBεA⊗BφAB
を可換にする射 φAB:!A⊗!B→!(A⊗B) が存在して、 これは可換コモノイドの射になっている。
また、 同様にして、
⊤!⊤⊤ε⊤φ
を可換にする射 φ:⊤→!⊤ も存在して、 これは可換コモノイドの射である。
これら 2 種類の射は、 ! にモノイダル関手の構造を定める。
以上によって定まった (!,φ,φ,δ,ε,d,e) は線型圏の公理を満たす。
これは簡単な計算によって確かめられる。
参考文献
- G. M. Bierman (1993) 「On intuitionistic linear logic」 Ph. D. thesis, The University of Cambridge
- Y. Lafont (1988) 「Logiques, catégories et machines」 Ph. D. thesis, Université de Paris VII