@alg_d 先生によるformal category theory入門

V-alg-d（ZZ） @alg_d

圏論の基礎でとある命題を読んだぼく「なるほど」 その証明を読んだぼく「わからん」 Kan拡張を使って自力で証明したぼく「自明」

V-alg-d（ZZ） @alg_d

数学徒もうみんな寝た?

V-alg-d（ZZ） @alg_d

最近、圏論は具体的過ぎて難しいのではないかという気がしてきたんですよ

V-alg-d（ZZ） @alg_d

圏論で一番重要なのは、やはり自然変換の合成だと思うんです。

V-alg-d（ZZ） @alg_d

まず自然変換の合成ができないとKan拡張の定義が理解できない。 #全ての概念はKan拡張である

V-alg-d（ZZ） @alg_d

圏論における「全ての概念」の一つである「随伴」も、通常(?)はHomを使って定義することも多いけど、自然変換の合成で定義することもできる。

V-alg-d（ZZ） @alg_d

そして、圏論をやっていて気付くのは、圏論の証明では「圏」「関手」「自然変換」の定義を気にすることはほとんどなくて、自然変換の計算をやっているだけで証明ができてしまう。

V-alg-d（ZZ） @alg_d

すると一つの疑問が出てくる: 「圏」「関手」「自然変換」を抽象化した概念を使って「圏論」を行うことはできるか?

V-alg-d（ZZ） @alg_d

圏全体は圏Catをなすけど、CatはHomが圏になっている(自然変換が射)。そこで一般に、Homが圏になるような「圏」を2圏という。

V-alg-d（ZZ） @alg_d

この2圏は先ほどの「圏」「関手」「自然変換」を抽象化したような概念になっている。例えば随伴やKan拡張の定義を知っている人であれば、直ちに「2圏の中での随伴/Kan拡張」を定義することができる

V-alg-d（ZZ） @alg_d

あ、今言っている2圏はstrict 2-categoryです。Cat豊穣圏と言ってもいい。

V-alg-d（ZZ） @alg_d

こういう、2圏で「圏論」をやるのはformal category theoryと言われていて、実はいろいろなことが知られている。

V-alg-d（ZZ） @alg_d

例えばStreetのthe formal theory of monadsというのがあって、これは一般の2圏の中でモナドを考察した論文だ。定義は関手の場合と同じ。

V-alg-d（ZZ） @alg_d

例えば、今Cを2圏とすると、Cの中の「モナド」全体はまた2圏になることが分かる。これをMonad(C)と書くことにする。対象c∈Cを一つ取ると、恒等射id: c→c は自明にモナドになる(恒等関手がモナドになるのと同じ)ので、包含Inc: C→Monad(C) が得られる。

V-alg-d（ZZ） @alg_d

このIncっていうのは2-関手と言われるもので、関手の2圏バージョン。

V-alg-d（ZZ） @alg_d

さて、このIncは2-左随伴(2圏の間の随伴)を持つことが知られているが、2-右随伴があるかどうかは分からない。

V-alg-d（ZZ） @alg_d

ところが、実は、Cを2圏としたとき「Inc: C→Monad(C) が2-右随伴を持つならば、Cの任意のモナドが随伴から得られる(関手の場合と同じで随伴からモナドを作ることができる)」という定理が成り立つことが分かる。

V-alg-d（ZZ） @alg_d

@alg_d これの証明に使ってるのがこのツイートの図式ですね twitter.com/alg_d/status/7…

V-alg-d（ZZ） @alg_d

モナドの勉強してるけどモナド is むずかC、よく分からない #たのしいけんろん pic.twitter.com/6sam8Thsz8

2016-04-14 00:47:29

V-alg-d（ZZ） @alg_d

関手の場合の、「任意のモナドが随伴から得られる」という定理は、Inc: Cat→Monad(Cat) が右随伴を持つ、ということに系にすぎない。

V-alg-d（ZZ） @alg_d

これすごくないですか(小並Kan)

V-alg-d（ZZ） @alg_d

ちなみにこの話にはオチがあって、Catの場合右随伴があることをどうやって証明するかというと、T代数を具体的に構成してわちゃわちゃやる(普通の場合とあんまりかわんねぇ…)

V-alg-d（ZZ） @alg_d

他にも、例えば左随伴が左Kan拡張と交換するという定理があって、 alg-d.com/math/category/ に証明が置いてあるけど(kan_extension.pdfの定理6)、この証明は何が書いてあるのかよく分からない

V-alg-d（ZZ） @alg_d

@alg_d 該当箇所 pic.twitter.com/GRx05r5mc1

拡大

V-alg-d（ZZ） @alg_d

この定理、実はこんな難しいことしなくても、一般の2圏で証明できる