モノイダル閉圏における指数随伴系の自然性

というかページをダイエットさせたい

モノイダル閉圏における指数随伴系の自然性#60ca10ff6115420000d6fe4f

目的

モノイダル閉圏における指数随伴系$ \Sigma_L[A]=\left\lang A\otimes \_ \dashv A⊸\_ ,{}^A\mathrm{unit} ,{}^A\mathrm{eval} \right\rang の自然性をちゃんと考える

単位、余単位、カリー化自然同型

dragoon8192.icon右にしといた方が図が素直だったかもしれんな……

code:sig

Adjunction

Cat Cat

A.&prod A.&hom

A.&unit A.&eval

前提

例としてデカルト閉圏 $ \mathbf{Cat} as %

左強モノイダル閉圏として扱う

デカルト積の対称性は使わない

Catの埋め込み先&

こっちは右強モノイダル閉圏として

dragoon8192.icon& = CATだと大きすぎ？

Catとその仲間たちだけの圏でよさそう

Catから生成されるモノイダル閉圏？

指標の接頭記号別名

code:sig

% = L-S-C-MC Cat %× %I %⊸

& = R-S-C-MC ??? &× &I &⟜

指数随伴対 $ A.\mathrm{prod} \dashv A.\mathrm{hom}

Cat P-1図式

https://gyazo.com/ab40fee2bbbbb4194c83e34b668829b6

code:ExpAdj.sig

&1-morph

A.&prod = (A×_) : Cat &-> Cat

A.&hom = A,_ : Cat &-> Cat

モノイダル積

左から掛けているやつ

$ (×)\colon \mathrm{Cat} × \mathrm{Cat} → \mathrm{Cat}

左内部hom函手

左指数函手

$ [,] = (⊸) \colon \mathrm{Cat}^\mathrm{op}× \mathrm{Cat} \to \mathrm{Cat}

$ [A,B] = A⊸B

code:ExpAdj.sig

&1-morph

(%×) = \A B -> A %× B

: Cat &× Cat &-> Cat

(%⊸) = %_,_ = \A B -> A %⊸ B

: Cat^{op} &× Cat &-> Cat

こいつらを一つ上(&)から右カリー化する

code:ExpAdj.sig

&1-morph

prod = (%×)&∩ = \A ->(\B -> A × B)

: Cat &-> (Cat &⟜ Cat)

hom = (%⊸)&∩ = \A ->(\B -> A ⊸ B)

: Cat^{op} &-> (Cat &⟜ Cat)

単位、余単位

$ {^A}\mathrm{unit} \colon (\_) ⇒ A⊸(A×\_)

$ {^A}\mathrm{eval}\colon A×(A⊸\_)⇒(\_)

Cat P-1図式

https://gyazo.com/07457a8fd92759138f06cd61e9ab4092

& 1-2図式

https://gyazo.com/ce5295a94f0706d0e6ef86d95485018f

code:ExpAdj.sig

&1-morph

&2-morph

A.unit : Cat^ &=> A,(A×_)

A.eval : A × A,_ &=> Cat^

: Cat &-> Cat

where

(*) = (&1)

A,(A×_) = A.prod * A.hom

A × A,_ = A.hom * A.prod

これで随伴系の材料が揃った

code:sig

Adjunction

Cat Cat

A.prod A.hom

A.unit A.eval

ニョロニョロ公理

snaky

またこれはニョロニョロしてる

code:ExpAdj.sig

Axioms

&3-eq snaky-1:

A.unit * A.prod^ ; A.prod^ * A.eval

== A.prod^

: A.prod => A.prod

&3-eq snaky-2:

A.hom^ * A.unit ; A.eval * A.hom^

== A.hom^

: A.hom => A.hom

where

(*) = (&1), (;) = (&2), (^) = (&^)

Cat P-1図式

https://gyazo.com/28a64fd951906c26360d8b463252b2d9https://gyazo.com/3fcdab32f0234b6dcef56ea35c1c9514

& 1-2図式

https://gyazo.com/3ff7dbf9592ddbcfe10938b148010202https://gyazo.com/1f8a70913ea389d224b7fdecca465222

dragoon8192.icon左右逆になっちゃうけど、紛らわしくなくて逆にいいかな……？

自然性

単位と余単位のI-スライダー性

成分Bについては自然変換なので

自然変換のエレベーター性がそのまま

Cat P-1図式

