豊穣圏の導入 第4回: Underlying Category について (後半) (1)
前回の記事 [
9
] では，モノイダル圏$\cat{V}$と$\cat{W}$に対して，lax モノイダル関手$\func{F}{\cat{V}}{\cat{W}}$が$\cat{V}$-圏$\ecat{A}$から$\cat{W}$-圏$F(\ecat{A})$を自然に定めることを確認した．
この記事では，モノイダル圏$\cat{V}$に対して，$\cat{V}$から$\set$への自然な lax モノイダル関手を与えることで，$\cat{V}$-圏の「underlying category」とよばれる圏を定義する．
導入
素朴集合論の基礎 (集合と写像，空集合など) に親しみがあり，圏の定義を知っていることを仮定する．
第2回 (前半) の記事 [ 6 ] からは，定義 3，定義 4，命題 1，命題 2，定義 5，定義 7，定義 8，定義 12 を用いており，これらを定義 2.a.3，定義 2.a.4，命題 2.a.1，命題 2.a.2，定義 2.a.5，定義 2.a.7，定義 2.a.8，定義 2.a.12 で表している．
第2回 (後半) の記事 [ 7 ] からは，命題 1，定義 1，定義 2，定義 3，定義 4，命題 2，定義 9 を用いており，これらを命題 2.b.1，定義 2.b.1，定義 2.b.2，定義 2.b.3，定義 2.b.4，命題 2.b.2，定義 2.b.9 で表している．
第3回の記事 [ 7 ] からは，命題 2，命題 3，定義 1，定義 2 を用いており，これらを命題 3.2，命題 3.3，定義 3.1，定義 3.2 で表している．
第4回 (前半) の記事 [ 8 ] からは定義 1，命題 1，定義 2 を用いており，これらを定義 4.a.1，命題 4.a.1，定義 4.a.2 で表している．
$\cat{V}$-圏の underlying category について (続き)
Lax モノイダル関手の性質
まず，$\cat{V}$をモノイダル圏とする．
定義 2.a.3 より$\cat{V}$の恒等関手$\func{\id{\cat{V}}}{\cat{V}}{\cat{V}}$が定まる．
定義 2.a.5 より関手$\func{\id{\cat{V}}\times\id{\cat{V}}}{\cat{V}^2}{\cat{V}^2}$が定まり，各$X,Y\in\cat{V}$に対して
$(\id{\cat{V}}\times\id{\cat{V}})(X,Y)=(\id{\cat{V}}X,\id{\cat{V}}Y)=(X,Y)=\id{\cat{V}^2}(X,Y)$であり，$\cat{V}$での各射$f,g$に対して$(\id{\cat{V}}\times\id{\cat{V}})((f,g))=(\id{\cat{V}}(f),\id{\cat{V}}(g))=(f,g)=\id{\cat{V}^2}((f,g))$だから，$\id{\cat{V}}\times\id{\cat{V}}=\id{\cat{V}^2}$である．
$\cat{V}$のテンソル積$\func{\otimes}{\cat{V}^2}{\cat{V}}$ (定義 2.a.12) に対して，命題 2.a.1 より$\otimes(\id{\cat{V}}\times\id{\cat{V}})=\otimes\,\id{\cat{V}^2}=\otimes$かつ$\id{\cat{V}}\otimes=\otimes$だから，定義 2.a.7 より$\otimes(\id{\cat{V}}\times\id{\cat{V}})$から$\id{\cat{V}}\otimes$への自然変換$\id{\otimes}$が定まる．
$\id{\cat{V}}I=I$だから，$I$から$\id{\cat{V}}I$への$\cat{V}$での射$\id{I}$が定まる．
このとき，以下が成り立つ:
$(\id{\cat{V}},\id{\otimes},\id{I})$は$\cat{V}$から$\cat{V}$への lax モノイダル関手である．
$\cat{V}$での任意の射$\func{f}{X}{X'}$と$\func{g}{Y}{Y'}$に対して，
\begin{align}
(\id{\otimes})_{X',Y'}(\id{\cat{V}}(f)\otimes\id{\cat{V}}(g))
&\,\textstyle=(\id{\otimes})_{X',Y'}(f\otimes g)&(\text{定義 2.a.3})\\
&\,\textstyle=\id{X'\otimes Y'}(f\otimes g)&(\text{定義 2.a.7})\\
&\,\textstyle=f\otimes g\\
&\,\textstyle=(f\otimes g)\id{X\otimes Y}\\
&\,\textstyle=(f\otimes f)(\id{\otimes})_{X,Y}&(\text{定義 2.a.7})\\
&\,\textstyle=\id{\cat{V}}(f\otimes g)(\id{\otimes})_{X,Y},&(\text{定義 2.a.3})
\end{align}
であり，任意の$X,Y,Z\in\cat{V}$に対して，
\begin{align}
\id{\cat{V}}(a_{X,Y,Z})(\id{\otimes})_{X\otimes Y,Z}((\id{\otimes})_{X,Y}\otimes\id{\id{\cat{V}Z}})
&\,\textstyle=\id{\cat{V}}(a_{X,Y,Z})(\id{\otimes})_{X\otimes Y,Z}((\id{\otimes})_{X,Y}\otimes\id{Z})&(\text{定義 2.a.3})\\
&\,\textstyle=a_{X,Y,Z}(\id{\otimes})_{X\otimes Y,Z}((\id{\otimes})_{X,Y}\otimes\id{Z})&(\text{定義 2.a.3})\\
&\,\textstyle=a_{X,Y,Z}\,\id{(X\otimes Y)\otimes Z}(\id{X\otimes Y}\otimes\id{Z})&(\text{定義 2.a.7})\\
&\,\textstyle=a_{X,Y,Z}\,\id{(X\otimes Y)\otimes Z}\,\id{(X\otimes Y)\otimes Z}\\
&\,\textstyle=a_{X,Y,Z}\,\id{(X\otimes Y)\otimes Z}\\
&\,\textstyle=a_{X,Y,Z}\\
&\,\textstyle=\id{X\otimes(Y\otimes Z)}a_{X,Y,Z}\\
&\,\textstyle=\id{X\otimes(Y\otimes Z)}\,\id{X\otimes(Y\otimes Z)}a_{X,Y,Z}\\
&\,\textstyle=\id{X\otimes(Y\otimes Z)}(\id{X}\otimes\id{Y\otimes Z})a_{X,Y,Z}\\
&\,\textstyle=(\id{\otimes})_{X,Y\otimes Z}(\id{X}\otimes(\id{\otimes})_{Y,Z})a_{X,Y,Z}&(\text{定義 2.a.7})\\
&\,\textstyle=(\id{\otimes})_{X,Y\otimes Z}(\id{\id{\cat{V}}X}\otimes(\id{\otimes})_{Y,Z})a_{\id{\cat{V}}X,\id{\cat{V}}Y,\id{\cat{V}}Z},&(\text{定義 2.a.3})
\end{align}
であり，任意の$X\in\cat{V}$に対して，
\begin{align}
\id{\cat{V}}(l_X)(\id{\otimes})_{I,X}(\id{I}\otimes\id{\id{\cat{V}}X})
&\,\textstyle=\id{\cat{V}}(l_X)(\id{\otimes})_{I,X}(\id{I}\otimes\id{X})&(\text{定義 2.a.3})\\
&\,\textstyle=l_X(\id{\otimes})_{I,X}(\id{I}\otimes\id{X})&(\text{定義 2.a.3})\\
&\,\textstyle=l_X\,\id{I\otimes X}(\id{I}\otimes\id{X})&(\text{定義 2.a.7})\\
&\,\textstyle=l_X\,\id{I\otimes X}\,\id{I\otimes X}\\
&\,\textstyle=l_X\,\id{I\otimes X}\\
&\,\textstyle=l_X\\
&\,\textstyle=l_{\id{\cat{V}}X},&(\text{定義 2.a.3})
\end{align}
であり，任意の$X\in\cat{V}$に対して，
\begin{align}
\id{\cat{V}}(r_X)(\id{\otimes})_{X,I}(\id{\id{\cat{V}}X}\otimes\id{I})
&\,\textstyle=\id{\cat{V}}(r_X)(\id{\otimes})_{X,I}(\id{X}\otimes\id{I})&(\text{定義 2.a.3})\\
&\,\textstyle=r_X(\id{\otimes})_{X,I}(\id{X}\otimes\id{I})&(\text{定義 2.a.3})\\
&\,\textstyle=r_X\,\id{X\otimes I}(\id{X}\otimes\id{I})&(\text{定義 2.a.7})\\
&\,\textstyle=r_X\,\id{X\otimes I}\,\id{X\otimes I}\\
&\,\textstyle=r_X\,\id{X\otimes I}\\
&\,\textstyle=r_X\\
&\,\textstyle=r_{\id{\cat{V}}X},&(\text{定義 2.a.3})
\end{align}
である．
ゆえに，命題 1 より$(\id{\cat{V}},\id{\otimes},\id{I})$は$\cat{V}$から$\cat{V}$へのモノイダル関手である．
$(\id{\cat{V}},\id{\otimes},\id{I})$を$\id{\cat{V}}$で表し，$\cat{V}$の恒等 lax モノイダル関手 (identity lax monoidal functor) という．
次に，$\func{G=(G,\mu^G,e^G)}{\cat{V}}{\cat{W}}$と$\func{F=(F,\mu^F,e^F)}{\cat{U}}{\cat{V}}$を lax モノイダル関手とする．
$G$は$\cat{V}$から$\cat{W}$への関手であり，$F$は$\cat{U}$から$\cat{V}$への関手だから，定義 2.a.4 より$G$と$F$の合成$\func{GF}{\cat{U}}{\cat{W}}$が定まる．
$\mu^F$は$\func{\otimes(F\times F)}{\cat{U}^2}{\cat{V}}$から$\func{F\otimes}{\cat{U}^2}{\cat{V}}$への自然変換であり，$G$は$\cat{V}$から$\cat{W}$への関手だから，定義 2.b.9, (1) より$\func{G(\otimes(F\times F))}{\cat{U}^2}{\cat{W}}$から$\func{G(F\otimes)}{\cat{U}^2}{\cat{W}}$への自然変換$G(\mu^F)$が定まる．
$\mu^G$は$\func{\otimes(G\times G)}{\cat{V}^2}{\cat{W}}$から$\func{G\otimes}{\cat{V}^2}{\cat{W}}$への自然変換であり，$F$は$\cat{U}$から$\cat{V}$への関手だから，定義 2.a.5 より関手$\func{F\times F}{\cat{U}^2}{\cat{V}^2}$が定まり，定義 2.b.9, (2) より$\func{(\otimes(G\times G))(F\times F)}{\cat{U}^2}{\cat{W}}$から$\func{(G\otimes)(F\times F)}{\cat{U}^2}{\cat{W}}$への自然変換$(\mu^G)(F\times F)$が定まる．
各$X,Y\in\cat{U}$に対して
$$\textstyle((G\times G)(F\times F))(X,Y)=(G\times G)((F\times F)(X,Y))=(G\times G)(FX,FY)=(G(FX),G(FY))=((GF)X,(GF)Y)=((GF)\times(GF))(X,Y),$$
であり，$\cat{U}$での各射$f,g$に対して
$$\textstyle((G\times G)(F\times F))((f,g))=(G\times G)((F\times F)((f,g)))=(G\times G)(F(f),F(g))=(G(F(f)),G(F(g)))=((GF)(f),(GF)(g))=((GF)\times(GF))((f,g)),$$
だから，$(G\times G)(F\times F)=(GF)\times(GF)$であり，命題 2.a.2 より$(\otimes(G\times G))(F\times F)=\otimes((G\times G)(F\times F))=\otimes((GF)\times(GF))$であり，$(G\otimes)(F\times F)=G(\otimes(F\times F))$であり，$G(F\otimes)=(GF)\otimes$だから，定義 2.a.8 より$G(\mu^F)$と$(\mu^G)(F\times F)$の垂直合成$G(\mu^F)\cdot(\mu^G)(F\times F)$が$\otimes((GF)\times(GF))$から$(GF)\otimes$への自然変換として定まる．
これを$\mu^{GF}$で表す:
$$\xymatrix{{\otimes((GF)\times(GF))}\ar[rr]^-{(\mu^G)(F\times F)}\ar[rrd]_-{\mu^{GF}}&&{G\otimes(F\times F)}\ar[d]^-{G(\mu^F)}\\
&&{(GF)\otimes}}$$
$e^F$は$I$から$FI$への$\cat{V}$での射であり，$G$は$\cat{V}$から$\cat{W}$への関手だから，$G(e^F)$は$GI$から$G(FI)=(GF)I$への$\cat{W}$での射である．
$e^G$は$I$から$GI$への$\cat{W}$での射である．
ゆえに，$G(e^F)$と$e^G$の合成$G(e^F)e^G$が$I$から$(GF)I$への写像として定まる．
これを$e^{GF}$で表す:
$$\xymatrix{I\ar[r]^-{e^G}\ar[rd]_-{e^{GF}}&{FI}\ar[d]^-{G(e^F)}\\
&{(GF)I}}$$
$(GF,\mu^{GF},e^{GF})$は$\cat{U}$から$\cat{W}$への lax モノイダル関手である．
$X,Y\in\cat{U}$に対して，
\begin{align}
(\mu^{GF})_{X,Y}
&\,\textstyle=(G(\mu^F)\cdot(\mu^G)(F\times F))_{X,Y}\\
&\,\textstyle=(G(\mu^F))_{X,Y}((\mu^G)(F\times F))_{X,Y}&(\text{定義 2.a.8})\\
&\,\textstyle=G((\mu^F)_{X,Y})((\mu^G)(F\times F))_{X,Y}&(\text{定義 2.b.9, (1)})\\
&\,\textstyle=G((\mu^F)_{X,Y})(\mu^G)_{(F\times F)(X,Y)}&(\text{定義 2.b.9, (2)})\\
&\,\textstyle=G((\mu^F)_{X,Y})(\mu^G)_{FX,FY},&(\text{定義 2.a.5})
\end{align}
である．
$\cat{U}$での射$\func{f}{X}{X'}$と$\func{g}{Y}{Y'}$を任意に取る．
$G=(G,\mu^G,e^G)$は$\cat{V}$から$\cat{W}$への lax モノイダル関手だから，定義 4.a.1 より$G$は$\cat{V}$から$\cat{W}$への関手であり，
$$\textstyle G((\mu^F)_{X',Y'})G(F(f)\otimes F(g))=G((\mu^F)_{X',Y'}(F(f)\otimes F(g))),$$
であり，
$$\textstyle G(F(f\otimes g)(\mu^F)_{X,Y})=G(F(f\otimes g))G((\mu^F)_{X,Y}),$$
である．また，命題 4.a.1, (1) より
$$\textstyle(\mu^G)_{FX',FY'}(G(F(f))\otimes G(F(g)))=G(F(f)\otimes F(g))(\mu^G)_{FX,FY},$$
である．
一方で，$F=(F,\mu^F,e^F)$は$\cat{U}$から$\cat{V}$への lax モノイダル関手だから，命題 4.a.1, (1) より
$$\textstyle(\mu^F)_{X',Y'}(F(f)\otimes F(g))=F(f\otimes g)(\mu^F)_{X,Y},$$
である．
ゆえに，
\begin{align}
(\mu^{GF})_{X',Y'}((GF)(f)\otimes(GF)(g))
&\,\textstyle=G((\mu^F)_{X',Y'})(\mu^G)_{FX',FY'}((GF)(f)\otimes(GF)(g))\\
&\,\textstyle=G((\mu^F)_{X',Y'})(\mu^G)_{FX',FY'}(G(F(f))\otimes G(F(g)))&(\text{定義 2.a.4})\\
&\,\textstyle=G((\mu^F)_{X',Y'})G(F(f)\otimes F(g))(\mu^G)_{FX,FY}\\
&\,\textstyle=G((\mu^F)_{X',Y'}(F(f)\otimes F(g)))(\mu^G)_{FX,FY}\\
&\,\textstyle=G(F(f\otimes g)(\mu^F)_{X,Y})(\mu^G)_{FX,FY}\\
&\,\textstyle=G(F(f\otimes g))G((\mu^F)_{X,Y})(\mu^G)_{FX,FY}\\
&\,\textstyle=(GF)(f\otimes g)G((\mu^F)_{X,Y})(\mu^G)_{FX,FY}&(\text{定義 2.a.4})\\
&\,\textstyle=(GF)(f\otimes g)(\mu^{GF})_{X,Y},
\end{align}
である．
$X,Y,Z\in\cat{U}$を任意に取る．
$\func{\otimes}{\cat{W}^2}{\cat{W}}$は関手だから，
$$\textstyle(G((\mu^F)_{X,Y})(\mu^G)_{FX,FY})\otimes(\id{G(FZ)}\,\id{G(FZ)})=(G((\mu^F)_{X,Y})\otimes\id{G(FZ)})((\mu^G)_{FX,FY}\otimes\id{G(FZ)}),$$
である．
$G=(G,\mu^G,e^G)$は$\cat{V}$から$\cat{W}$への lax モノイダル関手だから，定義 4.a.1 より$G$は$\cat{V}$から$\cat{W}$への関手であり，$G(F(a_{X,Y,Z}))G((\mu^F)_{X\otimes Y,Z})=G(F(a_{X,Y,Z})(\mu^F)_{X\otimes Y,Z})$かつ
$$\textstyle G(F(a_{X,Y,Z})(\mu^F)_{X\otimes Y,Z})G((\mu^F)_{X,Y}\otimes\id{FZ})=G(F(a_{X,Y,Z})(\mu^F)_{X\otimes Y,Z}((\mu^F)_{X,Y}\otimes\id{FZ})),$$
かつ
$$\textstyle G((\mu^F)_{X,Y\otimes Z}(\id{FX}\otimes(\mu^F)_{Y,Z})a_{FX,FY,FZ})=G((\mu^F)_{X,Y\otimes Z}(\id{FX}\otimes(\mu^F)_{Y,Z}))G(a_{FX,FY,FZ}),$$
かつ$G((\mu^F)_{X,Y\otimes Z}(\id{FX}\otimes(\mu^F)_{Y,Z}))=G((\mu^F)_{X,Y\otimes Z})G(\id{FX}\otimes(\mu^F)_{Y,Z})$かつ$\id{G(FZ)}=G(\id{FZ})$かつ$G(\id{FX})=\id{G(FX)}$である．また，命題 4.a.1, (1) より
$$\textstyle(\mu^G)_{F(X\otimes Y),FZ}(G((\mu^F)_{X,Y})\otimes G(\id{FZ}))=G((\mu^F)_{X,Y}\otimes\id{FZ})(\mu^G)_{FX\otimes FY,FZ},$$
かつ
$$\textstyle G(\id{FX}\otimes(\mu^F)_{Y,Z})(\mu^G)_{FX,FY\otimes FZ}=(\mu^G)_{FX,F(Y\otimes Z)}(G(\id{FX})\otimes G((\mu^F)_{Y,Z})),$$
であり，命題 4.a.1, (2) より
$$\textstyle G(a_{FX,FY,FZ})(\mu^G)_{FX\otimes FY,FZ}((\mu^G)_{FX,FY}\otimes\id{G(FZ)})=(\mu^G)_{FX,FY\otimes FZ}(\id{G(FX)}\otimes(\mu^G)_{FY,FZ})a_{G(FX),G(FY),G(FZ)},$$
である．
一方で，$F=(F,\mu^F,e^F)$は$\cat{U}$から$\cat{V}$への lax モノイダル関手だから，命題 4.a.1, (2) より
$$\textstyle F(a_{X,Y,Z})(\mu^F)_{X\otimes Y,Z}((\mu^F)_{X,Y}\otimes\id{FZ})=(\mu^F)_{X,Y\otimes Z}(\id{FX}\otimes(\mu^F)_{Y,Z})a_{FX,FY,FZ},$$
である．
ゆえに，
\begin{align}
&\,\,\,\,\,\,\,\textstyle(GF)(a_{X,Y,Z})(\mu^{GF})_{X\otimes Y,Z}((\mu^{GF})_{X,Y}\otimes\id{(GF)Z})\\
&\,\textstyle=(GF)(a_{X,Y,Z})G((\mu^F)_{X\otimes Y,Z})(\mu^G)_{F(X\otimes Y),FZ}((G((\mu^F)_{X,Y})(\mu^G)_{FX,FY})\otimes\id{(GF)Z})\\
&\,\textstyle=(GF)(a_{X,Y,Z})G((\mu^F)_{X\otimes Y,Z})(\mu^G)_{F(X\otimes Y),FZ}((G((\mu^F)_{X,Y})(\mu^G)_{FX,FY})\otimes\id{G(FZ)})&(\text{定義 2.a.4})\\
&\,\textstyle=G(F(a_{X,Y,Z}))G((\mu^F)_{X\otimes Y,Z})(\mu^G)_{F(X\otimes Y),FZ}((G((\mu^F)_{X,Y})(\mu^G)_{FX,FY})\otimes\id{G(FZ)})&(\text{定義 2.a.4})\\
&\,\textstyle=G(F(a_{X,Y,Z}))G((\mu^F)_{X\otimes Y,Z})(\mu^G)_{F(X\otimes Y),FZ}((G((\mu^F)_{X,Y})(\mu^G)_{FX,FY})\otimes(\id{G(FZ)}\,\id{G(FZ)}))\\
&\,\textstyle=G(F(a_{X,Y,Z}))G((\mu^F)_{X\otimes Y,Z})(\mu^G)_{F(X\otimes Y),FZ}(G((\mu^F)_{X,Y})\otimes\id{G(FZ)})((\mu^G)_{FX,FY}\otimes\id{G(FZ)})\\
&\,\textstyle=G(F(a_{X,Y,Z}))G((\mu^F)_{X\otimes Y,Z})(\mu^G)_{F(X\otimes Y),FZ}(G((\mu^F)_{X,Y})\otimes G(\id{FZ}))((\mu^G)_{FX,FY}\otimes\id{G(FZ)})\\
&\,\textstyle=G(F(a_{X,Y,Z}))G((\mu^F)_{X\otimes Y,Z})G((\mu^F)_{X,Y}\otimes\id{FZ})(\mu^G)_{FX\otimes FY,FZ}((\mu^G)_{FX,FY}\otimes\id{G(FZ)})\\
&\,\textstyle=G(F(a_{X,Y,Z})(\mu^F)_{X\otimes Y,Z})G((\mu^F)_{X,Y}\otimes\id{FZ})(\mu^G)_{FX\otimes FY,FZ}((\mu^G)_{FX,FY}\otimes\id{G(FZ)})\\
&\,\textstyle=G(F(a_{X,Y,Z})(\mu^F)_{X\otimes Y,Z}((\mu^F)_{X,Y}\otimes\id{FZ}))(\mu^G)_{FX\otimes FY,FZ}((\mu^G)_{FX,FY}\otimes\id{G(FZ)})\\
&\,\textstyle=G((\mu^F)_{X,Y\otimes Z}(\id{FX}\otimes(\mu^F)_{Y,Z})a_{FX,FY,FZ})(\mu^G)_{FX\otimes FY,FZ}((\mu^G)_{FX,FY}\otimes\id{G(FZ)})\\
&\,\textstyle=G((\mu^F)_{X,Y\otimes Z}(\id{FX}\otimes(\mu^F)_{Y,Z}))G(a_{FX,FY,FZ})(\mu^G)_{FX\otimes FY,FZ}((\mu^G)_{FX,FY}\otimes\id{G(FZ)})\\
&\,\textstyle=G((\mu^F)_{X,Y\otimes Z})G(\id{FX}\otimes(\mu^F)_{Y,Z})G(a_{FX,FY,FZ})(\mu^G)_{FX\otimes FY,FZ}((\mu^G)_{FX,FY}\otimes\id{G(FZ)})\\
&\,\textstyle=G((\mu^F)_{X,Y\otimes Z})G(\id{FX}\otimes(\mu^F)_{Y,Z})(\mu^G)_{FX,FY\otimes FZ}(\id{G(FX)}\otimes(\mu^G)_{FY,FZ})a_{G(FX),G(FY),G(FZ)}\\
&\,\textstyle=G((\mu^F)_{X,Y\otimes Z})(\mu^G)_{FX,F(Y\otimes Z)}(G(\id{FX})\otimes G((\mu^F)_{Y,Z}))(\id{G(FX)}\otimes(\mu^G)_{FY,FZ})a_{G(FX),G(FY),G(FZ)}\\
&\,\textstyle=G((\mu^F)_{X,Y\otimes Z})(\mu^G)_{FX,F(Y\otimes Z)}(\id{G(FX)}\otimes G((\mu^F)_{Y,Z}))(\id{G(FX)}\otimes(\mu^G)_{FY,FZ})a_{G(FX),G(FY),G(FZ)}\\
&\,\textstyle=G((\mu^F)_{X,Y\otimes Z})(\mu^G)_{FX,F(Y\otimes Z)}((\id{G(FX)}\,\id{G(FX)})\otimes(G((\mu^F)_{Y,Z})(\mu^G)_{FY,FZ}))a_{G(FX),G(FY),G(FZ)}\\
&\,\textstyle=G((\mu^F)_{X,Y\otimes Z})(\mu^G)_{FX,F(Y\otimes Z)}(\id{G(FX)}\otimes(G((\mu^F)_{Y,Z})(\mu^G)_{FY,FZ}))a_{G(FX),G(FY),G(FZ)}\\
&\,\textstyle=G((\mu^F)_{X,Y\otimes Z})(\mu^G)_{FX,F(Y\otimes Z)}(\id{(GF)X}\otimes(G((\mu^F)_{Y,Z})(\mu^G)_{FY,FZ}))a_{(GF)X,(GF)Y,(GF)Z}&(\text{定義 2.a.4})\\
&\,\textstyle=(\mu^{GF})_{X,Y\otimes Z}(\id{(GF)X}\otimes(\mu^{GF})_{Y,Z})a_{(GF)X,(GF)Y,(GF)Z},
\end{align}
である．
$X\in\cat{U}$を任意に取る．
$\otimes$は$\cat{W}^2$から$\cat{W}$への関手だから，
$$\textstyle(G(e^F)e^G)\otimes(\id{G(FX)}\,\id{G(FX)})=(G(e^F)\otimes\id{G(FX)})(e^G\otimes\id{G(FX)}),$$
である．
$G=(G,\mu^G,e^G)$は$\cat{V}$から$\cat{W}$への lax モノイダル関手だから，定義 4.a.1 より$G$は$\cat{V}$から$\cat{W}$への関手であり，$G(F(l_X))G((\mu^F)_{I,X})=G(F(l_X)(\mu^F)_{I,X})$かつ
$$\textstyle G(F(l_X)(\mu^F)_{I,X})G(e^F\otimes\id{FX})=G(F(l_X)(\mu^F)_{I,X}(e^F\otimes\id{FX})),$$
かつ$\id{G(FX)}=G(\id{FX})$である．また，命題 4.a.1, (1) より
$$\textstyle(\mu^G)_{FI,FX}(G(e^F)\otimes G(\id{FX}))=G(e^F\otimes\id{FX})(\mu^G)_{I,FX},$$
であり，命題 4.a.1, (3) より
$$\textstyle G(l_{FX})(\mu^G)_{I,FX}(e^G\otimes\id{G(FX)})=l_{G(FX)},$$
である．
一方で，$F=(F,\mu^F,e^F)$は$\cat{U}$から$\cat{V}$への lax モノイダル関手だから，命題 4.a.1, (3) より
$$\textstyle F(l_X)(\mu^F)_{I,X}(e^F\otimes\id{FX})=l_{FX},$$
である．
ゆえに，
\begin{align}
&\,\,\,\,\,\,\,\textstyle(GF)(l_X)(\mu^{GF})_{I,X}(e^{GF}\otimes\id{(GF)X})\\
&\,\textstyle=(GF)(l_X)G((\mu^F)_{I,X})(\mu^G)_{FI,FX}(e^{GF}\otimes\id{(GF)X})\\
&\,\textstyle=(GF)(l_X)G((\mu^F)_{I,X})(\mu^G)_{FI,FX}((G(e^F)e^G)\otimes\id{(GF)X})\\
&\,\textstyle=(GF)(l_X)G((\mu^F)_{I,X})(\mu^G)_{FI,FX}((G(e^F)e^G)\otimes\id{G(FX)})&(\text{定義 2.a.4})\\
&\,\textstyle=G(F(l_X))G((\mu^F)_{I,X})(\mu^G)_{FI,FX}((G(e^F)e^G)\otimes\id{G(FX)})&(\text{定義 2.a.4})\\
&\,\textstyle=G(F(l_X))G((\mu^F)_{I,X})(\mu^G)_{FI,FX}((G(e^F)e^G)\otimes(\id{G(FX)}\,\id{G(FX)}))\\
&\,\textstyle=G(F(l_X))G((\mu^F)_{I,X})(\mu^G)_{FI,FX}(G(e^F)\otimes\id{G(FX)})(e^G\otimes\id{G(FX)})\\
&\,\textstyle=G(F(l_X))G((\mu^F)_{I,X})(\mu^G)_{FI,FX}(G(e^F)\otimes G(\id{FX}))(e^G\otimes\id{G(FX)})\\
&\,\textstyle=G(F(l_X))G((\mu^F)_{I,X})G(e^F\otimes\id{FX})(\mu^G)_{I,FX}(e^G\otimes\id{G(FX)})\\
&\,\textstyle=G(F(l_X)(\mu^F)_{I,X})G(e^F\otimes\id{FX})(\mu^G)_{I,FX}(e^G\otimes\id{G(FX)})\\
&\,\textstyle=G(F(l_X)(\mu^F)_{I,X}(e^F\otimes\id{FX}))(\mu^G)_{I,FX}(e^G\otimes\id{G(FX)})\\
&\,\textstyle=G(l_{FX})(\mu^G)_{I,FX}(e^G\otimes\id{G(FX)})\\
&\,\textstyle=l_{G(FX)}\\
&\,\textstyle=l_{(GF)X},&(\text{定義 2.a.4})
\end{align}
である．
$X\in\cat{U}$を任意に取る．
$\otimes$は$\cat{W}^2$から$\cat{W}$への関手だから，
$$\textstyle(\id{G(FX)}\,\id{G(FX)})\otimes(G(e^F)e^G)=(\id{G(FX)}\otimes G(e^F))(\id{G(FX)}\otimes e^G),$$
である．
$G=(G,\mu^G,e^G)$は$\cat{V}$から$\cat{W}$への lax モノイダル関手だから，定義 4.a.1 より$G$は$\cat{V}$から$\cat{W}$への関手であり，$G(F(r_X))G((\mu^F)_{X,I})=G(F(r_X)(\mu^F)_{X,I})$かつ
$$\textstyle G(F(r_X)(\mu^F)_{X,I})G(\id{FX}\otimes e^F)=G(F(r_X)(\mu^F)_{X,I}(\id{FX}\otimes e^F)),$$
かつ$\id{G(FX)}=G(\id{FX})$である．また，命題 4.a.1, (1) より
$$\textstyle(\mu^G)_{FX,FI}(G(\id{FX})\otimes G(e^F))=G(\id{FX}\otimes e^F)(\mu^G)_{FX,I},$$
であり，命題 4.a.1, (4) より
$$\textstyle G(r_{FX})(\mu^G)_{FX,I}(\id{G(FX)}\otimes e^G)=r_{G(FX)},$$
である．
一方で，$F=(F,\mu^F,e^F)$は$\cat{U}$から$\cat{V}$への lax モノイダル関手だから，命題 4.a.1, (4) より
$$\textstyle F(r_X)(\mu^F)_{X,I}(\id{FX}\otimes e^F)=r_{FX},$$
である．
ゆえに，
\begin{align}
&\,\,\,\,\,\,\,\textstyle(GF)(r_X)(\mu^{GF})_{X,I}(\id{(GF)X}\otimes e^{GF})\\
&\,\textstyle=(GF)(r_X)G((\mu^F)_{X,I})(\mu^G)_{FX,FI}(\id{(GF)X}\otimes e^{GF})\\
&\,\textstyle=(GF)(r_X)G((\mu^F)_{X,I})(\mu^G)_{FX,FI}(\id{(GF)X}\otimes(G(e^F)e^G))\\
&\,\textstyle=(GF)(r_X)G((\mu^F)_{X,I})(\mu^G)_{FX,FI}(\id{G(FX)}\otimes(G(e^F)e^G))&(\text{定義 2.a.4})\\
&\,\textstyle=G(F(r_X))G((\mu^F)_{X,I})(\mu^G)_{FX,FI}(\id{G(FX)}\otimes(G(e^F)e^G))&(\text{定義 2.a.4})\\
&\,\textstyle=G(F(r_X))G((\mu^F)_{X,I})(\mu^G)_{FX,FI}((\id{G(FX)}\,\id{G(FX)})\otimes(G(e^F)e^G))\\
&\,\textstyle=G(F(r_X))G((\mu^F)_{X,I})(\mu^G)_{FX,FI}(\id{G(FX)}\otimes G(e^F))(\id{G(FX)}\otimes e^G)\\
&\,\textstyle=G(F(r_X))G((\mu^F)_{X,I})(\mu^G)_{FX,FI}(G(\id{FX})\otimes G(e^F))(\id{G(FX)}\otimes e^G)\\
&\,\textstyle=G(F(r_X))G((\mu^F)_{X,I})G(\id{FX}\otimes e^F)(\mu^G)_{FX,I}(\id{G(FX)}\otimes e^G)\\
&\,\textstyle=G(F(r_X)(\mu^F)_{X,I})G(\id{FX}\otimes e^F)(\mu^G)_{FX,I}(\id{G(FX)}\otimes e^G)\\
&\,\textstyle=G(F(r_X)(\mu^F)_{X,I}(\id{FX}\otimes e^F))(\mu^G)_{FX,I}(\id{G(FX)}\otimes e^G)\\
&\,\textstyle=G(r_{FX})(\mu^G)_{FX,I}(\id{G(FX)}\otimes e^G)\\
&\,\textstyle=r_{G(FX)}\\
&\,\textstyle=r_{(GF)X},&(\text{定義 2.a.4})
\end{align}
である．
ゆえに，命題 1 より$(GF,\mu^{GF},e^{GF})$は$\cat{U}$から$\cat{W}$へのモノイダル関手である．
$(GF,\mu^{GF},e^{GF})=(GF,G(\mu^F)\cdot(\mu^G)(F\times F),G(e^F)e^G)$を$GF$で表し，$G$と$F$の (lax モノイダル関手としての) 合成 (composition) という．
Lax モノイダル関手$\func{F=(F,\mu,e)}{\cat{V}}{\cat{W}}$に対して，lax モノイダル関手として$\id{\cat{W}}F=F=F\,\id{\cat{V}}$が成り立つ．
\begin{align}
\id{\cat{W}}F
&\,\textstyle=\id{\cat{W}}(F,\mu,e)\\
&\,\textstyle=(\id{\cat{W}},\id{\otimes},\id{I})(F,\mu,e)&(\text{命題 1})\\
&\,\textstyle=(\id{\cat{W}}F,\id{\cat{W}}\mu\cdot\id{\otimes}(F\times F),\id{\cat{W}}(e)\,\id{I})&(\text{命題 2})\\
&\,\textstyle=(\id{\cat{W}}F,\id{\cat{W}}\mu\cdot\id{\otimes}(F\times F),\id{\cat{W}}(e))\\
&\,\textstyle=(\id{\cat{W}}F,\id{\cat{W}}\mu\cdot\id{\otimes}(F\times F),e)&(\text{定義 2.a.3})\\
&\,\textstyle=(F,\id{\cat{W}}\mu\cdot\id{\otimes}(F\times F),e),&(\text{命題 2.a.1})\\
\end{align}
である．
各$X,Y\in\cat{V}$に対して，命題 2 の証明で述べたように，
$$\textstyle(\id{\cat{W}}\mu\cdot\id{\otimes}(F\times F))_{X,Y}=\id{\cat{W}}(\mu_{X,Y})(\id{\otimes})_{FX,FY},$$
であり，
\begin{align}
(\id{\cat{W}}\mu\cdot\id{\otimes}(F\times F))_{X,Y}
&\,\textstyle=\id{\cat{W}}(\mu_{X,Y})(\id{\otimes})_{FX,FY}\\
&\,\textstyle=\id{\cat{W}}(\mu_{X,Y})\,\id{FX\otimes FY}&(\text{定義 2.a.7})\\
&\,\textstyle=\id{\cat{W}}(\mu_{X,Y})\\
&\,\textstyle=\mu_{X,Y},&(\text{定義 2.a.3})
\end{align}
だから，$\id{\cat{W}}\mu\cdot\id{\otimes}(F\times F)=\mu$であり，$\id{\cat{W}}F=(F,\mu,e)=F$である．
また，$F$は$\cat{V}$から$\cat{W}$への lax モノイダル関手だから，定義 4.a.1 より$F$は$\cat{V}$から$\cat{W}$への関手であり，$F(\id{I})=\id{FI}$であり，$F(\id{X\otimes Y})=\id{F(X\otimes Y)}$である．
ゆえに，
\begin{align}
F\,\id{\cat{V}}
&\,\textstyle=(F,\mu,e)\,\id{\cat{V}}\\
&\,\textstyle=(F,\mu,e)(\id{\cat{V}},\id{\otimes},\id{I})&(\text{命題 1})\\
&\,\textstyle=(F\,\id{\cat{V}},F(\id{\otimes})\cdot\mu(\id{\cat{V}}\times\id{\cat{V}}),F(\id{I})e)&(\text{命題 2})\\
&\,\textstyle=(F\,\id{\cat{V}},F(\id{\otimes})\cdot\mu(\id{\cat{V}}\times\id{\cat{V}}),\id{FI}e)\\
&\,\textstyle=(F\,\id{\cat{V}},F(\id{\otimes})\cdot\mu(\id{\cat{V}}\times\id{\cat{V}}),e),\\
&\,\textstyle=(F,F(\id{\otimes})\cdot\mu(\id{\cat{V}}\times\id{\cat{V}}),e),&(\text{命題 2.a.1})
\end{align}
である．
各$X,Y\in\cat{V}$に対して，命題 2 の証明で述べたように，
$$\textstyle(F(\id{\otimes})\cdot\mu(\id{\cat{V}}\times\id{\cat{V}}))_{X,Y}=F((\id{\otimes})_{X,Y})\mu_{\id{\cat{V}}X,\id{\cat{V}}Y},$$
であり，
\begin{align}
(F(\id{\otimes})\cdot\mu(\id{\cat{V}}\times\id{\cat{V}}))_{X,Y}
&\,\textstyle=F((\id{\otimes})_{X,Y})\mu_{\id{\cat{V}}X,\id{\cat{V}}Y}\\
&\,\textstyle=F((\id{\otimes})_{X,Y})\mu_{X,Y}&(\text{定義 2.a.3})\\
&\,\textstyle=F(\id{X\otimes Y})\mu_{X,Y}&(\text{定義 2.a.7})\\
&\,\textstyle=\id{F(X\otimes Y)}\,\mu_{X,Y}\\
&\,\textstyle=\mu_{X,Y},
\end{align}
だから，$F(\id{\otimes})\cdot\mu(\id{\cat{V}}\times\id{\cat{V}})=\mu$であり，$F\,\id{\cat{V}}=(F,\mu,e)=F$である．
Lax モノイダル関手$\func{H=(H,\mu^H,e^H)}{\cat{W}}{\cat{X}}$と$\func{G=(G,\mu^G,e^G)}{\cat{V}}{\cat{W}}$と$\func{F=(F,\mu^F,e^F)}{\cat{U}}{\cat{V}}$に対して，lax モノイダル関手として$H(GF)=(HG)F$が成り立つ．
$X,Y\in\cat{U}$を取る．命題 2 の証明で述べたように，
$$\textstyle(H(\mu^{GF})\cdot\mu^H((GF)\times(GF)))_{X,Y}=H((\mu^{GF})_{X,Y})(\mu^H)_{(GF)X,(GF)Y},$$
かつ$(\mu^{GF})_{X,Y}=G((\mu^F)_{X,Y})(\mu^G)_{FX,FY}$かつ$H((\mu^G)_{FX,FY})(\mu^H)_{G(FX),G(FY)}=(\mu^{HG})_{FX,FY}$
$$\textstyle(HG)((\mu^F)_{X,Y})(\mu^{HG})_{FX,FY}=((HG)(\mu^F)\cdot\mu^{HG}(F\times F))_{X,Y},$$
である．
また，$H$が$\cat{W}$から$\cat{X}$への lax モノイダル関手であることから，定義 4.a.1 より$H$は$\cat{W}$から$\cat{X}$への関手であり，
$$\textstyle H(G((\mu^F)_{X,Y})(\mu^G)_{FX,FY})=H(G((\mu^F)_{X,Y}))H((\mu^G)_{FX,FY}),$$
である．
ゆえに，
\begin{align}
(H(\mu^{GF})\cdot\mu^H((GF)\times(GF)))_{X,Y}
&\,\textstyle=H((\mu^{GF})_{X,Y})(\mu^H)_{(GF)X,(GF)Y}\\
&\,\textstyle=H(G((\mu^F)_{X,Y})(\mu^G)_{FX,FY})(\mu^H)_{(GF)X,(GF)Y}\\
&\,\textstyle=H(G((\mu^F)_{X,Y}))H((\mu^G)_{FX,FY})(\mu^H)_{(GF)X,(GF)Y}\\
&\,\textstyle=H(G((\mu^F)_{X,Y}))H((\mu^G)_{FX,FY})(\mu^H)_{G(FX),G(FY)}&(\text{定義 2.a.4})\\
&\,\textstyle=(HG)((\mu^F)_{X,Y})H((\mu^G)_{FX,FY})(\mu^H)_{G(FX),G(FY)}&(\text{定義 2.a.4})\\
&\,\textstyle=(HG)((\mu^F)_{X,Y})(\mu^{HG})_{FX,FY}\\
&\,\textstyle=((HG)(\mu^F)\cdot\mu^{HG}(F\times F))_{X,Y},
\end{align}
であり，$H(\mu^{GF})\cdot\mu^H((GF)\times(GF))=(HG)(\mu^F)\cdot\mu^{HG}(F\times F)$である．
また，$H$が$\cat{W}$から$\cat{X}$への lax モノイダル関手であることから，定義 4.a.1 より$H$は$\cat{W}$から$\cat{X}$への関手であり，$H(G(e^F)e^G)=H(G(e^F))H(e^G)$であり，
\begin{align}
H(e^{GF})e^H
&\,\textstyle=H(G(e^F)e^G)e^H&(\text{命題 2})\\
&\,\textstyle=H(G(e^F))H(e^G)e^H\\
&\,\textstyle=(HG)(e^F)H(e^G)e^H&(\text{定義 2.a.4})\\
&\,\textstyle=(HG)(e^F)e^{HG},(\text{命題 2})
\end{align}
である．
従って，
\begin{align}
H(GF)
&\,\textstyle=(H,\mu^H,e^H)((G,\mu^G,e^G)(F,\mu^F,e^F))\\
&\,\textstyle=(H,\mu^H,e^H)(GF,\mu^{GF},e^{GF})\\
&\,\textstyle=(H(GF),H(\mu^{GF})\cdot\mu^H((GF)\times(GF)),H(e^{GF})e^H)\\
&\,\textstyle=((HG)F,H(\mu^{GF})\cdot\mu^H((GF)\times(GF)),H(e^{GF})e^H)&(\text{命題 2.a.2})\\
&\,\textstyle=((HG)F,(HG)(\mu^F)\cdot\mu^{HG}(F\times F),H(e^{GF})e^H)\\
&\,\textstyle=((HG)F,(HG)(\mu^F)\cdot\mu^{HG}(F\times F),(HG)(e^F)e^{HG})\\
&\,\textstyle=(HG,\mu^{HG},e^{HG})(F,\mu^F,e^F)\\
&\,\textstyle=((H,\mu^H,e^H)(G,\mu^G,e^G))(F,\mu^F,e^F)\\
&\,\textstyle=(HG)F,
\end{align}
である．
豊穣圏の性質
モノイダル圏$\cat{V}$と$\cat{V}$-圏$\ecat{A}$に対して，$\id{\cat{V}}(\ecat{A})=\ecat{A}$が成り立つ．
命題 1 より$\id{\cat{V}}=(\id{\cat{V}},\id{\otimes},\id{I})$であることに注意する．
定義 4.a.2, (1) より$\ob{(\id{\cat{V}}(\ecat{A}))}=\ob{\ecat{A}}$であり，各$A,B\in\ecat{A}$に対して，
\begin{align}
\mor{\id{\cat{V}}(\ecat{A})}{A}{B}
&\,\textstyle=\id{\cat{V}}(\mor{\ecat{A}}{A}{B})&(\text{定義 4.a.2, (2)})\\
&\,\textstyle=\mor{\ecat{A}}{A}{B},&(\text{定義 2.a.3})
\end{align}
であり，各$A,B,C\in\ecat{A}$に対して，
\begin{align}
M_{A,B,C}
&\,\textstyle=\id{\cat{V}}(M_{A,B,C})(\id{\otimes})_{\mor{\ecat{A}}{B}{C},\mor{\ecat{A}}{A}{B}}&(\text{定義 4.a.2, (3)})\\
&\,\textstyle=M_{A,B,C}(\id{\otimes})_{\mor{\ecat{A}}{B}{C},\mor{\ecat{A}}{A}{B}}&(\text{定義 2.a.3})\\
&\,\textstyle=M_{A,B,C}\,\id{\mor{\ecat{A}}{B}{C}\otimes\mor{\ecat{A}}{A}{B}}&(\text{定義 2.a.7})\\
&\,\textstyle=M_{A,B,C},
\end{align}
であり，各$A\in\ecat{A}$に対して，
\begin{align}
j_A&\,\textstyle=\id{\cat{V}}(j_A)\id{I}&(\text{定義 4.a.2, (4)})\\
&\,\textstyle=\id{\cat{V}}(j_A)\\
&\,\textstyle=j_A,&(\text{定義 2.a.3})
\end{align}
である．ゆえに，$\id{\cat{V}}(\ecat{A})=\ecat{A}$である．
Lax モノイダル関手$\func{G=(G,\mu^G,e^G)}{\cat{V}}{\cat{W}}$と$\func{(F,\mu^F,e^F)}{\cat{U}}{\cat{V}}$と$\cat{U}$-圏$\ecat{A}$に対して，$(GF)(\ecat{A})=G(F(\ecat{A}))$が成り立つ．
命題 2 より$GF=(GF,\mu^{GF},e^{GF})$であることに注意する．
\begin{align}
\ob{((GF)(\ecat{A}))}
&\,\textstyle=\ob{\ecat{A}}&(\text{定義 4.a.2, (1)})\\
&\,\textstyle=\ob{(F(\ecat{A}))}&(\text{定義 4.a.2, (1)})\\
&\,\textstyle=\ob{(G(F(\ecat{A})))},&(\text{定義 4.a.2, (1)})
\end{align}
である．
$$\textstyle(GF)(\ecat{A})=(\ob{\ecat{A}},\{\mor{(GF)(\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}})$$
及び
$$\textstyle G(F(\ecat{A}))=(\ob{\ecat{A}},\{\mor{G(F(\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}})$$
と定める．
各$A,B\in\ecat{A}$に対して，
\begin{align}
\mor{(GF)(\ecat{A})}{A}{B}
&\,\textstyle=(GF)(\mor{\ecat{A}}{A}{B})&(\text{定義 4.a.2, (2)})\\
&\,\textstyle=G(F(\mor{\ecat{A}}{A}{B}))&(\text{定義 2.a.4})\\
&\,\textstyle=G(\mor{F(\ecat{A})}{A}{B})&(\text{定義 4.a.2, (2)})\\
&\,\textstyle=\mor{G(F(\ecat{A}))}{A}{B},&(\text{定義 4.a.2, (2)})
\end{align}
である．
$A,B,C\in\ecat{A}$を取る．
命題 2 の証明で述べたように，
$$\textstyle(\mu^{GF})_{\mor{\ecat{A}}{B}{C},\mor{\ecat{A}}{A}{B}}=G((\mu^F)_{\mor{\ecat{A}}{B}{C},\mor{\ecat{A}}{A}{B}})(\mu^G)_{F(\mor{\ecat{A}}{B}{C}),F(\mor{\ecat{A}}{A}{B})},$$
である．
また，$G$は$\cat{V}$から$\cat{W}$への lax モノイダル関手だから，定義 4.a.1 より$G$は$\cat{V}$から$\cat{W}$への関手であり，
$$\textstyle G(F(M_{A,B,C}))G((\mu^F)_{\mor{\ecat{A}}{B}{C},\mor{\ecat{A}}{A}{B}})=G(F(M_{A,B,C})(\mu^F)_{\mor{\ecat{A}}{B}{C},\mor{\ecat{A}}{A}{B}}),$$
である．
ゆえに，
\begin{align}
M_{A,B,C}
&\,\textstyle=(GF)(M_{A,B,C})(\mu^{GF})_{\mor{\ecat{A}}{B}{C},\mor{\ecat{A}}{A}{B}}&(\text{定義 4.a.2, (3)})\\
&\,\textstyle=(GF)(M_{A,B,C})(\mu^{GF})_{\mor{\ecat{A}}{B}{C},\mor{\ecat{A}}{A}{B}}\\
&\,\textstyle=(GF)(M_{A,B,C})G((\mu^F)_{\mor{\ecat{A}}{B}{C},\mor{\ecat{A}}{A}{B}})(\mu^G)_{F(\mor{\ecat{A}}{B}{C}),F(\mor{\ecat{A}}{A}{B})}\\
&\,\textstyle=G(F(M_{A,B,C}))G((\mu^F)_{\mor{\ecat{A}}{B}{C},\mor{\ecat{A}}{A}{B}})(\mu^G)_{F(\mor{\ecat{A}}{B}{C}),F(\mor{\ecat{A}}{A}{B})}&(\text{定義 2.a.4})\\
&\,\textstyle=G(F(M_{A,B,C})(\mu^F)_{\mor{\ecat{A}}{B}{C},\mor{\ecat{A}}{A}{B}})(\mu^G)_{F(\mor{\ecat{A}}{B}{C}),F(\mor{\ecat{A}}{A}{B})}\\
&\,\textstyle=G(F(M_{A,B,C})(\mu^F)_{\mor{\ecat{A}}{B}{C},\mor{\ecat{A}}{A}{B}})(\mu^G)_{\mor{F(\ecat{A})}{B}{C},\mor{F(\ecat{A})}{A}{B}}&(\text{定義 4.a.2, (2)})\\
&\,\textstyle=G(M_{A,B,C})(\mu^G)_{\mor{F(\ecat{A})}{B}{C},\mor{F(\ecat{A})}{A}{B}}&(\text{定義 4.a.2, (3)})\\
&\,\textstyle=M'_{A,B,C},&(\text{定義 4.a.2, (3)})
\end{align}
である．
$A\in\ecat{A}$を取る．$G$は$\cat{V}$から$\cat{W}$への lax モノイダル関手だから，定義 4.a.1 より$G$は$\cat{V}$から$\cat{W}$への関手であり，$G(F(j_A))G(e^F)=G(F(j_A)e^F)$だから，
\begin{align}
j_A&\,\textstyle=(GF)(j_A)e^{GF}&(\text{定義 4.a.2, (4)})\\
&\,\textstyle=(GF)(j_A)G(e^F)e^G&(\text{命題 2})\\
&\,\textstyle=G(F(j_A))G(e^F)e^G&(\text{定義 2.a.4})\\
&\,\textstyle=G(F(j_A)e^F)e^G\\
&\,\textstyle=G(j_A)e^G&(\text{定義 4.a.2, (4)})\\
&\,\textstyle=j'_A,&(\text{定義 4.a.2, (4)})
\end{align}
である．
従って，$(GF)(\ecat{A})=G(F(\ecat{A}))$である．
これ以降は， 第4回 (後半) (2) の記事 で述べる．
