普段からモノイダル圏が前提の世界に生きていると基本的な命題すら証明できなくて焦ることになります(なりました)。備えておきましょう。
図式のレイアウトなどについて、本稿はこの命題を初めて証明したMax Kellyの論文[1]に大いに基づいて構成されています。
モノイダル圏$\fullmoncat$とは、
の組で、次の2つの図式を可換にするもの。
\begin{xy}
\xymatrix@C=.6em{
& A\otimes(B\otimes(C\otimes D))
\ar[dr]^(.7){A\otimes\alpha_{B,C,D}}
\ar[ddl]_{\alpha_{A,B,C\otimes D}}
\\
&
& A\otimes((B\otimes C)\otimes D)
\ar[dd]^{\alpha_{A,B\otimes C,D}}
\\
(A\otimes B)\otimes(C\otimes D)
\ar[ddr]_{\alpha_{A\otimes B,C,D}}
\\
&
& (A\otimes(B\otimes C))\otimes D
\ar[dl]^(.4){\alpha_{A,B,C}\otimes D}
\\
& ((A\otimes B)\otimes C)\otimes D
}
\end{xy}
\begin{xy}
\xymatrix{
A\otimes(I\otimes B) \ar[rr]^{\alpha_{A,I,B}} \ar[rd]_{A\otimes\lambda_B }
&
& (A\otimes I)\otimes B \ar[ld]^{\rho_A\otimes B}
\\
& A\otimes B
}
\end{xy}
モノイダル圏$\fullmoncat$および任意の$X,Y\in\moncat$について、以下の図式は可換。
\begin{xy}
\xymatrix@C=1em{
I\otimes(X\otimes Y) \ar[rr]^-{\alpha_{I,X,Y}} \ar[rd]_(.4){\lambda_{X\otimes Y}}
&
& (I\otimes X)\otimes Y \ar[ld]^(.4){\lambda_X\otimes Y}
\\
& X\otimes Y
}
\end{xy}
次の図式を考える。このうち、$?$が記された三角形が可換であることを示せば、$\lambda$が自然な同型であることから命題が従う。
\begin{xy}
\xymatrix@C=.1em@R=1.2em{
I\otimes(I\otimes(X\otimes Y))
\ar[rr]^-{I\otimes\alpha_{I,X,Y}}
\ar[rdd]_(.5){I\otimes\lambda_{X,Y}}
\ar[dddd]_-{\alpha_{I,I,X\otimes Y}}
&
& I\otimes((I\otimes X)\otimes Y)
\ar[ldd]^(.45){I\otimes(\lambda_X\otimes Y)}
\ar[dddddddd]^-{\alpha_{I,I\otimes X,Y}}
\\
& ?
\\
& I\otimes(X\otimes Y)
\ar[dddd]^-{\alpha_{I,X,Y}}
\\
\\
(I\otimes I)\otimes(X\otimes Y)
\ar[ruu]^(.45){\rho_I\otimes(X\otimes Y)}
\ar[dddd]_-{\alpha_{I\otimes I,X,Y}}
\\
\\
& (I\otimes X)\otimes Y
\\
\\
((I\otimes I)\otimes X)\otimes Y
\ar[ruu]^(.45){(\rho_I\otimes X)\otimes Y}
&
& (I\otimes(I\otimes X))\otimes Y
\ar[ll]^-{\alpha_{I,I,X}\otimes Y}
\ar[luu]_{(I\otimes\lambda_X)\otimes Y}
}
\end{xy}
$?$の書かれていない部分について、2つの三角形はモノイダル圏の公理から可換、2つの四角形は$\rho$および$\alpha$の自然性から可換となる。また、外側の四角形は五角図式であるためモノイダル圏の公理から可換。
従って$?$の三角形も可換であり、$\lambda_X\otimes Y\circ\alpha_{I,X,Y}=\lambda_{X\otimes Y}$が成り立つ。$\qed$
モノイダル圏$\fullmoncat$および任意の$X,Y\in\moncat$について、以下の図式は可換。
\begin{xy}
\xymatrix@C=1em{
X\otimes(Y\otimes I) \ar[rr]^-{\alpha_{X,Y,I}} \ar[rd]_(.4){X\otimes\rho_Y}
&
& (X\otimes Y)\otimes I \ar[ld]^(.4){\rho_{X\otimes Y}}
\\
& X\otimes Y
}
\end{xy}
先ほどの図式の左右を全て入れ替えればよい。
モノイダル圏$\fullmoncat$について、$\lambda_I=\rho_I$。
$\lambda$の自然性から次の図式は可換である:
\begin{xy}
\xymatrix{
I\otimes(I\otimes I) \ar[r]^-{\lambda_{I\otimes I}} \ar[d]^-{I\otimes\lambda_I}
& I\otimes I \ar[d]^-{\lambda_I}
\\
I\otimes I \ar[r]^-{\lambda_I}
& I
}
\end{xy}
ここで、$\lambda$が自然同型であることから$\lambda_{I\otimes I}=I\otimes\lambda_I$。
次に、命題1およびモノイダル圏の公理から次の2つの図式が可換となる。
\begin{xy}
\xymatrix@C=.9em{
I\otimes(I\otimes I)
\ar[rr]^-{\alpha_{I,I,I}}
\ar[rd]_(.4){\lambda_{I\otimes I}}
&
& (I\otimes I)\otimes I
\ar[ld]^(.4){\lambda_I\otimes I}
& I\otimes(I\otimes I)
\ar[rr]^-{\alpha_{I,I,I}}
\ar[rd]_(.4){I\otimes\lambda_I}
&
& (I\otimes I)\otimes I
\ar[ld]^(.4){\rho_I\otimes I}
\\
& I
& &
& I
}
\end{xy}
$\alpha$は同型であり、かつ$\lambda_{I\otimes I}=I\otimes\lambda_I$であったので、2つの図式は同一であり$\lambda_I\otimes I=\rho_I\otimes I$、従って$\lambda_I=\rho_I$。$\qed$
モノイダル圏などにはコヒーレンス定理が成り立つので、モノイダル圏が前提の世界では本稿に書かれていたたくさんの括弧はすべてないものとして扱ってよい(どの順番で計算しようがすべて同値)のですが、本稿の2つの性質はそのコヒーレンス定理の証明にも使われるほど基本中の基本となる性質です。備えておきましょう(自戒)。