左指数随伴系

summary.icon

signature.icon

code:left_exponential_adjunction.sig

a.LExpAdjs

= Adjunction C C (a⊗) (a⊸) a.unit a.eval

where

MonoidalCategory C ⊗ _ _ _ _ in &

&1-morph

(a⊸) : C -> C

&2-morph

a.unit : C^ => (a⊗) * (a⊸)

a.eval : (a⊸) * (a⊗) => C^

definition.icon

$ \mathrm{LExpAdjs}[a]

$ =\left\langle (a⊗) \dashv (a⊸) ,{}^a\mathrm{unit} ,{}^a\mathrm{eval} \right\rangle

随伴対

$ (a⊗) \colon C→C

$ (a⊸) = {}^a\_\colon C→C

https://gyazo.com/a06d2918b4910e35cd3f330eb7c9a07e

$ ^a\mathrm{unit} \colon C^\wedge ⇒ (a⊗) * (a⊸)

i.e.

$ {}^a\mathrm{unit}_z\colon z→a⊸(a\otimes z)

$ ^a\mathrm{eval} \colon (a⊸) * (a⊗) ⇒ C^\wedge

i.e.

$ {}^a\mathrm{eval}_z\colon a\otimes (a⊸z)→z

https://gyazo.com/8f8819411c213153b86172e78b5fec58

https://gyazo.com/484b8f6204b6ae732212938de933fef6

https://gyazo.com/250b9f8575edbd1f714b7cd3124d0234

into.icon

i.e.

out-of.icon

随伴系の自然同型、転置、反転置

$ {^a}\Lambda \colon \hom_C(a\otimes \_,\_) \Rightarrow \hom_C(\_,a⊸\_)

$ \colon C^\mathrm{op}× C \to \mathbf{Set}

$ {}^\cap\_ \coloneqq (x,y).\Lambda'^a

$ \colon \hom_C(a\otimes x,y) → \hom_C(x,{}^ay)

$ {}_{\cup}\_ \coloneqq (x,y).(\Lambda'^a )^{-1} =({}^{\cap}\_)^{-1}

$ \colon \hom_C(x,{}^ay) → \hom_C(a\otimes x,y)

p-dual.icon