冪の普遍性から随伴を導くまでの準備(?)

冪と関数適用を先に読んでおくと良い

参考

『圏論の道案内』 8章

目標

直積と冪の間の三角等式を導く

これが随伴の定義に用いる三角等式につながる

冪と直積は手元にあるものとして、ここから上図を導く

例えば上図には、自然変換\eta,\epsilonが出てくるが、これがどういうものなのかを理解する必要がある

三角等式には、関手と自然変換しか出てこないが、一旦、対象などを具体的において、そこからgenericに対象を省いて考える

この目標はちょっと間違っているかもしれないのであとで確認

大まかな流れ

1) 冪と直積から、自然変換G_AF_A\xRightarrow{\epsilon}\mathrm{id}_\mathscr{C}を得る

これは易しい

2) 次に\epsilonの双対である\mathrm{id}_\mathscr{C}\xRightarrow{\eta}G_AF_Aを導く

これが難しい

このために、以下の図式が可換になることを示す

図0-1

これが示せれば目標の三角図式の片方を得られる

3) さらに上で示した可換図式の双対を得ることで、目標の三角図式のもう片方を得る

\eta,\epsilonともにもう得てるのに何故これが必要 #??

前提

積関手と冪関手を以下のように表す

積関手B\xrightarrow{F_A}A\times B

冪関手C\xrightarrow{G_D}C^D

なので、A\times X^A== F_AG_A(X)

A\times X^A→F_A(X^A)→F_A(G_A(X))→F_AG_A(X)というふうに式変形した

1) 最初の目標

「冪と直積から、自然変換G_AF_A\xRightarrow{\epsilon}\mathrm{id}_\mathscr{C}を得る」

重要なのは\epsilon

図1-1

この図は以下と全く同じだ

こちらのほうがわかりやすいかもしれない

図1-2

青色で囲ったところは、冪と関数適用のところで見た評価射などの話そのまま

Aが引数で、X^Aが関数、Xが出力。\epsilon_Xがメタ的なeval（関数適用）

圏\mathscr{A},\mathscr{C}間の関手F_AG_A,\mathrm{id}を考えることにより、その間の自然変換\epsilonを得る

ここでは、冪などのことを一旦忘れて、自然変換のことだけを意識すればすんなり理解できる

2) 次の目標

「\epsilonの双対である\mathrm{id}_\mathscr{C}\xRightarrow{\eta}G_AF_Aを導く」

さっきの話の双対を考える

個別の\etaは逆evalだな

とりあえず、さっきの図の矢印を逆転させてみると下図になる

図2-1

図2-1を関手F,Gを使わずに書くと以下のようになる

図2-1-1

この青線の可換性はまだ示せていない。これを示すのが次の目標である。

そうすることで、結果的に自然変換\etaを得ることになる

前提

これ書く意味ある？

A\times Yの冪の関係を用いる

冪の定義により、(A\times Y)^Aが冪、評価射は\epsilon_{A\times Y}

下図を可換にするg: X\to (A\times Y)^Aが存在する

図2-2

↑の図は後の説明のために、冪の図とは違う角度で書いていてややこしいが、同じ様に書くと以下のようになる

図2-3

右図は冪の定義などに用いている図

図2-1-1と図2-2の対応付けを示すならこんな感じになる

言ってることはわかるが、意味あるのか？

図2-1の青線①を考える

図2-2に矢印を加えることで、\eta_Y\circ f:X\to F_AG_A(Y)を考える

図2-3

図2-2に青矢印を追加した

なんでこういうふうに青線を書き足すことが許されるのかを見る

以下のように図2-3の底辺を、左図のように冪のときのような図に書き換えるとわかりやすい

図2-3-1

冪と関数適用の議論と同様にして、左図を可換にする\eta_Y:A\to(A\times Y)^Aが存在する

\eta_Yのアンカリー化とも見れるし、1_{Y\times A}のカリー化とも見れる

後述するが、実はこの左図が目標の三角図式の1つ目になる

図2-1の青線②を考える

図2-4

青点線を一旦無視して、緑線が成り立つ

この上で何故青点線が書けるのかを見る

図2-4-1

図2-4の上三角を冪の図に書き直す

\eta_Xのアンカリー化を考えることで、左図を可換にする\eta_X:X\to (A\times X)^Aが存在する

以上により図2-1の可換性が示され、自然変換\eta: \mathrm{id}_\mathscr{C}\to G_AF_Aが得られた

図2-1再掲

\etaが得られた上で再び図2-3-1を見る

図2-3-1再び再掲

この左図が目的の三角図式の1つ目になる

同様のものをF_A,G_Aを用いて書くとこうなる

図2-5

3) ここからは、2)の議論の双対を考える

つまり図2-5の双対である下図の可換性を示すのが目的

図3-1

これが最初の目標の三角等式の2つ目の図式になる

なんでこれが図2-5の双対になるのかは??...

\epsilon:G_AF_A\Rightarrow\mathrm{id}_\mathscr{C}、\eta:\mathrm{id}_\mathscr{C}\Rightarrow G_AF_Aの関係はちゃんと思い出しておこう

図3-1の可換性を示すために以下の自明な図式を用いる

図3-2

これは、「自明な式」。目的達成のための補助定理として用いる

なので「この図はどこから出てきた？」という疑問には答えづらい

図3-1の可換性を示すために少し遠回りして下図の可換性を示すことを考える

図3-3

点線のところの可換性を示したい

なんで急にこんな複雑な図が出てくるのかと言うのを見ていく

わかりやすくするために図3-2と図3-3を横に並べて書く

図3-4

これらの図でざっくりと以下のような対応を見出そうとしている

右図を使って左図の可換性を示したいのだ

右図は成り立っている前提で話をすすめる

図3-4-1

わかりやすく番号を付けて、順番に見ていこう

図3-5

まずは緑5を示す

両図の左側にある、紫2、緑1、赤3に着目する

図3-6

次に赤2を示す

そのためにまず赤1を示す

両図の右上にある、緑1,2に着目する

図3-7

この図は、図3-6と全く同じなので赤1が存在し可換

赤1が言えたことで図3-4から不要なところを消したものが以下

図3-8

点線の赤2を示したいんだったが、右図と比べると自明に成り立つのがわかる

すごい

最後に残っているのは緑4だ

図3-9

これまでの話により、自明に導かれる

これで目的達成

図3-3の可換性が示せた

図3-3再掲

四角形は可換になる

また図3-6が一番最初の目標だった三角等式の2つめになる

図3-6再掲

これをF_A,G_Aを用いて書き直すとこうなる

図3-10

図2-5と図3-10より2つの三角等式が得られた

point-free styleに書き換えたものが以下

図2-3と図2-4を重ねて書く

図2-5

図2-5を横に広げて書いてみる

図2-6

こういうふうに広げたイメージ

図2-6の上辺のみに着目する

さらに、冪の普遍性から随伴を導く#5e78dcb8198270000052ffa6にかいた書き換えをする

図2-7

これが目標の三角等式の1つ目