双対系

summary.icon

signature.icon

2-圏でないぶん、全体のランクが下がっている

code:Adjunction.sig

1-signature Dual in % = MonCAT C %× %i

Data

0-morph leftAdjoint @ l

0-morph rightAdjoint @ r

1-morph unit @ η

: %i -> l %× r

1-morph eval @ ε

: r %× l -> %i

Axioms

2-mon-eq snaky-1

: (η %× l^) %1 (l^ %× ε) => l^

: l -> l

2-mon-eq snaky-1

: (r^ %× η) %1 (ε %× r^) => r^

: r -> r

$ = \left\lang\mathrm{ Dual }\colon l, r ; \mathrm{unit}, \mathrm{eval}\right\rang

0-morph

左右はここで決めてしまう

随伴系と図式順で合わせた

1-morph

$ \mathrm{unit} \colon i → l\otimes r

$ \mathrm{eval}\colon r\otimes l → i

https://gyazo.com/0eb37db61288112f7968d55c5931f602

公理系

ニョロニョロ公理

$ \lambda_l^{-1}; \mathrm{unit} \otimes l^\wedge ; \alpha_{l,r,l}; l^\wedge \otimes \mathrm{eval};\rho_l=l^\wedge

$ \rho_r^{-1}; r^\wedge \otimes \mathrm{unit}; \alpha^{-1}_{r,l,r}; \mathrm{eval}\otimes r^\wedge ;\lambda_r = r^\wedge

用語

$ \exist \: \mathrm{LDuals} \colon |MC| → \mathbf{Dual} ( MC )

$ \mathrm{LDuals} * π_r = |MC|^\wedge

i.e.

$ b.\mathrm{LDuals} = \left\lang\mathrm{ Dual }\colon b^L, b ; \_, \_ \right\rang

$ \exist \: \mathrm{RDuals} \colon |MC| → \mathbf{Dual} ^ \mathrm{op} ( MC )

$ \mathrm{RDuals} * π_l = |MC|^\wedge

i.e.

$ a.\mathrm{RDuals} = \left\lang\mathrm{ Dual }\colon a, a^R ; \_, \_ \right\rang

双対系をもつ

左双対を持つ、かつ

右双対を持つ

WIP.icon