エレファント・ビジュアライザー調査記録

ビジュアルプログラミングで数式の変形を表すことを考えていくブロクです。

代数的構造による圏論(12)

随伴(3) 随伴の三角等式による定義

随伴の定義についても本に従って見ていきます。

随伴の三角等式による定義

定義 8.1 \mathcal{C} \mathcal{D} 間の関手  \mathcal{C} \xrightarrow{F} \mathcal{D} \mathcal{C} \xleftarrow{G} \mathcal{D} について、自然変換  FG \overset{\varepsilon}{\Longrightarrow} \mathrm{id}_\mathcal{D} \mathrm{id}_\mathcal{C} \overset{\eta}{\Longrightarrow} GF が存在してこれらが三角等式を満たすとき、すなわち  \require{AMScd} \begin{CD}
F @> 1_F >> F \\
@V Fη VV @| \\
FGF @>> εF > F
\end{CD} \begin{CD}
G @> ηG >> GFG \\
@| @VV Gε V \\
G @>> 1_G > G
\end{CD} を可換にするとき、四つ組  \langle F, G, \varepsilon, \eta \rangle を随伴関係と呼びます。

定義(圏の積) \mathcal{C} \mathcal{D} の積  \mathcal{C} \times \mathcal{D} とは、

  •  \mathcal{C} \times \mathcal{D} の対象は、 \mathcal{C} の対象  X \mathcal{D} の対象  Y の組  \langle X, Y \rangle
  •  \mathcal{C} \times \mathcal{D} の射は、 \mathcal{C} の射  X \xrightarrow{f} X' \mathcal{D} の射  Y \xrightarrow{g} Y' の組  \langle X, Y \rangle \xrightarrow{\langle f, g \rangle} \langle X', Y' \rangle

であるものと定義します(これは圏となります)。

定義 関手  \mathcal{C}^\mathrm{op} \times \mathcal{C} \xrightarrow{\mathrm{Hom}_\mathcal{C}(-, -)} \mathbf{Set}

  •  \mathcal{C}^\mathrm{op} \times \mathcal{D} の対象  \langle X, Y \rangle \mathrm{Hom}_\mathcal{C}(X, Y) を対応させる
  •  \mathcal{C} の射  A' \xrightarrow{a} A に対応する  \mathcal{C}^\mathrm{op} の射を  A \xrightarrow{a^\mathrm{op}} A' とすると、 \mathcal{C}^\mathrm{op} の射を  A \xrightarrow{a^\mathrm{op}} A' \mathcal{C} の射  B \xrightarrow{b} B' の組である  \mathcal{C}^\mathrm{op} \times \mathcal{C} の射  \langle A, B \rangle \xrightarrow{\langle a^\mathrm{op}, b \rangle} \langle A', B' \rangle に対応する  \mathbf{Set} の射  \mathrm{Hom}_\mathcal{C}(A, B) \xrightarrow{\mathrm{Hom}_\mathcal{C}(a^\mathrm{op}, b)} \mathrm{Hom}_\mathcal{C}(A,' B') を、
    •  A \xrightarrow{x} B A' \xrightarrow{a} A \xrightarrow{x} B \xrightarrow{b} B' に対応させるもの

と定義します(これは関手となります)。

定義 関手  \mathcal{C} \xrightarrow{F} \mathcal{D} に対応する関手  \mathcal{C}^\mathrm{op} \xrightarrow{F^\mathrm{op}} \mathcal{D}^\mathrm{op} F^\mathrm{op} として

  •  \mathcal{C}^\mathrm{op} \times \mathcal{D} \xrightarrow{F^\mathrm{op} \times \mathrm{id}_\mathcal{D}} \mathcal{D}^\mathrm{op} \times \mathcal{D} \xrightarrow{\mathrm{Hom}_\mathcal{D}(-, -)} \mathrm{Set} \mathrm{Hom}_\mathcal{D}(F(-), -)
  •  \mathcal{C}^\mathrm{op} \times \mathcal{D} \xrightarrow{\mathrm{id}_{\mathcal{C}^\mathrm{op}} \times G} \mathcal{C}^\mathrm{op} \times \mathcal{C} \xrightarrow{\mathrm{Hom}_\mathcal{C}(-, -)} \mathrm{Set} \mathrm{Hom}_\mathcal{C}(-, G(-))

