強化したベータ変換等式 - (2nd) 檜山正幸のキマイラ飼育記

$\newcommand{\hyp}{\mbox{-}}\newcommand{\cat}[1]{\mathcal{#1}}\newcommand{\In}{\mbox{ in }}\newcommand{\id}{\mathrm{id}}(\cat{C}, \otimes, I)$ をモノイド圏とする。デカルト性も対称性も仮定しない。モノイド閉構造が次のようにして与えられているとする。

右掛け算関手 $\hyp\otimes A:\cat{C} \to \cat{C}$ の右随伴パートナーが右指数関手 $\hyp^A:\cat{C}^{op} \to \cat{C}$ （対象部分だけでも十分）
左掛け算関手 $A\otimes \hyp:\cat{C} \to \cat{C}$ の右随伴パートナーが左指数関手 ${}^A\hyp:\cat{C}^{op} \to \cat{C}$ （対象部分だけでも十分）
右掛け算・右指数-随伴に伴う右カリー化が $RCurry^A_{X, Y}:\cat{C}(X\otimes A, Y) \to \cat{C}(X, Y^A)$
左掛け算・左指数-随伴に伴う左カリー化が $LCurry^A_{X, Y}:\cat{C}(A\otimes X, Y) \to \cat{C}(X, {}^A{Y})$
右カリー化の逆を与える右エバル $rev_{A,Y}: Y^A \otimes A \to Y \In\cat{C}$
左カリー化の逆を与える左エバル $lev_{A,Y}: A \otimes {}^A{Y} \to Y \In\cat{C}$

右エバルに関するベータ変換等式は：

$(RCurry^A_{X,Y}(f)\otimes \id_A); rev_{A, Y} = f : X\otimes A \to Y\In\cat{C}$

略記と省略を使えば：

$(f^\cap \otimes \id_A); rev = f : X\otimes A \to Y\In\cat{C}$

これを強化（ストロング化）した等式が得られる。

$(f^\cap \otimes \id_{F(A)}); rev^\heartsuit = f^\heartsuit : X\otimes F(A) \to F(Y)\In\cat{C}$

上の等式に出現した $F,\, \heartsuit$ について説明する。

$F:\cat{C} \to \cat{C}$ は関手（モノイド構造に対する挙動は特に仮定しない）、添字族 $\tau_{A,B}:A\otimes F(B) \to F(A\otimes B)\mbox{ for }A, B\in|\cat{C}|$ は自然変換になっており、テンソル強度の公理を満たす。対称性を仮定してないので、右強度 ${\tau'}_{A,B}: F(B)\otimes A \to F(B\otimes A)$ も必要だが、左強度だけ使う。

左強関手 $(F, \tau)$ を記号の乱用で単に $F$ と書く。左強関手があると、それをもとに圏論的コンビネータ $\Phi^F$ を次のように定義できる。

$\newcommand{\WeWillDefine}{\mbox{WeWillDefine }}% \newcommand{\WeDefine}{\mbox{WeDefine }}% \newcommand{\For}{\mbox{For }}% % \For F:\cat{C} \to \cat{C}\In {\bf CAT} \mbox{ strong-functor} \\ \For X, A, Y\in |\cat{C}|\\ \WeWillDefine \Phi^F_{X,A,Y}: \cat{C}(X\otimes A, Y) \to\cat{C}(X\otimes F(A), F(Y))\In {\bf Set}\\ \For f \in \cat{C}(X\otimes A, Y) \\ \WeDefine \Phi^F_{X,A,Y}(f) := \tau_{X, A};F(f) \,:X\otimes F(A) \to F(Y)\In\cat{C}$