評価関手関係の計算

モノイド圏 本編ネタ

余クライスリ評価関手の余クライスリ結合 - (新) 檜山正幸のキマイラ飼育記 メモ編 の、新しいターゲット命題に至るまでの等式的変形も書いておこう、忘れないうちに。 \newcommand{\Arr}{\:\downarrow } % \newcommand{\coM}{\boldsymbol{d} } % comultiplication \newcommand{\coU}{\boldsymbol{e} } % counit \newcommand{\Ev}{\mathrm{Ev} } \newcommand{\gcoM}{\bar{\boldsymbol{\delta}} } % generic comultiplication \newcommand{\oast}{\circledast }

余クライスリ圏の評価関手 1 ： ターゲット項

\widehat{\Ev}( (t, \beta, t'); (t', \beta', t''), \vec{A}) =\\ \begin{bmatrix} F(t[\vec{A}]) \\ \gcoM_t^\vec{A} \Arr\\ t[F\oast \vec{A}]\\ \coU_{t[F\oast \vec{A}]} \Arr\\ t[\vec{A}]\\ (\beta;\beta')[\vec{A}] \Arr\\ t''[\vec{A}] \end{bmatrix}

余クライスリ圏の評価関手 2 ： ソース項＝スタート

\widehat{\Ev}( (t, \beta, t'), \vec{A})\hat{;}\widehat{\Ev}( (t', \beta', t''), \vec{A}) =\\ \begin{array}{c} \begin{bmatrix} F(t[\vec{A}]) \\ \coM_{t[\vec{A}]} \Arr\\ F^2(t[\vec{A}]) \end{bmatrix} \\ F \begin{bmatrix} F(t[\vec{A}])\\ \gcoM_t^{\vec{A}} \Arr\\ t[F\oast \vec{A}] \\ t[\coU_{\oast( F\oast \vec{A}) } ] \Arr\\ t[\vec{A}]\\ \beta[\vec{A}] \Arr\\ t'[\vec{A}] \end{bmatrix} \\ \begin{bmatrix} F(t'[\vec{A}]) \\ \gcoM_{t'}^{\vec{A}} \Arr\\ t'[F\oast \vec{A}] \\ t'[\coU_{\oast (F\oast \vec{A})} ] \Arr\\ t'[\vec{A}]\\ \beta'[\vec{A}] \Arr\\ t''[\vec{A}] \end{bmatrix} \end{array}

書き方の変更

\begin{array}{c} \begin{bmatrix} F(t[\vec{A}]) \\ \coM_{t[\vec{A}]} \Arr\\ F^2(t[\vec{A}]) \end{bmatrix} \\ F \begin{bmatrix} F(t[\vec{A}])\\ \gcoM_t^{\vec{A}} \Arr\\ t[F\oast \vec{A}] \\ t[\coU_{\oast( F\oast \vec{A}) } ] \Arr\\ t[\vec{A}]\\ \end{bmatrix} \\ \begin{bmatrix} F(t[\vec{A}])\\ F(\beta[\vec{A}]) \Arr\\ F(t'[\vec{A}])\\ \gcoM_{t'}^{\vec{A}} \Arr\\ t'[F\oast \vec{A}] \\ \end{bmatrix} \\ \begin{bmatrix} t'[F\oast \vec{A}] \\ t'[\coU_{\oast (F\oast \vec{A})} ] \Arr\\ t'[\vec{A}]\\ \beta'[\vec{A}] \Arr\\ t''[\vec{A}] \end{bmatrix} \end{array}

第3ブロックに一般余結合律

\begin{array}{c} \begin{bmatrix} F(t[\vec{A}]) \\ \coM_{t[\vec{A}]} \Arr\\ F^2(t[\vec{A}]) \end{bmatrix} \\ F \begin{bmatrix} F(t[\vec{A}])\\ \gcoM_t^{\vec{A}} \Arr\\ t[F\oast \vec{A}] \\ t[\coU_{\oast( F\oast \vec{A}) } ] \Arr\\ t[\vec{A}]\\ \end{bmatrix} \\ \begin{bmatrix} F(t[\vec{A}])\\ \gcoM_{t}^{\vec{A}} \Arr\\ t[F\oast \vec{A}] \\ \beta[F\oast \vec{A}]) \Arr\\ t'[F\oast \vec{A}] \\ \end{bmatrix} \\ \begin{bmatrix} t'[F\oast \vec{A}] \\ t'[\coU_{\oast (F\oast \vec{A})} ] \Arr\\ t'[\vec{A}]\\ \beta'[\vec{A}] \Arr\\ t''[\vec{A}] \end{bmatrix} \end{array}

書き方の変更

\begin{array}{c} \begin{bmatrix} F(t[\vec{A}]) \\ \coM_{t[\vec{A}]} \Arr\\ F^2(t[\vec{A}]) \end{bmatrix} \\ F \begin{bmatrix} F(t[\vec{A}])\\ \gcoM_t^{\vec{A}} \Arr\\ t[F\oast \vec{A}] \\ t[\coU_{\oast( F\oast \vec{A}) } ] \Arr\\ t[\vec{A}]\\ \end{bmatrix} \\ \begin{bmatrix} F(t[\vec{A}])\\ \gcoM_{t}^{\vec{A}} \Arr\\ t[F\oast \vec{A}] \\ \end{bmatrix} \\ \begin{bmatrix} t[F\oast \vec{A}] \\ \beta[F\oast \vec{A}]) \Arr\\ t'[F\oast \vec{A}] \\ t'[\coU_{\oast (F\oast \vec{A})} ] \Arr\\ t'[\vec{A}] \end{bmatrix} \\ \begin{bmatrix} t'[\vec{A}]\\ \beta'[\vec{A}] \Arr\\ t''[\vec{A}] \end{bmatrix} \end{array}

第4ブロックにエレベーター法則

\begin{array}{c} \begin{bmatrix} F(t[\vec{A}]) \\ \coM_{t[\vec{A}]} \Arr\\ F^2(t[\vec{A}]) \end{bmatrix} \\ F \begin{bmatrix} F(t[\vec{A}])\\ \gcoM_t^{\vec{A}} \Arr\\ t[F\oast \vec{A}] \\ t[\coU_{\oast( F\oast \vec{A}) } ] \Arr\\ t[\vec{A}]\\ \end{bmatrix} \\ \begin{bmatrix} F(t[\vec{A}])\\ \gcoM_{t}^{\vec{A}} \Arr\\ t[F\oast \vec{A}] \\ \end{bmatrix} \\ \begin{bmatrix} t[F\oast \vec{A}] \\ t[\coU_{\oast (F\oast \vec{A})} ] \Arr\\ t[\vec{A}] \\ \beta[\vec{A}] \Arr\\ t'[ \vec{A}] \\ \end{bmatrix} \\ \begin{bmatrix} t'[\vec{A}]\\ \beta'[\vec{A}] \Arr\\ t''[\vec{A}] \end{bmatrix} \end{array}

書き方の変更

\begin{array}{c} \begin{bmatrix} F(t[\vec{A}]) \\ \coM_{t[\vec{A}]} \Arr\\ F^2(t[\vec{A}]) \end{bmatrix} \\ F \begin{bmatrix} F(t[\vec{A}])\\ \gcoM_t^{\vec{A}} \Arr\\ t[F\oast \vec{A}] \\ t[\coU_{\oast( F\oast \vec{A}) } ] \Arr\\ t[\vec{A}]\\ \end{bmatrix} \\ \begin{bmatrix} F(t[\vec{A}])\\ \gcoM_{t}^{\vec{A}} \Arr\\ t[F\oast \vec{A}] \\ t[\coU_{\oast (F\oast \vec{A})} ] \Arr\\ t[\vec{A}] \\ \end{bmatrix} \\ \begin{bmatrix} t[\vec{A}] \\ \beta[\vec{A}] \Arr\\ t'[ \vec{A}] \\ \beta'[\vec{A}] \Arr\\ t''[\vec{A}] \end{bmatrix} \end{array}

最後のブロックで結合の実行

\begin{array}{c} \begin{bmatrix} F(t[\vec{A}]) \\ \coM_{t[\vec{A}]} \Arr\\ F^2(t[\vec{A}]) \end{bmatrix} \\ F \begin{bmatrix} F(t[\vec{A}])\\ \gcoM_t^{\vec{A}} \Arr\\ t[F\oast \vec{A}] \\ t[\coU_{\oast( F\oast \vec{A}) } ] \Arr\\ t[\vec{A}]\\ \end{bmatrix} \\ \begin{bmatrix} F(t[\vec{A}])\\ \gcoM_{t}^{\vec{A}} \Arr\\ t[F\oast \vec{A}] \\ t[\coU_{\oast (F\oast \vec{A})} ] \Arr\\ t[\vec{A}] \\ \end{bmatrix} \\ \begin{bmatrix} t[\vec{A}] \\ (\beta;\beta')[\vec{A}] \Arr\\ t''[\vec{A}] \end{bmatrix} \end{array}

一部分を取り出して整理

\begin{bmatrix} F(t[\vec{A}]) \\ \coM_{t[\vec{A}]} \Arr\\ F^2(t[\vec{A}])\\ F(\gcoM_t^{\vec{A}} )\Arr\\ F(t[F\oast \vec{A}] )\\ F(t[\coU_{\oast( F\oast \vec{A}) } ] )\Arr\\ F(t[\vec{A}] )\\ \gcoM_{t}^{\vec{A}} \Arr\\ t[F\oast \vec{A}] \\ t[\coU_{\oast (F\oast \vec{A})} ] \Arr\\ t[\vec{A}] \\ \end{bmatrix}

新しいターゲット命題〈等式〉を作成

\begin{bmatrix} F(t[\vec{A}]) \\ \gcoM_t^\vec{A} \Arr\\ t[F\oast \vec{A}]\\ \coU_{t[F\oast \vec{A}]} \Arr\\ t[\vec{A}]\\ \end{bmatrix} = \begin{bmatrix} F(t[\vec{A}]) \\ \coM_{t[\vec{A}]} \Arr\\ F^2(t[\vec{A}])\\ F(\gcoM_t^{\vec{A}} )\Arr\\ F(t[F\oast \vec{A}] )\\ F(t[\coU_{\oast( F\oast \vec{A}) } ] )\Arr\\ F(t[\vec{A}] )\\ \gcoM_{t}^{\vec{A}} \Arr\\ t[F\oast \vec{A}] \\ t[\coU_{\oast (F\oast \vec{A})} ] \Arr\\ t[\vec{A}] \\ \end{bmatrix}