と書きます。

定理 8.2 \mathcal{C} \mathcal{D} 間の関手  \mathcal{C} \xrightarrow{F} \mathcal{D} \mathcal{C} \xleftarrow{G} \mathcal{D} の定める随伴関係  \langle F, G, \varepsilon, \eta \rangle から自然同値  \mathrm{Hom}_\mathcal{D}(F(-), -) \implies \mathrm{Hom}_\mathcal{C}(-, G(-)) を構成することができます。

[証明]

  •  F(X) \xrightarrow{f} Y から  X \xrightarrow{\eta_X} GF(X) \xrightarrow{G(f)} G(Y) への対応を  \Phi_{\langle X, Y \rangle}
  •  X \xrightarrow{g} G(Y) から  F(X) \xrightarrow{F(g)} FG(Y) \xrightarrow{\varepsilon_Y} Y への対応を  \Psi_{\langle X, Y \rangle}

とおきます。

  •  \mathrm{Hom}_\mathcal{D}(F(-), -) \overset{\Phi}{\Longrightarrow} \mathrm{Hom}_\mathcal{C}(-, G(-)) (カリー化)
  •  \mathrm{Hom}_\mathcal{D}(F(-), -) \overset{\Psi}{\Longleftarrow} \mathrm{Hom}_\mathcal{C}(-, G(-)) (アンカリー化)

は以下の図式が可換図式となることから自然変換となります。

 X \xrightarrow{x} X' Y \xrightarrow{y} Y' に関する以下の図式を考えます。(図式1) \begin{CD}