https://gyazo.com/ceac3ae5f7f2748d0094c79d7183e34ahttps://gyazo.com/2545c6d19e8b9dfc0e0b4eca42853e46

code:I-slider.sig

%1-morph

G: B -> B'

G.A.unit

== B.A.unit ; A,(A×G)

== G ; B'.A.unit

G.A.eval

== B.A.eval ; G

== (A×A,G) ; B'.A.eval

where

(;) = (%1)

いつもは*にしてる函手の結合だけど、今回はCatが最下層なのでこうした方が見やすい

& 1-2図式

https://gyazo.com/a5e37f7622cd0a6c10422747da70920dhttps://gyazo.com/db8e0b297a4e3d98bbd6b7a329bfaa52

単位の∩-スライダー性と余単位の∪-スライダー性

dragoon8192.iconなんの自然性というべきか

左内部hom函手の構成から自動的に導かれる

reference.icon ラムダ計算の自然性とお絵描き - 檜山正幸のキマイラ飼育記 (はてなBlog)

Cat P-1図式

https://gyazo.com/e64e5e5a0503c5fbb5de38f34e2e5b48https://gyazo.com/8af5f69b5dbf7880bc6907bebd5cfaf9

code:U-slider.sig

F : A %-> A'

&3-eq

F.unit : Cat^ &=> A,(A'×_)

:= A.unit; A,(F×_)

== A'.unit; F,(A'×_)

F.eval : A × A',_ &=> Cat^

:= (A×F,_); A.eval

== (F×A',_); A'.eval

where

(*) = (&1), (;) = (&2)

指数随伴系は自己函手圏における双対系

左カリー化自然同型

$ {^A}\Lambda \colon \mathbf{Cat}[A×\_,\_] \Rightarrow \mathbf{Cat}[\_,A⊸\_]

$ {^∩}P=P.{^A}\Lambda^B_{B'} = {^A}\mathrm{unit}_{B};(A⊸P)

$ {_∪}Q=Q.({^A}\Lambda^B_{B'})^{-1} = (A×Q);{^A}\mathrm{eval}_{B'}

where

$ P : A×B→B'

$ Q : B→A⊸B'

内部homでやってみる

Cat P-1図式

https://gyazo.com/c692a74d361ef5c0cf4d5ba39328cc02 https://gyazo.com/fc7d8bcfcf57e20ecfd0f7e551911273 https://gyazo.com/1da1a69699623fb672e69597e9350e90

code:curry.sig

&2-iso

A.%ΛL : (A×_)⊸_ &=> _⊸(A⊸_)

: Cat^{op} &× Cat &-> Cat

%1-iso

(B,B').A.%ΛL : (A×B)⊸B' %-> B⊸(A⊸B')

%1-morph

P : A×B -> B'

Q : B -> A⊸B'

∩P = P.(B,B').A.%ΛL

= B.A.unit %1 P.A.hom

: B -> A⊸B'

∪Q = Q.(B,B').A.%ΛL^{-1}

= Q.A.prod %1 B.A.eval

: A×B -> B'

うまくいかない……

随伴系のなす圏への函手にしたかった

しかしスライディングの同値が噛み合わない

付録

計算途中に使ったやつ

code:ExpAdj.sig

%0-morph

A, B

A %⊸ B , A %× B

&0-morph

Cat(%)

$ [F,G] : [A',B] → [A,B']

where

$ F\colon A→A' $ G\colon B→B'

想定される成分は$ \colon H \mapsto F;H;G

https://gyazo.com/4c65dae3c90e0a16d099b756e4c74775

https://gyazo.com/be4b82c9eeeb74d3f293cc2b474d69de

code:スライディング.sig

&2-morph

A.unit : Cat^ &=> A,(A×_)

A.eval : A × A,_ &=> Cat^

A,(F×_) = (F.prod) * (A.hom)

: A,(A×_) &=> A,(A'×_)

F,(A'×_) = (A'.prod) * (F.hom)

: A',(A'×_) &=> A,(A'×_)

A × F,_ = (F.hom) * (A.prod)

: A × A',_ &=> A × A,_

F × A',_ = (A'.hom) * (F.prod)

: A × A',_ &=> A' × A',_

https://gyazo.com/5312fcdd91c468ae4d4c364b075f0855

https://gyazo.com/50f0be8854d3855dfee595627fdeab2c

code:sig

CatA×B,B' = (A×B)⊸B'

CatB,A×B' = B⊸(A⊸B')