Kleisli圏の単位律と結合律

西郷 甲矢人 (著), 能美 十三 (著) 圏論の道案内 ~矢印でえがく数学の世界~ (数学への招待シリーズ) の「第9章モナド」で、モナドから随伴を作るときにKleisli圏という圏が登場した。

この記事では、Kleisli圏の単位律と結合律についてまとめてみる。

まず、圏 C上のモナド Tとは、組 \langle T, \eta, \mu \rangleであり、以下の図式を可換にするものである。

f:id:yabaniyatun:20191014195735p:plain

ここで、 T, \eta, \muは、関手 T: C \to C, 自然変換 \eta: id_C \Rightarrow T, 自然変換 \mu: TT \Rightarrow T

Kleisli圏はモナドに関連して考えられる圏である。 モナド Tに関するKleisli圏 C_{T}の対象 X_{T}は、圏 Cの対象 Xと同じであり、圏 C_{T}の射 f_{T}: X_{T} \to Y_{T}は、圏 Cの射 f: X \to T(Y)に対応する。

対象 X_{T}の恒等射 1_{X_{T}}: X_{T} \to X_{T}は、圏 Cの射 \eta_{X}: X \to T(X)に対応する。

 f_{T}: X_{T} \to Y_{T} g_{T}: Y_{T} \to Z_{T}の合成 g_{T} \circ_{T} f_{T}: X_{T} \to Z_{T}は、圏 Cの射 \mu_{Z} \circ T(g) \circ f: X \to T(Z)に対応する。

ここで、このように定義した恒等射が単位律を満たすこと、それから、このように定義した射および射の合成が結合律を満たすことを示したい。

まずは、恒等射が単位律を満たすこと、すなわち、任意の f_{T}: X_{T} \to Y_{T}に対して、

 f_{T} \circ_{T} 1_{X_{T}} = 1_{Y_{T}} \circ_{T} f_{T} = f_{T}

が成り立つことを示す。

 Cにおいて、

 \mu_{Y} \circ T(f) \circ \eta_{X} = \mu_{Y} \circ T(\eta_{Y}) \circ f = f

が成り立つことを示せばよい。

 \etaの自然性を表す図式とモナド Tの定義に使った2番目の可換図式を組み合わせた以下の図式が可換であることから、上の式が成り立つことがわかる。

f:id:yabaniyatun:20191014203533p:plain

よって、恒等射が単位律を満たすことが示せた。

次に、射および射の合成が結合律を満たすこと、すなわち

 f_{T}: X_{T} \to Y_{T}, g_{T}: Y_{T} \to Z_{T}, h_{T}: Z_{T} \to W_{T}

に対して、

 (h_{T} \circ_{T} g_{T}) \circ_{T} f_{T} = h_{T} \circ_{T} (g_{T} \circ_{T} f_{T})

が成り立つことを示す。

 Cにおいて、

 \mu_{W} \circ T(\mu_{W} \circ T(h) \circ g) \circ f = \mu_{W} \circ T(h) \circ (\mu_{Z} \circ T(g) \circ f)

が成り立つことを示せばよい。

 \mu_{W} \circ T(\mu_{W} \circ T(h) \circ g) \circ f = \mu_{W} \circ T(\mu_{W}) \circ TT(h) \circ T(g) \circ f

ここで、モナド Tの定義の1番目の可換図式から、以下の図式が可換であることがわかる。

f:id:yabaniyatun:20191014205033p:plain

よって、上の式は以下になる。

 \mu_{W} \circ \mu_{T(W)} \circ TT(h) \circ T(g) \circ f

 \muの自然性を表す以下の可換図式が書けるので、

f:id:yabaniyatun:20191014205629p:plain

上の式は以下になる。

 \mu_{W} \circ T(h) \circ \mu_{Z} \circ T(g) \circ f = \mu_{W} \circ T(h) \circ (\mu_{Z} \circ T(g) \circ f)

射および射の合成が結合律を満たすことが示せた。

図式を書くのに使ったTexソース

\documentclass[12pt]{ujarticle}
\usepackage{amsmath,amsfonts,amsthm,amssymb,amscd}
\usepackage[all]{xy}
\def\objectstyle{\displaystyle}
\begin{document}
\[
\xymatrix{
  TTT \ar@{=>}[r]^{T\mu} \ar@{=>}[d]_{\mu T} & TT \ar@{=>}[d]^{\mu} \\
  TT \ar@{=>}[r]_{\mu} & T
}
\]
\[
\xymatrix{
  T \ar@{=>}[r]^{T\eta} \ar@{=>}[rd]_{1_T} & TT \ar@{=>}[d]^{\mu} & T \ar@{=>}[l]_{\eta T} \ar@{=>}[ld]^{1_T} \\
  & T &
}
\]
\[
\xymatrix{
  X \ar[r]^{f} \ar[d]_{\eta_X} & T(Y) \ar[d]^{T(\eta_Y)} \ar[rd]^{1_{T(Y)}} \\
  T(X) \ar[r]_{T(f)} & TT(Y) \ar[r]_{\mu_Y} & T(Y)
}
\]
\[
\xymatrix{
  TTT(W) \ar[r]^{T(\mu_W)} \ar[d]_{\mu_{T(W)}} & TT(W) \ar[d]^{\mu_W} \\
  TT(W) \ar[r]_{\mu_W} & T(W)
}
\]
\[
\xymatrix{
  TT(Z) \ar[r]^{TT(h)} \ar[d]_{\mu_Z} & TTT(W) \ar[d]^{\mu_{T(W)}} \\
  T(Z) \ar[r]_{T(h)} & TT(W)
}
\]
\end{document}