いや、まぁ、そこにかかりきりだったわけではないんですけど。圏の Limit を Product と Equalizer から作るという、かなり最初の方で出てくる、いや、そうでもないか。The book (Category theory for working mathematician )の真ん中ぐらいに出てくる証明ですね。
一行だけ除いて、比較的スムースに証明できたんだけど、そこだけどうしてもわからない。そもそも、本ちゃんの証明ではなくて、存在を証明する Limit の定義の一部の自然変換の可換性の証明だし。そこを仮定してしまえば証明できる。
仮定する方法は、いくつかあって、
＊ 別に書いて postulate (前提) と書く
＊ 定理の入力に書いちゃう
＊ Product とか Equalizer とかの性質に付け加える
postulate と書くとバレバレだが、後の二つはもっともらしい(ぉぃ)。で、しばらく放っておいて他の定理やら仕事やら授業やらをやってました。
この連休で、それをいじっていたんだけど、どうも Product を使ったのでは up to iso (等しくはないが繋がってるぐらい)までしか証明できないことにようやっと気がついた。
もともと、これは Pullback を Product と Equalizer から作るってのの延長なんだよね。で、そっちは証明できているので、対応する部分を見比べてみると…
＊ 使っているのは Equalizer であって、Product じゃない
えぇ〜? そうなの? で、Equalizer を使ってみると、一発ころりでした。なんだよ〜 Pullback の証明を見直すのは何回もやったなのになんで気が付かなかったんだよ〜
じゃぁ、なんで、Pullback の方は悩まなかったんだと思ったら、そっちは Higher order categorical logic の方の5行の証明の中の1行に書いてありました。それで十分なヒントだったらしい。なるほどね。The book の方の証明では、少し証明が違う(Coneを使う)のと、そこは結果だけしか書いてなかったんだよな。
型を見ているだけだけど、どの定理や定義を使うかはわからないからな〜 あと、Product は直積なので直観が働きやすいけど、Equalizer は余り対応した概念がないのでわかりにくかったのかも。
Product でできると思い込んだのが間違いだったみたい。それで証明できないと気がつくまでに余計なものを証明しまくっていたし。π1 x π2 = id とか。π1 x π2' = id が証明できればできるとか思っていたみたい。Agda では「絶対証明できる」と思って突っ走るのが良いのですが、もっといろいろ周りをみないとだめだな。
とりあえずは、できてめでたいってな感じです。
http://www.cr.ie.u-ryukyu.ac.jp/hg/Members/kono/Proof/category/file/7f40d6a51c72/pullback.agda
No comments:
Post a Comment