フロイトの随伴関手定理

Agda で圏論を証明していくシリーズですが、ようやっとフロイトの随伴関手定理まで終わりました。Hihger order categorical logic だと2 page、しかも、課題になってる。

内容的には、圏Aがcomplete(Limitiが存在する)で、U:A→BがLimitを保存するなら、圏Bのすべての対象bに対して、コンマ圏 b↓U が preinitial small full subcategory を持てば、U には随伴関手があるってもの。長い。

証明は段階を追っていて、

1. Complete な圏が preinitial small full subcategory を持てば initial object (任意のaに対して i → a なユニークな射があるi) がある。

preinitial small full subcategory ってのが、良くわからなかったんだけど、Aの部分圏ってのは要するに関手 S : A → A で送った先のことだとわかったら、任意のAの対象 a に対して、F(pi) → a という(ユニークとは限らない)射があるってことだとわかりました。この部分は丁寧に説明されていたので、割とすぐにできました。

で、次は、

2. if A is complete and G preserve limit, Comma Category F↓G is complete i.e. it has limit for Γ : I → F↓G

で、コンマ圏を定義することに。FにLimitの保存が要求されてないところが肝らしいです。これは激ムズだったんですが、3月ぐらいに片付けたみたい。この次は、

3. U : A → Sets, K{*}↓U has preinitial full subcategory iif U is representable

なんですが、AとUの条件が書いてない。2を使うはずなので、ないのは変なんだが。prepresentableってのは、米田関手 A → Hom (a,-) つまり、AからAの射の集合への関手に U が同相だってことらしい。つまり、Uは米田関手だとして片方向は証明してよいわけね。

ここで、もしかして、Sets の Completenessを使うんじゃないかと思って、まぁ、使わないんだけど、証明はするべきだなと思った。思ったんですが、結構、時間食ったのだが、Product と Equalizer はできたんだけど、Limit が直接に作れない。Product と Equalizer があれば Limit はできるという証明があるんですが、それにも、うまくマッピングできず。で、Stack overflow に投げたんですが、まだ、解答はきてないです。Agda の推論能力がちょっと足りないんじゃないかと思ってます。

結局、Uが米田関手なら K{*}↓U にinitial objectがあって、initial objectがあれば U が representable だってのは、AとUの条件抜きに証明できた。でも、2を使うには、UがLimitを保存するってのと、AがCompleteだってのが必要なんだが... AがCompleteってのは、さすがにでるわけないんだけど、UがLimitiを保存するってのは、AがCompleteならできそうだったんですが...

黄色の本(Category theory for working mathematian)を読み直したら「UがLimitを保存するから明らか」と書いてあって、結局、仮定だったのか。証明できそうだったはなんだったんだ。(後から見たらUのLimitの保存は使ってませんでした。representableならばUはLimitを保存するから仮定は必要ない)

ここまで来ると、K{b}↓U の initial object が universal mapping の解だってのを示せば、それから随伴関手ができるというわけ。これは、ここまでくれば、まぁ、楽勝。

というわけで、寄り道を除けば、2が一番難しかったみたい。黄色の本では equalizer と product の保存から導出してるな。

あとやるとすれば、Beck theorem か Kan extension でしょうけど、まぁ、やらんかな。

http://www.cr.ie.u-ryukyu.ac.jp/hg/Members/kono/Proof/category/file/9242298cffa8/freyd2.agda