圏同値の同値性を確認する
これを圏と圏の間の$ \congについて、成り立っているのかを確認する
参考
示すこと
任意の圏$ \mathscr{A}について、$ \mathscr{A}\cong\mathscr{A}が成り立つ
つまり$ FG\cong GF\cong 1_\mathscr{A}になるような
2つの関手$ F,G:\mathscr{A}\to\mathscr{A}を見つけられればいい
ここで$ \mathrm{id}_\mathscr{A}=F,Gとすると、
$ FG=GF=\mathrm{id}_\mathscr{A}が成り立つ
これは$ FG\cong GF\cong 1_\mathscr{A}よりも強い条件である
したがって反射律は成り立つ
示すこと
任意の2つの圏$ \mathscr{A},\mathscr{B}について、以下が成り立つ
$ \mathscr{A}\cong\mathscr{B}ならば$ \mathscr{B}\cong\mathscr{A}
仮定である$ \mathscr{A}\cong\mathscr{B}があるとき、どういう状態か
それは以下の2つの圏(赤)で、少なくとも以下の4本の射(青)の存在が示されている状態である
https://gyazo.com/c6248752b02bb05e9fe48b3dae04adfa
図2-1
https://gyazo.com/27b4b97f927879e81a4aee9270ea095a
図2-2
図2-1の状態から以下のように置き換えた
$ F'=G
$ G'=F
$ \varepsilon'=\eta
$ \eta'=\varepsilon
図2-2と同じ関係性のまま$ \mathscr{A},\mathscr{B}を逆に書いたものが以下
https://gyazo.com/3a3cbc79a868db63fb19a9bdab16825c
図2-3
図2-1と図2-3を並べてみることで、成り立っていることがわかる
示すこと
任意の3つの圏$ \mathscr{A},\mathscr{B},\mathscr{C}について、
$ \mathscr{A}\cong\mathscr{B}かつ$ \mathscr{B}\cong\mathscr{C}ならば、$ \mathscr{A}\cong\mathscr{C}
最初の２つの仮定を図にするとこう
https://gyazo.com/c57f26cd4eca07a39b044539922e89c9
https://gyazo.com/331ac369288cbb4e0b3275f3c813c057
この2つの図から下図を導けられればいい
https://gyazo.com/2e5136525e0995ba3e36d9760ab50699
図3-3
最初の2つの図の左半分を一つの図にして書くとこうなる
https://gyazo.com/2f49259683350afb74a1a73f54550bb4
この図の中の関手と自然変換を合成していくわけだが、ストリング図でやってみた https://gyazo.com/87797875b025a1baef842b3afa40bf02
③で出現する$ G\eta'F: GF\to GG'F'Fは自然同型
④で出現する$ G\eta'F\eta:\mathrm{id}_\mathscr{A}\to GG'F'Fも自然同型
④を普通の図に戻すとこうなる
https://gyazo.com/e414e18989055cea15fde515c101c2eb
この自然同型を$ \eta'':=G\eta'F\etaと定義する
最初の2つの図の右半分を一つの図についても同様
ストリング図のみ示す
https://gyazo.com/e7092bd8240bdbdd1fe6f2ad5a6417b1
最後の自然同型を$ \varepsilon''=F'FGG'\to \mathrm{id}_\mathscr{C}と定義する
図3-3を再掲する
https://gyazo.com/2e5136525e0995ba3e36d9760ab50699
以上の流れで定義した2つの自然同型$ \eta'',\varepsilon''により、これが示されている