冪の普遍性から随伴を導く
参考
目標
https://gyazo.com/6d7ca93744615f5cdd0abec334df5135
冪と直積は手元にあるものとして、ここから上図を導く 例えば上図には、自然変換$ \eta,\epsilonが出てくるが、これがどういうものなのかを理解する必要がある 三角等式には、関手と自然変換しか出てこないが、一旦、対象などを具体的において、そこからgenericに対象を省いて考える
この目標はちょっと間違っているかもしれないのであとで確認mrsekut.icon*2
大まかな流れ
1) 冪と直積から、自然変換$ G_AF_A\xRightarrow{\epsilon}\mathrm{id}_\mathscr{C}を得る
これは易しい
2) 次に$ \epsilonの双対である$ \mathrm{id}_\mathscr{C}\xRightarrow{\eta}G_AF_Aを導く これが難しいmrsekut.icon
このために、以下の図式が可換になることを示す
https://gyazo.com/56ca5df4f15a7c4c5813c3d32ad4dfce
図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}を得る」
重要なのは$ \epsilonmrsekut.icon
https://gyazo.com/37c4ea09a5d9ff8a869dd571b000c8b8
図1-1
この図は以下と全く同じだ
こちらのほうがわかりやすいかもしれない
https://gyazo.com/7abc1b97444c8a67a53910f78f8e7624
図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だなmrsekut.icon
出力->(入力,関数)
とりあえず、さっきの図の矢印を逆転させてみると下図になる
https://gyazo.com/b2e0cd38141d884e7d61b338aa826bc5
図2-1
図2-1を関手$ F,Gを使わずに書くと以下のようになる
https://gyazo.com/961b43f4993044c9457cddc3b5fc3b31
図2-1-1
この青線の可換性はまだ示せていない。これを示すのが次の目標である。
そうすることで、結果的に自然変換$ \etaを得ることになる
前提
これ書く意味ある？mrsekut.icon
$ A\times Yの冪の関係を用いる
冪の定義により、$ (A\times Y)^Aが冪、評価射は$ \epsilon_{A\times Y} 下図を可換にする$ g: X\to (A\times Y)^Aが存在する
https://gyazo.com/0e5b82789fe2e9ecd506465b50e5629d
図2-2
↑の図は後の説明のために、冪の図とは違う角度で書いていてややこしいが、同じ様に書くと以下のようになる https://gyazo.com/efe1ebb58c7ca2fb2c88881a96741b95
図2-3
図2-1-1と図2-2の対応付けを示すならこんな感じになる
https://gyazo.com/e65268d9c71fe03315b708e2699e371d
言ってることはわかるが、意味あるのか？mrsekut.icon
図2-1の青線①を考える
図2-2に矢印を加えることで、$ \eta_Y\circ f:X\to F_AG_A(Y)を考える
https://gyazo.com/168d421af3ee476418c869eb0f042beb
図2-3
図2-2に青矢印を追加した
なんでこういうふうに青線を書き足すことが許されるのかを見る
以下のように図2-3の底辺を、左図のように冪のときのような図に書き換えるとわかりやすい https://gyazo.com/ab5c68a2b9010299c9aaf33e9d186f25
図2-3-1
冪と関数適用の議論と同様にして、左図を可換にする$ \eta_Y:A\to(A\times Y)^Aが存在する $ \eta_Yのアンカリー化とも見れるし、$ 1_{Y\times A}のカリー化とも見れるmrsekut.icon
後述するが、実はこの左図が目標の三角図式の1つ目になる
図2-1の青線②を考える
https://gyazo.com/e3c315fdb25c8d11f4f5708a8f3c76d8
図2-4
青点線を一旦無視して、緑線が成り立つ
この上で何故青点線が書けるのかを見る
https://gyazo.com/be7f968f2fbe0bf42772af391b29ccf9
図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が得られた
https://gyazo.com/b2e0cd38141d884e7d61b338aa826bc5
図2-1再掲
$ \etaが得られた上で再び図2-3-1を見る
https://gyazo.com/ab5c68a2b9010299c9aaf33e9d186f25
図2-3-1再び再掲
この左図が目的の三角図式の1つ目になる
同様のものを$ F_A,G_Aを用いて書くとこうなる
https://gyazo.com/f366c784bf0d9dee78b947139cce8b0a
図2-5
3) ここからは、2)の議論の双対を考える
つまり図2-5の双対である下図の可換性を示すのが目的
https://gyazo.com/2f85731a60da5dbcfb87214c71758783
図3-1
これが最初の目標の三角等式の2つ目の図式になる
なんでこれが図2-5の双対になるのかは??...mrsekut.icon $ \epsilon:G_AF_A\Rightarrow\mathrm{id}_\mathscr{C}、$ \eta:\mathrm{id}_\mathscr{C}\Rightarrow G_AF_Aの関係はちゃんと思い出しておこうmrsekut.icon
図3-1の可換性を示すために以下の自明な図式を用いる
https://gyazo.com/5f2c226ab9a53eacd6d095a4ce25c279
図3-2
これは、「自明な式」。目的達成のための補助定理として用いるmrsekut.icon
なので「この図はどこから出てきた？」という疑問には答えづらい
図3-1の可換性を示すために少し遠回りして下図の可換性を示すことを考える
https://gyazo.com/5b159baf0e8c7fe8ae891913ec4ee83b
図3-3
点線のところの可換性を示したい
なんで急にこんな複雑な図が出てくるのかと言うのを見ていく
わかりやすくするために図3-2と図3-3を横に並べて書く
https://gyazo.com/c0ca3f2a0608faba3b28b7c9a9729947
図3-4
これらの図でざっくりと以下のような対応を見出そうとしている
右図を使って左図の可換性を示したいのだ
右図は成り立っている前提で話をすすめる
https://gyazo.com/98a7484f177c60246670d585e691264c
図3-4-1
わかりやすく番号を付けて、順番に見ていこう
https://gyazo.com/29b77dfe89cd154e64a26571978fc533
図3-5
まずは緑5を示す
両図の左側にある、紫2、緑1、赤3に着目する
https://gyazo.com/ea39a77d7b76bf45ba34c5b1eb32ca1e
図3-6
次に赤2を示す
そのためにまず赤1を示す
両図の右上にある、緑1,2に着目する
https://gyazo.com/14281b68740f7c87b6fff80ed97c4c8e
図3-7
この図は、図3-6と全く同じなので赤1が存在し可換
赤1が言えたことで図3-4から不要なところを消したものが以下
https://gyazo.com/5589bf2831064f5deb7b9433476c8bf3
図3-8
点線の赤2を示したいんだったが、右図と比べると自明に成り立つのがわかる
すごいmrsekut.icon
最後に残っているのは緑4だ
https://gyazo.com/544021a2bf0875a8e4ac33faa850ed0c
図3-9
これまでの話により、自明に導かれる
これで目的達成
図3-3の可換性が示せた
https://gyazo.com/5b159baf0e8c7fe8ae891913ec4ee83b
図3-3再掲
四角形は可換になる
また図3-6が一番最初の目標だった三角等式の2つめになる
https://gyazo.com/ea39a77d7b76bf45ba34c5b1eb32ca1e
図3-6再掲
これを$ F_A,G_Aを用いて書き直すとこうなる
https://gyazo.com/943f243e36f6e59766ed13fa97339700
図3-10
図2-5と図3-10より2つの三角等式が得られた
https://gyazo.com/6d7ca93744615f5cdd0abec334df5135
書いたけど、よくよく考えたら使わなかった図たち
図2-3と図2-4を重ねて書く
https://gyazo.com/8df06bd3354ca9c8fd296dcf6b4b8a51
図2-5
図2-5を横に広げて書いてみる
https://gyazo.com/7b71c3cb528ebb17f20149fd8c35c5af
図2-6
こういうふうに広げたイメージ
https://gyazo.com/319e8a37571069f9890ce35863b437b0
図2-6の上辺のみに着目する
https://gyazo.com/2a6e67d91b84df42ec3d63a3fbac25e1
図2-7