「代数的な随伴系から自然なホムセット同型へ」において、次のように書きました。
“自然なホムセット同型”から“単位と余単位を含む代数系”を作るほうは、（僕は）うまくストリング図が描けなくて毎回行き詰まります。なので、やりません（うまくいったら報告するかも）。
ストリング図を使って計算する方法は思いつきません。うまくいってないです。もうしょうがないので、等式的な計算を使います。与えられた自然性を表す可換図式から要素を追いかけて等式を絞り出して。連立の等式から目的の自然性等式を得る方法です。面白くないし、絵図的直感は効かないです。ムーッ（不満）。$`\newcommand{\mrm}[1]{\mathrm{#1}}
\newcommand{\cat}[1]{\mathcal{#1}}
\newcommand{\twoto}{\Rightarrow }
\newcommand{\In}{\text{ in } }
%\newcommand{\Iff}{\Leftrightarrow }
\newcommand{\hyp}{\text{－} }
\newcommand{\op}{\mathrm{op} }
\newcommand{\id}{\mathrm{id} }
\newcommand{\vin}{ \style{display: inline-block; transform: rotate(-90deg)}{\in} }% \vin = lvin
\require{color} % 緑色
\newcommand{\Keyword}[1]{ \textcolor{green}{\text{#1}} }%
\newcommand{\For}{\Keyword{For } }%
\newcommand{\Define}{\Keyword{Define } }%
\newcommand{\Subject}{\Keyword{Subject } }%
%\newcommand{\Let}{\Keyword{Let } }
`$
記号の約束
| 図式順 | 反図式順 | |
| 関手／自然変換の横結合 | $`*`$ | $`\cdot`$ |
| 自然変換の縦結合 | $`;`$ | $`\circ`$ |
| 圏における射の結合 | $`;`$ | $`\circ`$ |
| 適用〈引数渡し〉 | $`.`$ | $`()`$ |
結合記号は、適用〈引数渡し〉より優先されます。
セットアップ
$`F, G`$ は関手の随伴ペアだとします。図式で描けば次のような状況です。
$`\quad \xymatrix@C+1pc{
\cat{C} \ar@/^1pc/[r]^{F} \ar@{}[r]|{\bot}
& \cat{D} \ar@/^1pc/[l]^{G}
}`$
随伴ペアであることは、次のような関手の自然同型 $`\varphi`$ で与えられているとします。
$`\quad \varphi : \cat{D}(F(\hyp), \hyp) \overset{\cong}{\to} \cat{C}(\hyp, G(\hyp) )
\In [\cat{C}^\op \times \cat{D}, {\bf Set}]
`$
$`\cat{C}`$ の射の族 $`|\cat{C}| \ni X \mapsto \eta_X \in \mrm{Mor}(\cat{C})`$ は次のように定義します。
$`\quad \begin{array}{ccc}
\cat{D}(F(X), F(X)) & \overset{\varphi_{X, F(X)}}{\longrightarrow} & \cat{C}(X, G\cdot F (X))\\
\vin & & \vin \\
\id_{F(X)} & \mapsto & \eta_X
\end{array}
`$
詳しく書けば：
$`\Subject \eta : |\cat{C}| \to \mrm{Mor}(\cat{C})\\
\quad \For X \in |\cat{C}|\\
\quad \Define \eta_X := \varphi_{X, F(X)}(\id_{F(X)} ) \in \cat{C}(X, G\cdot F (X)) \subseteq \mrm{Mor}(\cat{C})
`$
今定義した射の族 $`\eta`$ が $`\mrm{Id} \twoto G\cdot F`$ という自然変換であるためには次が要求されます。
$`\require{AMScd}
\forall X \in |\cat{C}|\\
\quad \begin{CD}
X @>{\eta_X}>> G\cdot F (X)\\
@V{f}VV @VV{G\cdot F (f)}V \\
Y @>{\eta_Y}>> G\cdot F (Y)
\end{CD}\\
\text{commutative in }\cat{C}
`$
等式としては：
$`\quad \eta_X ; G\cdot F(f) = f ; \eta_Y \In \cat{C}`$
これが、示すべきターゲット命題〈等式〉です。
計算
$`\varphi`$ の自然性から：
$`\For f:X \to Y \In \cat{C}\\
\quad \begin{CD}
\cat{D}(F(X), F(X)) @>{ \varphi_{X, F(X)}}>> \cat{C}(X, G\cdot F (X))\\
@V{ F(f)_* = F(f)\circ \hyp}VV @VV{ G\cdot F(f)_* = G\cdot F(f) \circ \hyp }V\\
\cat{D}(F(X), F(Y)) @>{ \varphi_{X, F(Y)}}>> \cat{C}(X, G\cdot F (Y))
\end{CD}\\
\text{commutative in }{\bf Set}
`$
要素を追いかける計算をします。
$`\xymatrix{
{ \id_{F(X)} } \ar@{|->}[r] \ar@{|->}[d]
& {\varphi_{X, F(X)} (\id_{F(X)}) = \eta_X } \ar@{|->}[d]
\\
{ F(f)_*(\id_{F(X)}) = F(f) } \ar@{|->}[r]
& { \varphi_{X, F(Y)} ( F(f) ) = G\cdot F (f) \circ \eta_X }
}
`$
再び $`\varphi`$ の自然性から：
$`\For f:X \to Y \In \cat{C}\\
\quad \begin{CD}
\cat{D}(F(X), F(Y)) @>{ \varphi_{X, F(Y)}}>> \cat{C}(X, G\cdot F (Y))\\
@A{ F(f)^* = \hyp \circ F(f)}AA @AA{ f^* = \hyp \circ f }A\\
\cat{D}(F(Y), F(Y)) @>{ \varphi_{Y, F(Y)}}>> \cat{C}(Y, G\cdot F (Y))
\end{CD}\\
\text{commutative in }{\bf Set}
`$
また、要素を追いかける計算をします。
$`\xymatrix{
{ F(f)^*(\id_{F(Y)}) = F(f) } \ar@{|->}[r]
& {\varphi_{X, F(Y)} ( F(f) ) = \eta_Y \circ f}
\\
{ \id_{F(Y)} } \ar@{|->}[r] \ar@{|->}[u]
& { \varphi_{Y, F(Y)} ( \id_{F(Y)} ) = \eta_Y } \ar@{|->}[u]
}
`$
要素を追いかけて得られた等式は：
- $`\varphi_{X, F(Y)} ( F(f) ) = G\cdot F (f) \circ \eta_X \text{ on }\cat{C}(X, G\cdot F (Y))`$
- $`\varphi_{X, F(Y)} ( F(f) ) = \eta_Y \circ f \text{ on }\cat{C}(X, G\cdot F (Y))`$
これらより、
$`\quad G\cdot F (f) \circ \eta_X = \eta_Y \circ f \In \cat{C}`$
あるいは、
$`\quad \eta_X ; G\cdot F (f) = f; \eta_Y \In \cat{C}`$
これは目的の等式です。
