豊穣圏の導入 第4回: Underlying Category について (前半)
前回の記事 [
8
] では，モノイダル圏$\cat{V}$に対して$\cat{V}$-圏や$\cat{V}$-関手を定義して，基本的な$\cat{V}$-関手を構成して，$\cat{V}$-関手の性質を述べた．
この記事では，モノイダル圏$\cat{V}$と$\cat{W}$に対して，$\cat{V}$から$\cat{W}$への lax モノイダル関手が "$\cat{V}$-圏を$\cat{W}$-圏に写す" ことを示す．
導入
素朴集合論の基礎 (集合と写像，空集合など) に親しみがあり，圏の定義を知っていることを仮定する．
第2回 (前半) の記事 [ 6 ] からは，定義 5 を用いており，これを定義 2.a.5 で表している．
第3回の記事 [ 8 ] からは，定義 2 を用いており，これを定義 3.2 で表している．
$\cat{V}$-圏の underlying category について
$\cat{V}$をモノイダル圏とする．第3回の記事 [ 8 ] では，圏を自然に拡張した概念として$\cat{V}$-圏が定義された．
一方で，$\cat{V}$-圏$\ecat{A}$に対して，$\ecat{A}$の underlying category とよばれる圏がある意味で自然に構成される．ここでは，[ 3 , Tag 00BL ] を参考に underlying category の構成について述べる．
Lax モノイダル関手
Lax モノイダル関手の定義
$\cat{V}$と$\cat{W}$をモノイダル圏とする．
- 関手$\func{F}{\cat{V}}{\cat{W}}$，
- $\otimes(F\times F)$から$F\otimes $への自然変換$\mu$，
- $I$から$FI$への$\cat{W}$での射$e$
の組$\widehat{F}=(F,\mu,e)$が$\cat{V}$から$\cat{W}$へのlax モノイダル関手 (lax monoidal functor) であるとは，以下が成り立つことをいう:
任意の$X,Y,Z\in\cat{V}$に対して，以下の等式が成り立つ:
$$\textstyle F(a_{X,Y,Z})\mu_{X\otimes Y,Z}(\mu_{X,Y}\otimes\id{FZ})=\mu_{X,Y\otimes Z}(\id{FX}\otimes\,\mu_{Y,Z})a_{FX,FY,FZ}.$$
$$\xymatrix{{(FX\otimes FY)\otimes FZ}\ar[d]_-{\mu_{X,Y}\otimes\,\id{FZ}}\ar[rr]^-{a_{FX,FY,FZ}}&&{FX\otimes(FY\otimes FZ)}\ar[d]^-{\id{FX}\,\otimes\,\mu_{Y,Z}}\\ {F(X\otimes Y)\otimes FZ}\ar[d]_-{\mu_{X\otimes Y,Z}}&&{FX\otimes F(Y\otimes Z)}\ar[d]^-{\mu_{X,Y\otimes Z}}\\ {F((X\otimes Y)\otimes Z)}\ar[rr]_-{F(a_{X,Y,Z})}&&{F(X\otimes(Y\otimes Z))}}$$任意の$X\in\cat{V}$に対して，$F(l_X)\mu_{I,X}(e\otimes\id{FX})=l_{FX}$である:
$$\xymatrix{{I\otimes FX}\ar[rr]^-{e\otimes\id{FX}}\ar[d]_-{l_{FX}}&&{FI\otimes FX}\ar[d]^-{\mu_{I,X}}\\ {FX}&&{F(I\otimes X)}\ar[ll]_-{F(l_X)}}$$任意の$X\in\cat{V}$に対して，$F(r_X)\mu_{X,I}(\id{FX}\otimes e)=r_{FX}$である:
$$\xymatrix{{FX\otimes I}\ar[rr]^-{\id{FX}\otimes e}\ar[d]_-{r_{FX}}&&{FX\otimes FI}\ar[d]^-{\mu_{X,I}}\\ {FX}&&{F(X\otimes I)}\ar[ll]_-{F(r_X)}}$$
$\widehat{F}$が$\cat{V}$から$\cat{W}$への lax モノイダル関手であることを，$\func{\widehat{F}}{\cat{V}}{\cat{W}}$が lax モノイダル関手であるという．また，lax モノイダル関手$\func{\widehat{F}=(F,\mu,e)}{\cat{V}}{\cat{W}}$に対して，$\widehat{F}$を$F$と略記する．
定義 7 の解説
$\cat{V}$と$\cat{W}$をモノイダル圏として，$\func{F}{\cat{V}}{\cat{W}}$を関手とする．
$\otimes$は$\cat{W}^2$から$\cat{W}$への関手であり，$F$は$\cat{V}$から$\cat{W}$への関手だから，$F\times F$は$\cat{V}^2$から$\cat{W}^2$への関手であり，$\otimes$と$F\times F$の合成$\otimes(F\times F)$が$\cat{V}^2$から$\cat{W}$への関手として定まる．
また，$F$は$\cat{V}$から$\cat{W}$への関手であり，$\otimes$は$\cat{V}^2$から$\cat{V}$への関手であり，$F$と$\otimes$の合成$F\otimes$が$\cat{V}^2$から$\cat{W}$への関手として定まる．
$X,Y\in\cat{V}$に対して，
\begin{align}
\textstyle(\otimes(F\times F))(X,Y)&\,\textstyle=\otimes((F\times F)(X,Y))\\
&\,\textstyle=\otimes(FX,FY)&(\text{定義
2.a.5})\\
&\,\textstyle=FX\otimes FY,
\end{align}
かつ$(F\otimes)(X,Y)=F(\otimes(X,Y))=F(X\otimes Y)$であり，$\cat{V}$での射$\func{f}{X}{X'}$と$\func{g}{Y}{Y'}$に対して，
\begin{align}
\textstyle(\otimes(F\times F))(f,g)&\,\textstyle=\otimes((F\times F)(f,g))\\
&\,\textstyle=\otimes(F(f),F(g))&(\text{定義
2.a.5})\\
&\,\textstyle=F(f)\otimes F(g),
\end{align}
かつ$(F\otimes)((f,g))=F(\otimes((f,g)))=F(f\otimes g)$だから，$\mu$が$\otimes(F\times F)$から$F\otimes$への自然変換であるということは，$\mu$が$FX\otimes FY$から$F(X\otimes Y)$への$\cat{W}$での射$\mu_{X,Y}$ ($X,Y\in\cat{V}$) の族$\{\func{\mu_{X,Y}}{FX\otimes FY}{F(X\otimes Y)}\}_{X,Y\in\cat{V}}$であり，$\cat{V}$での任意の射$\func{f}{X}{X'}$と$\func{g}{Y}{Y'}$に対して，$\mu_{X',Y'}(F(f)\otimes F(g))=F(f\otimes g)\mu_{X,Y}$が成立するということである:
$$\xymatrix{{FX\otimes FY}\ar[r]^-{\mu_{X,Y}}\ar[d]_-{F(f)\otimes F(g)}&{F(X\otimes Y)}\ar[d]^-{F(f\otimes g)}\\
{FX'\otimes FY'}\ar[r]_-{\mu_{X',Y'}}&{F(X'\otimes Y')}}$$
従って，以下が成り立つ:
$\cat{V}$と$\cat{W}$をモノイダル圏とする．
- 関手$\func{F}{\cat{V}}{\cat{W}}$，
- $\cat{W}$での射$\func{\mu_{X,Y}}{FX\otimes FY}{F(X\otimes Y)}$ ($X,Y\in\cat{V}$)，
- $\cat{W}$での射$\func{e}{I}{FI}$，
が与えられているとする．$\cat{W}$での射の族$\mu$を$\mu=\{\mu_{X,Y}\}_{X,Y\in\cat{V}}$で定めるとき，組$(F,\mu,e)$が$\cat{V}$から$\cat{W}$への lax モノイダル関手であることは，以下が成立することと同値である:
$\cat{V}$での任意の射$\func{f}{X}{X'}$と$\func{g}{Y}{Y'}$に対して，$\mu_{X',Y'}(F(f)\otimes F(g))=F(f\otimes g)\mu_{X,Y}$である:
$$\xymatrix{{FX\otimes FY}\ar[r]^-{\mu_{X,Y}}\ar[d]_-{F(f)\otimes F(g)}&{F(X\otimes Y)}\ar[d]^-{F(f\otimes g)}\\ {FX'\otimes FY'}\ar[r]_-{\mu_{X',Y'}}&{F(X'\otimes Y')}}$$任意の$X,Y,Z\in\cat{V}$に対して，以下の等式が成り立つ:
$$\textstyle F(a_{X,Y,Z})\mu_{X\otimes Y,Z}(\mu_{X,Y}\otimes\id{FZ})=\mu_{X,Y\otimes Z}(\id{FX}\otimes\,\mu_{Y,Z})a_{FX,FY,FZ}.$$
$$\xymatrix{{(FX\otimes FY)\otimes FZ}\ar[d]_-{\mu_{X,Y}\otimes\,\id{FZ}}\ar[rr]^-{a_{FX,FY,FZ}}&&{FX\otimes(FY\otimes FZ)}\ar[d]^-{\id{FX}\,\otimes\,\mu_{Y,Z}}\\ {F(X\otimes Y)\otimes FZ}\ar[d]_-{\mu_{X\otimes Y,Z}}&&{FX\otimes F(Y\otimes Z)}\ar[d]^-{\mu_{X,Y\otimes Z}}\\ {F((X\otimes Y)\otimes Z)}\ar[rr]_-{F(a_{X,Y,Z})}&&{F(X\otimes(Y\otimes Z))}}$$任意の$X\in\cat{V}$に対して，$F(l_X)\mu_{I,X}(e\otimes\id{FX})=l_{FX}$である:
$$\xymatrix{{I\otimes FX}\ar[rr]^-{e\otimes\id{FX}}\ar[d]_-{l_{FX}}&&{FI\otimes FX}\ar[d]^-{\mu_{I,X}}\\ {FX}&&{F(I\otimes X)}\ar[ll]_-{F(l_X)}}$$任意の$X\in\cat{V}$に対して，$F(r_X)\mu_{X,I}(\id{FX}\otimes e)=r_{FX}$である:
$$\xymatrix{{FX\otimes I}\ar[rr]^-{\id{FX}\otimes e}\ar[d]_-{r_{FX}}&&{FX\otimes FI}\ar[d]^-{\mu_{X,I}}\\ {FX}&&{F(X\otimes I)}\ar[ll]_-{F(r_X)}}$$
$\cat{W}$-圏$F(\ecat{A})$の構成
$\func{F}{\cat{V}}{\cat{W}}$を lax モノイダル関手として，$\ecat{A}$を$\cat{V}$-圏とする．$\cat{W}$-圏$F(\ecat{A})$を以下で定める:
(1) 集合の "集まり"$\ob{(F(\ecat{A}))}$を$\ob{(F(\ecat{A}))}:=\ob{\ecat{A}}$で定める．
(2) 各$A,B\in\ob{(F(\ecat{A}))}=\ob{\ecat{A}}$に対して，$\cat{W}$の対象$\mor{F(\ecat{A})}{A}{B}$を$\mor{F(\ecat{A})}{A}{B}:=F(\mor{\ecat{A}}{A}{B})$で定める．
(3) 各$A,B,C\in\ob{(F(\ecat{A}))}=\ob{\ecat{A}}$に対して，$\mor{F(\ecat{A})}{B}{C}\otimes\mor{F(\ecat{A})}{A}{B}=F(\mor{\ecat{A}}{B}{C})\otimes F(\mor{\ecat{A}}{A}{B})$から$\mor{F(\ecat{A})}{A}{C}=F(\mor{\ecat{A}}{A}{C})$への$\cat{W}$での射$M_{A,B,C}$を$M_{A,B,C}:=F(M_{A,B,C})\mu_{\mor{\ecat{A}}{B}{C},\mor{\ecat{A}}{A}{B}}$で定める:
$$\xymatrix{{\mor{F(\ecat{A})}{B}{C}\otimes\mor{F(\ecat{A})}{A}{B}}\ar@{=}[r]\ar[dd]_-{M_{A,B,C}}&{F(\mor{\ecat{A}}{B}{C})\otimes F(\mor{\ecat{A}}{A}{B})}\ar[d]^-{\mu_{\mor{\ecat{A}}{B}{C},\mor{\ecat{A}}{A}{B}}}\\
&{F(\mor{\ecat{A}}{B}{C}\otimes\mor{\ecat{A}}{A}{B})}\ar[d]^-{F(M_{A,B,C})}\\
{\mor{F(\ecat{A})}{A}{C}}\ar@{=}[r]&{F(\mor{\ecat{A}}{A}{C})}
}$$
- 各$A\in\ob{(F(\ecat{A}))}=\ob{\ecat{A}}$に対して，$I$から$\mor{F(\ecat{A})}{A}{B}=F(\mor{\ecat{A}}{A}{B})$への$\cat{W}$での射$j_A$を$j_A:=F(j_A)e$で定める:
$$\xymatrix{{I}\ar[r]^-{e}\ar[d]_-{j_A}&{FI}\ar[d]^-{F(j_A)}\\ {\mor{F(\ecat{A})}{A}{A}}\ar@{=}[r]&{F(\mor{\ecat{A}}{A}{A})}}$$
以下では，Lax モノイダル関手$\func{F}{\cat{V}}{\cat{W}}$と$\cat{V}$-圏$\ecat{A}$を固定して，$F(\ecat{A})$が$\cat{W}$-圏をなすことを証明する．
簡単のために，$F(\ecat{A})$を$\ecat{A}'$で表し，$A,B\in\ob{\ecat{A}}$に対して$\mor{\ecat{A}}{A}{B}$を$\ecat{A}_{A,B}$で表し，$A,B\in\ob{\ecat{A}'}=\ob{\ecat{A}}$に対して$\mor{\ecat{A}'}{A}{B}$を$\ecat{A}'_{A,B}$で表す．$\ecat{A}:=(\ob{\ecat{A}},\{\ecat{A}_{A,B}\}_{A,B\in\ecat{A}},\{M_{A,B,C}\}_{A,B,C\in\ecat{A}},\{j_A\}_{A\in\ecat{A}})$及び$\ecat{A}':=(\ob{\ecat{A}'},\{\ecat{A}'_{A,B}\}_{A,B\in\ecat{A}},\{M'_{A,B,C}\}_{A,B,C\in\ecat{A}},\{j'_A\}_{A\in\ecat{A}})$と表す．
このとき，$\ob{\ecat{A}'}=\ob{\ecat{A}}$であり，$\ecat{A}'_{A,B}=F(\ecat{A}_{A,B})$ ($A,B\in\ecat{A}$) であり，$M'_{A,B,C}=F(M_{A,B,C})\mu_{\ecat{A}_{B,C},\ecat{A}_{A,B}}$ ($A,B,C\in\ecat{A}$) であり:
$$\xymatrix{{\ecat{A}'_{B,C}\otimes\ecat{A}'_{A,B}}\ar@{=}[r]\ar[dd]_-{M'_{A,B,C}}&{F(\ecat{A}_{B,C})\otimes F(\ecat{A}_{A,B})}\ar[d]^-{\mu_{\ecat{A}_{B,C},\ecat{A}_{A,B}}}\\
&{F(\ecat{A}_{B,C}\otimes\ecat{A}_{A,B})}\ar[d]^-{F(M_{A,B,C})}\\
{\ecat{A}'_{A,C}}\ar@{=}[r]&{F(\ecat{A}_{A,C})}
}$$
$j'_A:=F(j_A)e$ ($A\in\ecat{A}$) である:
$$\xymatrix{{I}\ar[r]^-{e}\ar[d]_-{j'_A}&{FI}\ar[d]^-{F(j_A)}\\
{\ecat{A}'_{A,A}}\ar@{=}[r]&{F(\ecat{A}_{A,A})}}$$
$\ecat{A}'$が定義 3.2, (1) をみたすこと
$A,B\in\ecat{A}$を任意に取る．
まず，$l_{\ecat{A}'_{A,B}}=M'_{A,B,B}(j'_B\otimes\id{\ecat{A}'_{A,B}})$であることを示す．
$\func{\otimes}{\cat{W}^2}{\cat{W}}$は関手だから，第2回 (後半) の記事 [ 7 ] の §2.2 で述べたように，$(F(j_B)\otimes F(\id{\ecat{A}_{A,B}}))(e\otimes\id{F(\ecat{A}_{A,B})})=(F(j_B)e)\otimes(F(\id{\ecat{A}_{A,B}})\,\id{F(\ecat{A}_{A,B})})$である．
$\func{F}{\cat{V}}{\cat{W}}$は lax モノイダル関手だから，以下が成り立つ:
定義 1 より$\func{F}{\cat{V}}{\cat{W}}$は関手であり，
$F(M_{A,B,B}(j_B\otimes\id{\ecat{A}_{A,B}}))=F(M_{A,B,B})F(j_B\otimes\id{\ecat{A}_{A,B}})$かつ$F(\id{\ecat{A}_{A,B}})=\id{F(\ecat{A}_{A,B})}$である．命題 2, (1) より$F(j_B\otimes\id{\ecat{A}_{A,B}})\mu_{I,\ecat{A}_{A,B}}=\mu_{\ecat{A}_{B,B},\ecat{A}_{A,B}}(F(j_B)\otimes F(\id{\ecat{A}_{A,B}}))$である:
$$\xymatrix{{FI\otimes F(\ecat{A}_{A,B}))}\ar[rr]^-{\mu_{I,\ecat{A}_{A,B}}}\ar[d]_-{F(j_B)\otimes F(\id{\ecat{A}_{A,B}})}&&{F(I\otimes\ecat{A}_{A,B})}\ar[d]^-{F(j_B\otimes\,\id{\ecat{A}_{A,B}})}\\ {F(\ecat{A}_{B,B})\otimes F(\ecat{A}_{A,B})}\ar[rr]_-{\mu_{\ecat{A}_{B,B},\ecat{A}_{A,B}}}&&{F(\ecat{A}_{B,B}\otimes\ecat{A}_{A,B})}}$$命題 2, (3) より$l_{F(\ecat{A}_{A,B})}=F(l_{\ecat{A}_{A,B}})\mu_{I,\ecat{A}_{A,B}}(e\otimes\id{F(\ecat{A}_{A,B})})$である:
$$\xymatrix{{I\otimes F(\ecat{A}_{A,B})}\ar[rr]^-{e\otimes\id{F(\ecat{A}_{A,B})}}\ar[d]_-{l_{F(\ecat{A}_{A,B})}}&&{FI\otimes F(\ecat{A}_{A,B})}\ar[d]^-{\mu_{I,\ecat{A}_{A,B}}}\\ {F(\ecat{A}_{A,B})}&&{F(I\otimes\ecat{A}_{A,B})}\ar[ll]_-{F(l_{\ecat{A}_{A,B}})}}$$
また，$\ecat{A}$は$\cat{V}$-圏だから，定義 3.2, (1) より$l_{\ecat{A}_{A,B}}=M_{A,B,B}(j_B\otimes\id{\ecat{A}_{A,B}})$である:
$$\xymatrix{{\ecat{A}_{B,B}\otimes\ecat{A}_{A,B}}\ar[r]^-{M_{A,B,B}}&{\ecat{A}_{A,B}}\\
{I\otimes\ecat{A}_{A,B}}\ar[u]^-{j_B\otimes\,\id{\ecat{A}_{A,B}}}\ar[ru]_-{l_{\ecat{A}_{A,B}}}}$$
従って，
- $(F(j_B)\otimes F(\id{\ecat{A}_{A,B}}))(e\otimes\id{F(\ecat{A}_{A,B})})=(F(j_B)e)\otimes(F(\id{\ecat{A}_{A,B}})\,\id{F(\ecat{A}_{A,B})})$，
- $F(M_{A,B,B}(j_B\otimes\id{\ecat{A}_{A,B}}))=F(M_{A,B,B})F(j_B\otimes\id{\ecat{A}_{A,B}})$，
- $F(\id{\ecat{A}_{A,B}})=\id{F(\ecat{A}_{A,B})}$，
- $F(j_B\otimes\id{\ecat{A}_{A,B}})\mu_{I,\ecat{A}_{A,B}}=\mu_{\ecat{A}_{B,B},\ecat{A}_{A,B}}(F(j_B)\otimes F(\id{\ecat{A}_{A,B}}))$，
- $l_{F(\ecat{A}_{A,B})}=F(l_{\ecat{A}_{A,B}})\mu_{I,\ecat{A}_{A,B}}(e\otimes\id{F(\ecat{A}_{A,B})})$，
- $l_{\ecat{A}_{A,B}}=M_{A,B,B}(j_B\otimes\id{\ecat{A}_{A,B}})$，
が成り立つので，
\begin{align}
&\,\,\,\,\,\,\,\,\textstyle l_{\ecat{A}'_{A,B}}\\
&\,\textstyle=l_{F(\ecat{A}_{A,B})}\\
&\,\textstyle=F(l_{\ecat{A}_{A,B}})\mu_{I,\ecat{A}_{A,B}}(e\otimes\id{F(\ecat{A}_{A,B})})\\
&\,\textstyle=F(M_{A,B,B}(j_B\otimes\id{\ecat{A}_{A,B}}))\mu_{I,\ecat{A}_{A,B}}(e\otimes\id{F(\ecat{A}_{A,B})})\\
&\,\textstyle=F(M_{A,B,B})F(j_B\otimes\id{\ecat{A}_{A,B}})\mu_{I,\ecat{A}_{A,B}}(e\otimes\id{F(\ecat{A}_{A,B})})\\
&\,\textstyle=F(M_{A,B,B})\mu_{\ecat{A}_{B,B},\ecat{A}_{A,B}}(F(j_B)\otimes F(\id{\ecat{A}_{A,B}}))(e\otimes\id{F(\ecat{A}_{A,B})})\\
&\,\textstyle=F(M_{A,B,B})\mu_{\ecat{A}_{B,B},\ecat{A}_{A,B}}((F(j_B)e)\otimes(F(\id{\ecat{A}_{A,B}})\,\id{F(\ecat{A}_{A,B})}))\\
&\,\textstyle=F(M_{A,B,B})\mu_{\ecat{A}_{B,B},\ecat{A}_{A,B}}((F(j_B)e)\otimes F(\id{\ecat{A}_{A,B}}))\\
&\,\textstyle=F(M_{A,B,B})\mu_{\ecat{A}_{B,B},\ecat{A}_{A,B}}((F(j_B)e)\otimes \id{F(\ecat{A}_{A,B})})\\
&\,\textstyle=F(M_{A,B,B})\mu_{\ecat{A}_{B,B},\ecat{A}_{A,B}}((F(j_B)e)\otimes \id{\ecat{A}'_{A,B}})\\
&\,\textstyle=M'_{A,B,B}((F(j_B)e)\otimes \id{\ecat{A}'_{A,B}})\\
&\,\textstyle=M'_{A,B,B}(j'_B\otimes\id{\ecat{A}'_{A,B}}),
\end{align}
である:
$$\xymatrix{{\ecat{A}'_{B,B}\otimes\ecat{A}'_{A,B}}\ar[r]^-{M'_{A,B,B}}&{\ecat{A}'_{A,B}}\\
{I\otimes\ecat{A}'_{A,B}}\ar[u]^-{j'_B\otimes\,\id{\ecat{A}'_{A,B}}}\ar[ru]_-{l_{\ecat{A}'_{A,B}}}}$$
次に，$r_{\ecat{A}'_{A,B}}=M'_{A,A,B}(\id{\ecat{A}'_{A,B}}\otimes j'_A)$であることを示す．
$\func{\otimes}{\cat{W}^2}{\cat{W}}$は関手だから，第2回 (後半) の記事 [ 7 ] の §2.2 で述べたように，$(F(\id{\ecat{A}_{A,B}})\otimes F(j_A))(\id{F(\ecat{A}_{A,B})}\otimes e)=(F(\id{\ecat{A}_{A,B}})\,\id{F(\ecat{A}_{A,B})})\otimes(F(j_A)e)$である．
$\func{F}{\cat{V}}{\cat{W}}$は lax モノイダル関手だから，以下が成り立つ:
定義 1 より$\func{F}{\cat{V}}{\cat{W}}$は関手であり，$F(M_{A,A,B}(\id{\ecat{A}_{A,B}}\otimes j_A))=F(M_{A,A,B})F(\id{\ecat{A}_{A,B}}\otimes j_A)$かつ$F(\id{\ecat{A}_{A,B}})=\id{F(\ecat{A}_{A,B})}$である．
命題 2, (1) より$F(\id{\ecat{A}_{A,B}}\otimes j_A)\mu_{\ecat{A}_{A,B},I}=\mu_{\ecat{A}_{A,B},\ecat{A}_{A,A}}(F(\id{\ecat{A}_{A,B}})\otimes F(j_A))$である:
$$\xymatrix{{F(\ecat{A}_{A,B})\otimes FI}\ar[r]^-{\mu_{\ecat{A}_{A,B},I}}\ar[d]_-{F(\id{\ecat{A}_{A,B}})\otimes F(j_A)}&{F(\ecat{A}_{A,B}\otimes I)}\ar[d]^-{F(\id{\ecat{A}_{A,B}}\otimes j_A)}\\ {F(\ecat{A}_{A,B})\otimes F(\ecat{A}_{A,A})}\ar[r]_-{\mu_{\ecat{A}_{A,B},\ecat{A}_{A,A}}}&{F(\ecat{A}_{A,B}\otimes\ecat{A}_{A,A})}}$$命題 2, (4) より$r_{F(\ecat{A}_{A,B})}=F(r_{\ecat{A}_{A,B}})\mu_{\ecat{A}_{A,B},I}(\id{F(\ecat{A}_{A,B})}\otimes e)$である:
$$\xymatrix{{F(\ecat{A}_{A,B})\otimes I}\ar[rr]^-{\id{F(\ecat{A}_{A,B})}\otimes e}\ar[d]_-{r_{F(\ecat{A}_{A,B})}}&&{F(\ecat{A}_{A,B})\otimes FI}\ar[d]^-{\mu_{\ecat{A}_{A,B},I}}\\ {F(\ecat{A}_{A,B})}&&{F(\ecat{A}_{A,B}\otimes I)}\ar[ll]_-{F(r_{\ecat{A}_{A,B}})}}$$
また，$\ecat{A}$は$\cat{V}$-圏だから，定義 3.2, (1) より$r_{\ecat{A}_{A,B}}=M_{A,A,B}(\id{\ecat{A}_{A,B}}\otimes j_A)$である:
$$\xymatrix{{\ecat{A}_{A,B}\otimes\ecat{A}_{A,A}}\ar[r]^-{M_{A,A,B}}&{\ecat{A}_{A,B}}\\
{\ecat{A}_{A,B}\otimes I}\ar[u]^-{\id{\ecat{A}_{A,B}}\otimes\,j_A}\ar[ru]_-{r_{\ecat{A}_{A,B}}}}$$
従って，
- $(F(\id{\ecat{A}_{A,B}})\otimes F(j_A))(\id{F(\ecat{A}_{A,B})}\otimes e)=(F(\id{\ecat{A}_{A,B}})\,\id{F(\ecat{A}_{A,B})})\otimes(F(j_A)e)$，
- $F(M_{A,A,B}(\id{\ecat{A}_{A,B}}\otimes j_A))=F(M_{A,A,B})F(\id{\ecat{A}_{A,B}}\otimes j_A)$，
- $F(\id{\ecat{A}_{A,B}})=\id{F(\ecat{A}_{A,B})}$，
- $F(\id{\ecat{A}_{A,B}}\otimes j_A)\mu_{\ecat{A}_{A,B},I}=\mu_{\ecat{A}_{A,B},\ecat{A}_{A,A}}(F(\id{\ecat{A}_{A,B}})\otimes F(j_A))$，
- $r_{F(\ecat{A}_{A,B})}=F(r_{\ecat{A}_{A,B}})\mu_{\ecat{A}_{A,B},I}(\id{F(\ecat{A}_{A,B})}\otimes e)$，
- $r_{\ecat{A}_{A,B}}=M_{A,A,B}(\id{\ecat{A}_{A,B}}\otimes j_A)$，
が成り立つので，
\begin{align}
&\,\,\,\,\,\,\,\,\textstyle r_{\ecat{A}'_{A,B}}\\
&\,\textstyle=r_{F(\ecat{A}_{A,B})}\\
&\,\textstyle=F(r_{\ecat{A}_{A,B}})\mu_{\ecat{A}_{A,B},I}(\id{F(\ecat{A}_{A,B})}\otimes e)\\
&\,\textstyle=F(M_{A,A,B}(\id{\ecat{A}_{A,B}}\otimes j_A))\mu_{\ecat{A}_{A,B},I}(\id{F(\ecat{A}_{A,B})}\otimes e)\\
&\,\textstyle=F(M_{A,A,B})F(\id{\ecat{A}_{A,B}}\otimes j_A)\mu_{\ecat{A}_{A,B},I}(\id{F(\ecat{A}_{A,B})}\otimes e)\\
&\,\textstyle=F(M_{A,A,B})\mu_{\ecat{A}_{A,B},\ecat{A}_{A,A}}(F(\id{\ecat{A}_{A,B}})\otimes F(j_A))(\id{F(\ecat{A}_{A,B})}\otimes e)\\
&\,\textstyle=F(M_{A,A,B})\mu_{\ecat{A}_{A,B},\ecat{A}_{A,A}}((F(\id{\ecat{A}_{A,B}})\,\id{F(\ecat{A}_{A,B})})\otimes(F(j_A)e))\\
&\,\textstyle=F(M_{A,A,B})\mu_{\ecat{A}_{A,B},\ecat{A}_{A,A}}(F(\id{\ecat{A}_{A,B}})\otimes(F(j_A)e))\\
&\,\textstyle=F(M_{A,A,B})\mu_{\ecat{A}_{A,B},\ecat{A}_{A,A}}(\id{F(\ecat{A}_{A,B})}\otimes(F(j_A)e))\\
&\,\textstyle=F(M_{A,A,B})\mu_{\ecat{A}_{A,B},\ecat{A}_{A,A}}(\id{\ecat{A}'_{A,B}}\otimes(F(j_A)e))\\
&\,\textstyle=M'_{A,A,B}(\id{\ecat{A}'_{A,B}}\otimes(F(j_A)e))\\
&\,\textstyle=M'_{A,A,B}(\id{\ecat{A}'_{A,B}}\otimes j'_A),
\end{align}
である:
$$\xymatrix{{\ecat{A}'_{A,B}\otimes\ecat{A}'_{A,A}}\ar[r]^-{M'_{A,A,B}}&{\ecat{A}'_{A,B}}\\
{\ecat{A}'_{A,B}\otimes I}\ar[u]^-{\id{\ecat{A}'_{A,B}}\otimes\,j'_A}\ar[ru]_-{r_{\ecat{A}'_{A,B}}}}$$
$\ecat{A}'$が定義 3.2, (2) をみたすこと
$A,B,C,D\in\ecat{A}$を任意に取る．
$\func{\otimes}{\cat{W}^2}{\cat{W}}$は関手だから，第2回 (後半) の記事 [
7
] の §2.2 で述べたように，
$$\textstyle(F(M_{B,C,D})\mu_{\ecat{A}_{C,D},\ecat{A}_{B,C}})\otimes(\id{F(\ecat{A}_{A,B})}\,\id{F(\ecat{A}_{A,B})})=(F(M_{B,C,D})\otimes\id{F(\ecat{A}_{A,B})})(\mu_{\ecat{A}_{C,D},\ecat{A}_{B,C}}\otimes\id{F(\ecat{A}_{A,B})}),$$
かつ
$$\textstyle(\id{F(\ecat{A}_{C,D})}\otimes F(M_{A,B,C}))(\id{F(\ecat{A}_{C,D})}\otimes\,\mu_{\ecat{A}_{B,C},\ecat{A}_{A,B}})=(\id{F(\ecat{A}_{C,D})}\,\id{F(\ecat{A}_{C,D})})\otimes(F(M_{A,B,C})\mu_{\ecat{A}_{B,C},\ecat{A}_{A,B}}),$$
である．
$\func{F}{\cat{V}}{\cat{W}}$は lax モノイダル関手だから，以下が成り立つ:
定義 1 より$\func{F}{\cat{V}}{\cat{W}}$は関手であり，
$$\textstyle F(M_{A,B,D})F(M_{B,C,D}\otimes\id{\ecat{A}_{A,B}})=F(M_{A,B,D}(M_{B,C,D}\otimes\id{\ecat{A}_{A,B}})),$$
かつ
$$\textstyle F(M_{A,C,D}(\id{\ecat{A}_{C,D}}\otimes M_{A,B,C})a_{\ecat{A}_{C,D},\ecat{A}_{B,C},\ecat{A}_{A,B}})=F(M_{A,C,D})F((\id{\ecat{A}_{C,D}}\otimes M_{A,B,C})a_{\ecat{A}_{C,D},\ecat{A}_{B,C},\ecat{A}_{A,B}}),$$
かつ
$$\textstyle F((\id{\ecat{A}_{C,D}}\otimes M_{A,B,C})a_{\ecat{A}_{C,D},\ecat{A}_{B,C},\ecat{A}_{A,B}})=F(\id{\ecat{A}_{C,D}}\otimes M_{A,B,C})F(a_{\ecat{A}_{C,D},\ecat{A}_{B,C},\ecat{A}_{A,B}}),$$
かつ$\id{F(\ecat{A}_{A,B})}=F(\id{\ecat{A}_{A,B}})$かつ$F(\id{\ecat{A}_{C,D}})=\id{F(\ecat{A}_{C,D})}$である．命題 2, (1) より
$$\textstyle\mu_{\ecat{A}_{B,D},\ecat{A}_{A,B}}(F(M_{B,C,D})\otimes F(\id{\ecat{A}_{A,B}}))=F(M_{B,C,D}\otimes\id{\ecat{A}_{A,B}})\mu_{\ecat{A}_{C,D}\otimes\ecat{A}_{B,C},\ecat{A}_{A,B}},$$
であり:
$$\xymatrix{{F(\ecat{A}_{C,D}\otimes\ecat{A}_{B,C})\otimes F(\ecat{A}_{A,B})}\ar[rr]^-{\mu_{\ecat{A}_{C,D}\otimes\ecat{A}_{B,C},\ecat{A}_{A,B}}}\ar[d]_-{F(M_{B,C,D})\otimes F(\id{\ecat{A}_{A,B}})}&&{F((\ecat{A}_{C,D}\otimes\ecat{A}_{B,C})\otimes\ecat{A}_{A,B})}\ar[d]^-{F(M_{B,C,D}\otimes\id{\ecat{A}_{A,B}})}\\ {F(\ecat{A}_{B,D})\otimes F(\ecat{A}_{A,B})}\ar[rr]_-{\mu_{\ecat{A}_{B,D},\ecat{A}_{A,B}}}&&{F(\ecat{A}_{B,D}\otimes\ecat{A}_{A,B})}}$$
また
$$\textstyle F(\id{\ecat{A}_{C,D}}\otimes M_{A,B,C})\mu_{\ecat{A}_{C,D},\ecat{A}_{B,C}\otimes\ecat{A}_{A,B}}=\mu_{\ecat{A}_{C,D},\ecat{A}_{A,C}}(F(\id{\ecat{A}_{C,D}})\otimes F(M_{A,B,C})),$$
である:
$$\xymatrix{{F(\ecat{A}_{C,D})\otimes F(\ecat{A}_{B,C}\otimes\ecat{A}_{A,B})}\ar[rr]^-{\mu_{\ecat{A}_{C,D},\ecat{A}_{B,C}\otimes\ecat{A}_{A,B}}}\ar[d]_-{F(\id{\ecat{A}_{C,D}})\otimes F(M_{A,B,C})}&&{F(\ecat{A}_{C,D}\otimes(\ecat{A}_{B,C}\otimes\ecat{A}_{A,B}))}\ar[d]^-{F(\id{\ecat{A}_{C,D}}\otimes M_{A,B,C})}\\ {F(\ecat{A}_{C,D})\otimes F(\ecat{A}_{A,C})}\ar[rr]_-{\mu_{\ecat{A}_{C,D},\ecat{A}_{A,C}}}&&{F(\ecat{A}_{C,D}\otimes\ecat{A}_{A,C})}}$$命題 2, (2) より
\begin{align} &\,\,\,\,\,\,\,\textstyle F(a_{\ecat{A}_{C,D},\ecat{A}_{B,C},\ecat{A}_{A,B}})\mu_{\ecat{A}_{C,D}\otimes\ecat{A}_{B,C},\ecat{A}_{A,B}}(\mu_{\ecat{A}_{C,D},\ecat{A}_{B,C}}\otimes\id{F(\ecat{A}_{A,B})})\\ &\,\textstyle=\mu_{\ecat{A}_{C,D},\ecat{A}_{B,C}\otimes\ecat{A}_{A,B}}(\id{F(\ecat{A}_{C,D})}\otimes\,\mu_{\ecat{A}_{B,C},\ecat{A}_{A,B}})a_{F(\ecat{A}_{C,D}),F(\ecat{A}_{B,C}),F(\ecat{A}_{A,B})}, \end{align}
である:
$$\xymatrix{{(F(\ecat{A}_{C,D})\otimes F(\ecat{A}_{B,C}))\otimes F(\ecat{A}_{A,B})}\ar[d]_-{\mu_{\ecat{A}_{C,D},\ecat{A}_{B,C}}\otimes\,\id{F(\ecat{A}_{A,B})}}\ar[rrr]^-{a_{F(\ecat{A}_{C,D}),F(\ecat{A}_{B,C}),F(\ecat{A}_{A,B})}}&&&{F(\ecat{A}_{C,D})\otimes(F(\ecat{A}_{B,C})\otimes F(\ecat{A}_{A,B}))}\ar[d]^-{\id{F(\ecat{A}_{C,D})}\,\otimes\,\mu_{\ecat{A}_{B,C},\ecat{A}_{A,B}}}\\ {F(\ecat{A}_{C,D}\otimes\ecat{A}_{B,C})\otimes F(\ecat{A}_{A,B})}\ar[d]_-{\mu_{\ecat{A}_{C,D}\otimes\ecat{A}_{B,C},\ecat{A}_{A,B}}}&&&{F(\ecat{A}_{C,D})\otimes F(\ecat{A}_{B,C}\otimes\ecat{A}_{A,B})}\ar[d]^-{\mu_{\ecat{A}_{C,D},\ecat{A}_{B,C}\otimes\ecat{A}_{A,B}}}\\ {F((\ecat{A}_{C,D}\otimes\ecat{A}_{B,C})\otimes\ecat{A}_{A,B})}\ar[rrr]_-{F(a_{\ecat{A}_{C,D},\ecat{A}_{B,C},\ecat{A}_{A,B}})}&&&{F(\ecat{A}_{C,D}\otimes(\ecat{A}_{B,C}\otimes\ecat{A}_{A,B}))}}$$
また，$\ecat{A}$は$\cat{V}$-圏だから，定義 3.2, (2) より
$$\textstyle M_{A,B,D}(M_{B,C,D}\otimes\id{\ecat{A}_{A,B}})=M_{A,C,D}(\id{\ecat{A}_{C,D}}\otimes M_{A,B,C})a_{\ecat{A}_{C,D},\ecat{A}_{B,C},\ecat{A}_{A,B}},$$
である:
$$\xymatrix{{(\ecat{A}_{C,D}\otimes\ecat{A}_{B,C})\otimes\ecat{A}_{A,B}}\ar[rr]^-{a_{\ecat{A}_{C,D},\ecat{A}_{B,C},\ecat{A}_{A,B}}}\ar[d]_-{M_{B,C,D}\otimes\,\id{\ecat{A}_{A,B}}}&&{\ecat{A}_{C,D}\otimes(\ecat{A}_{B,C}\otimes\ecat{A}_{A,B})}\ar[d]^-{\id{\ecat{A}_{C,D}}\otimes M_{A,B,C}}\\
{\ecat{A}_{B,D}\otimes\ecat{A}_{A,B}}\ar[rd]_-{M_{A,B,D}}&&{\ecat{A}_{C,D}\otimes\ecat{A}_{A,C}}\ar[ld]^-{M_{A,C,D}}\\
&{\ecat{A}_{A,D}}}$$
従って，
- $(F(M_{B,C,D})\mu_{\ecat{A}_{C,D},\ecat{A}_{B,C}})\otimes(\id{F(\ecat{A}_{A,B})}\,\id{F(\ecat{A}_{A,B})})=(F(M_{B,C,D})\otimes\id{F(\ecat{A}_{A,B})})(\mu_{\ecat{A}_{C,D},\ecat{A}_{B,C}}\otimes\id{F(\ecat{A}_{A,B})})$，
- $(\id{F(\ecat{A}_{C,D})}\otimes F(M_{A,B,C}))(\id{F(\ecat{A}_{C,D})}\otimes\,\mu_{\ecat{A}_{B,C},\ecat{A}_{A,B}})=(\id{F(\ecat{A}_{C,D})}\,\id{F(\ecat{A}_{C,D})})\otimes(F(M_{A,B,C})\mu_{\ecat{A}_{B,C},\ecat{A}_{A,B}})$，
- $F(M_{A,B,D})F(M_{B,C,D}\otimes\id{\ecat{A}_{A,B}})=F(M_{A,B,D}(M_{B,C,D}\otimes\id{\ecat{A}_{A,B}}))$，
- $F(M_{A,C,D}(\id{\ecat{A}_{C,D}}\otimes M_{A,B,C})a_{\ecat{A}_{C,D},\ecat{A}_{B,C},\ecat{A}_{A,B}})=F(M_{A,C,D})F((\id{\ecat{A}_{C,D}}\otimes M_{A,B,C})a_{\ecat{A}_{C,D},\ecat{A}_{B,C},\ecat{A}_{A,B}})$，
- $F((\id{\ecat{A}_{C,D}}\otimes M_{A,B,C})a_{\ecat{A}_{C,D},\ecat{A}_{B,C},\ecat{A}_{A,B}})=F(\id{\ecat{A}_{C,D}}\otimes M_{A,B,C})F(a_{\ecat{A}_{C,D},\ecat{A}_{B,C},\ecat{A}_{A,B}})$，
- $\id{F(\ecat{A}_{A,B})}=F(\id{\ecat{A}_{A,B}})$，
- $F(\id{\ecat{A}_{C,D}})=\id{F(\ecat{A}_{C,D})}$，
- $\mu_{\ecat{A}_{B,D},\ecat{A}_{A,B}}(F(M_{B,C,D})\otimes F(\id{\ecat{A}_{A,B}}))=F(M_{B,C,D}\otimes\id{\ecat{A}_{A,B}})\mu_{\ecat{A}_{C,D}\otimes\ecat{A}_{B,C},\ecat{A}_{A,B}},$
- $F(\id{\ecat{A}_{C,D}}\otimes M_{A,B,C})\mu_{\ecat{A}_{C,D},\ecat{A}_{B,C}\otimes\ecat{A}_{A,B}}=\mu_{\ecat{A}_{C,D},\ecat{A}_{A,C}}(F(\id{\ecat{A}_{C,D}})\otimes F(M_{A,B,C}))$，
- \begin{align} &\,\,\,\,\,\,\,\textstyle F(a_{\ecat{A}_{C,D},\ecat{A}_{B,C},\ecat{A}_{A,B}})\mu_{\ecat{A}_{C,D}\otimes\ecat{A}_{B,C},\ecat{A}_{A,B}}(\mu_{\ecat{A}_{C,D},\ecat{A}_{B,C}}\otimes\id{F(\ecat{A}_{A,B})})\\ &\,\textstyle=\mu_{\ecat{A}_{C,D},\ecat{A}_{B,C}\otimes\ecat{A}_{A,B}}(\id{F(\ecat{A}_{C,D})}\otimes\,\mu_{\ecat{A}_{B,C},\ecat{A}_{A,B}})a_{F(\ecat{A}_{C,D}),F(\ecat{A}_{B,C}),F(\ecat{A}_{A,B})}, \end{align}
が成り立つので，
\begin{align}
&\,\,\,\,\,\,\,\,\textstyle M'_{A,B,D}(M'_{B,C,D}\otimes\id{\ecat{A}'_{A,B}})\\
&\,\textstyle=M'_{A,B,D}(M'_{B,C,D}\otimes\id{F(\ecat{A}_{A,B})})\\
&\,\textstyle=F(M_{A,B,D})\mu_{\ecat{A}_{B,D},\ecat{A}_{A,B}}((F(M_{B,C,D})\mu_{\ecat{A}_{C,D},\ecat{A}_{B,C}})\otimes\id{F(\ecat{A}_{A,B})})\\
&\,\textstyle=F(M_{A,B,D})\mu_{\ecat{A}_{B,D},\ecat{A}_{A,B}}((F(M_{B,C,D})\mu_{\ecat{A}_{C,D},\ecat{A}_{B,C}})\otimes(\id{F(\ecat{A}_{A,B})}\,\id{F(\ecat{A}_{A,B})}))\\
&\,\textstyle=F(M_{A,B,D})\mu_{\ecat{A}_{B,D},\ecat{A}_{A,B}}(F(M_{B,C,D})\otimes\id{F(\ecat{A}_{A,B})})(\mu_{\ecat{A}_{C,D},\ecat{A}_{B,C}}\otimes\id{F(\ecat{A}_{A,B})})\\
&\,\textstyle=F(M_{A,B,D})\mu_{\ecat{A}_{B,D},\ecat{A}_{A,B}}(F(M_{B,C,D})\otimes F(\id{\ecat{A}_{A,B}}))(\mu_{\ecat{A}_{C,D},\ecat{A}_{B,C}}\otimes\id{F(\ecat{A}_{A,B})})\\
&\,\textstyle=F(M_{A,B,D})F(M_{B,C,D}\otimes\id{\ecat{A}_{A,B}})\mu_{\ecat{A}_{C,D}\otimes\ecat{A}_{B,C},\ecat{A}_{A,B}}(\mu_{\ecat{A}_{C,D},\ecat{A}_{B,C}}\otimes\id{F(\ecat{A}_{A,B})})\\
&\,\textstyle=F(M_{A,B,D}(M_{B,C,D}\otimes\id{\ecat{A}_{A,B}}))\mu_{\ecat{A}_{C,D}\otimes\ecat{A}_{B,C},\ecat{A}_{A,B}}(\mu_{\ecat{A}_{C,D},\ecat{A}_{B,C}}\otimes\id{F(\ecat{A}_{A,B})})\\
&\,\textstyle=F(M_{A,C,D}(\id{\ecat{A}_{C,D}}\otimes M_{A,B,C})a_{\ecat{A}_{C,D},\ecat{A}_{B,C},\ecat{A}_{A,B}})\mu_{\ecat{A}_{C,D}\otimes\ecat{A}_{B,C},\ecat{A}_{A,B}}(\mu_{\ecat{A}_{C,D},\ecat{A}_{B,C}}\otimes\id{F(\ecat{A}_{A,B})})\\
&\,\textstyle=F(M_{A,C,D})F((\id{\ecat{A}_{C,D}}\otimes M_{A,B,C})a_{\ecat{A}_{C,D},\ecat{A}_{B,C},\ecat{A}_{A,B}})\mu_{\ecat{A}_{C,D}\otimes\ecat{A}_{B,C},\ecat{A}_{A,B}}(\mu_{\ecat{A}_{C,D},\ecat{A}_{B,C}}\otimes\id{F(\ecat{A}_{A,B})})\\
&\,\textstyle=F(M_{A,C,D})F(\id{\ecat{A}_{C,D}}\otimes M_{A,B,C})F(a_{\ecat{A}_{C,D},\ecat{A}_{B,C},\ecat{A}_{A,B}})\mu_{\ecat{A}_{C,D}\otimes\ecat{A}_{B,C},\ecat{A}_{A,B}}(\mu_{\ecat{A}_{C,D},\ecat{A}_{B,C}}\otimes\id{F(\ecat{A}_{A,B})})\\
&\,\textstyle=F(M_{A,C,D})F(\id{\ecat{A}_{C,D}}\otimes M_{A,B,C})F(a_{\ecat{A}_{C,D},\ecat{A}_{B,C},\ecat{A}_{A,B}})\mu_{\ecat{A}_{C,D}\otimes\ecat{A}_{B,C},\ecat{A}_{A,B}}(\mu_{\ecat{A}_{C,D},\ecat{A}_{B,C}}\otimes\id{F(\ecat{A}_{A,B})})\\
&\,\textstyle=F(M_{A,C,D})F(\id{\ecat{A}_{C,D}}\otimes M_{A,B,C})\mu_{\ecat{A}_{C,D},\ecat{A}_{B,C}\otimes\ecat{A}_{A,B}}(\id{F(\ecat{A}_{C,D})}\otimes\,\mu_{\ecat{A}_{B,C},\ecat{A}_{A,B}})a_{F(\ecat{A}_{C,D}),F(\ecat{A}_{B,C}),F(\ecat{A}_{A,B})}\\
&\,\textstyle=F(M_{A,C,D})\mu_{\ecat{A}_{C,D},\ecat{A}_{A,C}}(F(\id{\ecat{A}_{C,D}})\otimes F(M_{A,B,C}))(\id{F(\ecat{A}_{C,D})}\otimes\,\mu_{\ecat{A}_{B,C},\ecat{A}_{A,B}})a_{F(\ecat{A}_{C,D}),F(\ecat{A}_{B,C}),F(\ecat{A}_{A,B})}\\
&\,\textstyle=F(M_{A,C,D})\mu_{\ecat{A}_{C,D},\ecat{A}_{A,C}}(\id{F(\ecat{A}_{C,D})}\otimes F(M_{A,B,C}))(\id{F(\ecat{A}_{C,D})}\otimes\,\mu_{\ecat{A}_{B,C},\ecat{A}_{A,B}})a_{F(\ecat{A}_{C,D}),F(\ecat{A}_{B,C}),F(\ecat{A}_{A,B})}\\
&\,\textstyle=F(M_{A,C,D})\mu_{\ecat{A}_{C,D},\ecat{A}_{A,C}}((\id{F(\ecat{A}_{C,D})}\,\id{F(\ecat{A}_{C,D})})\otimes(F(M_{A,B,C})\mu_{\ecat{A}_{B,C},\ecat{A}_{A,B}}))a_{F(\ecat{A}_{C,D}),F(\ecat{A}_{B,C}),F(\ecat{A}_{A,B})}\\
&\,\textstyle=F(M_{A,C,D})\mu_{\ecat{A}_{C,D},\ecat{A}_{A,C}}(\id{F(\ecat{A}_{C,D})}\otimes(F(M_{A,B,C})\mu_{\ecat{A}_{B,C},\ecat{A}_{A,B}}))a_{F(\ecat{A}_{C,D}),F(\ecat{A}_{B,C}),F(\ecat{A}_{A,B})}\\
&\,\textstyle=F(M_{A,C,D})\mu_{\ecat{A}_{C,D},\ecat{A}_{A,C}}(\id{\ecat{A}'_{C,D}}\otimes(F(M_{A,B,C})\mu_{\ecat{A}_{B,C},\ecat{A}_{A,B}}))a_{\ecat{A}'_{C,D},\ecat{A}'_{B,C},\ecat{A}'_{A,B}}\\
&\,\textstyle=M'_{A,C,D}(\id{\ecat{A}'_{C,D}}\otimes M'_{A,B,C})a_{\ecat{A}'_{C,D},\ecat{A}'_{B,C},\ecat{A}'_{A,B}},
\end{align}
である:
$$\xymatrix{{(\ecat{A}'_{C,D}\otimes\ecat{A}'_{B,C})\otimes\ecat{A}'_{A,B}}\ar[rr]^-{a_{\ecat{A}'_{C,D},\ecat{A}'_{B,C},\ecat{A}'_{A,B}}}\ar[d]_-{M'_{B,C,D}\otimes\,\id{\ecat{A}'_{A,B}}}&&{\ecat{A}'_{C,D}\otimes(\ecat{A}'_{B,C}\otimes\ecat{A}'_{A,B})}\ar[d]^-{\id{\ecat{A}'_{C,D}}\otimes M'_{A,B,C}}\\
{\ecat{A}'_{B,D}\otimes\ecat{A}'_{A,B}}\ar[rd]_-{M'_{A,B,D}}&&{\ecat{A}'_{C,D}\otimes\ecat{A}'_{A,C}}\ar[ld]^-{M'_{A,C,D}}\\
&{\ecat{A}'_{A,D}}}$$
従って，定義 3.2 より$\ecat{A}'=F(\ecat{A})$が$\cat{W}$-圏であることが示された．
まとめ
この記事では，モノイダル圏の間の構造を保つ関手である lax モノイダル関手を定義して，lax モノイダル関手$\func{F}{\cat{V}}{\cat{W}}$と$\cat{V}$-圏$\ecat{A}$を用いて$\cat{W}$-圏$F(\ecat{A})$を自然に構成した．
次の記事では，この構成を元にして，モノイダル圏$\cat{V}$に対して，$\cat{V}$-圏の「underlying category」とよばれる圏を定義する．
追記
- 2022/3/3 13:53 定義 1, (3) の誤植を修正した．
- 2022/3/3 22:49 間違えて削除してしまったので，改めて投稿した．
- 2022/3/3 23:48 参考文献に第4回 (後半) (2) の記事 [ 10 ] を加えた．
- 2022/3/3 23:48 §1 を修正した．