\mathrm{Hom}_{\mathcal{D}}(F(X),Y) @> \Phi_{\langle X, Y \rangle} >> \mathrm{Hom}_{\mathcal{C}}(X,G(Y)) \\
@V \mathrm{Hom}_{\mathcal{D}}(F(x),y) VV @VV \mathrm{Hom}_{\mathcal{C}}(x,G(y)) V \\
\mathrm{Hom}_{\mathcal{D}}(F(X'),Y') @> \Phi_{\langle X', Y' \rangle} >> \mathrm{Hom}_{\mathcal{C}}(X',G(Y')) \\
\end{CD}

 F(X) \xrightarrow{f} Y をとると、 \eta が自然変換であることから  GF(x) \circ η_{X'} = η_{X} \circ x となるので \begin{eqnarray*}
\Phi_{\langle X', Y' \rangle} ( \mathrm{Hom}_{\mathcal{D}}(F(x),y) (f) )
& = & \Phi_{\langle X', Y' \rangle} ( y \circ f \circ F(x) ) \\
& = & G(y) \circ G(f) \circ GF(x) \circ η_{X'} \\
& = & G(y) \circ G(f) \circ η_{X} \circ x \\
& = & \mathrm{Hom}_{\mathcal{C}}(x,G(y)) ( G(f) \circ η_{X} ) \\
& = & \mathrm{Hom}_{\mathcal{C}}(x,G(y)) ( \Phi_{\langle X, Y \rangle}(f) ) \\
\end{eqnarray*} となって、(図式1)は可換図式となります。よって  \Phi は自然変換となります。

 X \xrightarrow{x} X' Y \xrightarrow{y} Y' に関する以下の図式を考えます。(図式2) \begin{CD}
\mathrm{Hom}_{\mathcal{D}}(F(X),Y) @< \Psi_{\langle X, Y \rangle} << \mathrm{Hom}_{\mathcal{C}}(X,G(Y)) \\
@V \mathrm{Hom}_{\mathcal{D}}(F(x),y) VV @VV \mathrm{Hom}_{\mathcal{C}}(x,G(y)) V \\
\mathrm{Hom}_{\mathcal{D}}(F(X'),Y') @< \Psi_{\langle X', Y' \rangle} << \mathrm{Hom}_{\mathcal{C}}(X',G(Y')) \\
\end{CD}

 X \xrightarrow{g} G(Y) をとると、 \varepsilon が自然変換であることから  ε_{Y'} \circ FG(y) = y \circ ε_{Y} となるので \begin{eqnarray*}
\Psi_{\langle X', Y' \rangle} ( \mathrm{Hom}_{\mathcal{c}}(x,G(y)) (g) )
& = & \Phi_{\langle X', Y' \rangle} ( G(y) \circ g \circ x ) \\
& = & ε_{Y'} \circ FG(y) \circ F(g) \circ F(x) \\
& = & y \circ ε_{Y} \circ F(g) \circ F(x) \\
& = & \mathrm{Hom}_{\mathcal{D}}(F(x),y) ( ε_{Y} \circ F(g) ) \\
& = & \mathrm{Hom}_{\mathcal{D}}(F(x),y) ( \Psi_{\langle X, Y \rangle}(g) ) \\
\end{eqnarray*} となって、(図式2)は可換図式となります。よって  \Psi は自然変換となります。

 (Fη)_X = F(η_X) (εF)_X = ε_{F(X)} なので三角等式を書き換えると(図式3) \begin{CD}
F(X) @> 1_{F(X)} >> F(X) \\
@V F(η_X) VV @VV 1_{F(X)} V \\
FGF(X) @>> ε_{F(X)} > F(X)
\end{CD} は可換図式となります。 F(X) \xrightarrow{f} Y をとると、 ε は自然変換なので(図式4) \begin{CD}
F(X) @> 1_{F(X)} >> F(X) \\
@V F(η_X) VV @VV 1_{F(X)} V \\
FGF(X) @>> ε_{F(X)} > F(X) \\
@V FG(f) VV @VV f V \\
F(X) @>> ε_{Y} > Y
\end{CD} は可換図式となります。よって \begin{eqnarray*}
\Psi_{\langle X, Y \rangle} ( \Phi_{\langle X, Y \rangle} (f) )
& = & \Psi_{\langle X, Y \rangle} ( G(f) \circ η_{X} ) \\
& = & ε_{Y} \circ FG(f) \circ F(η_{X}) \\
& = & f \\
\end{eqnarray*} となって、 \Psi \circ \Phi \mathrm{Hom}_{\mathcal{D}}(F(-), -) の恒等自然変換となります。

 (Gε)_Y = G(ε_Y) (ηG)_Y = η_{G(Y)} なので三角等式を書き換えると(図式5) \begin{CD}
G(Y) @> η_{G(Y)} >> GFG(Y) \\
@V 1_{G(Y)} VV @VV G(ε_Y) V \\
G(Y) @>> 1_{G(Y)} > G(Y)
\end{CD} は可換図式となります。 X \xrightarrow{g} G(Y) をとると、 η は自然変換なので(図式6) \begin{CD}
X @> η_{X} >> GF(X) \\
@V g VV @VV GF(g) V \\
G(Y) @> η_{G(Y)} >> GFG(Y) \\
@V 1_{G(Y)} VV @VV G(ε_Y) V \\
G(Y) @>> 1_{G(Y)} > G(Y)
\end{CD} は可換図式となります。よって \begin{eqnarray*}
\Phi_{\langle X, Y \rangle} ( \Psi_{\langle X, Y \rangle} (g) )
& = & \Phi_{\langle X, Y \rangle} ( ε_Y \circ F(g) ) \\
& = & G(ε_{Y}) \circ GF(g) \circ η_{X} \\
& = & g \\
\end{eqnarray*} となって、 \Phi \circ \Psi \mathrm{Hom}_{\mathcal{C}}(-, G(-)) の恒等自然変換となります。

よって  \Phi は自然同値となります。[証明終わり]