圏論ユーザーのレベル10
その昔「○○プログラマのレベル10」というネタがあった。それを思い出したので圏論バージョンを作ってみようと思った。私がかく成長したいという独断的な妄想ノートである。誤りや見えていない境地については諸氏のご指導を仰ぐものである。
元祖はPerlのようだが、もっともっとさかのぼると起源は十牛図ではないかと思われる。章題はこれに則った。
レベル0：尋牛
圏論というものがあるらしい。熱心な知り合いがいるものの新興宗教じみており避けている。
レベル1：見跡
ポップな表紙の『圏論の歩き方』に手を出して絶望する。関連書籍がアマゾンのレコメンドに出てくるようになった。深遠みを覚えるが想像が及ばない。
レベル2：見牛
対象・射・函手・自然変換の定義を一通りさらう。直積を普遍射で定義して何が嬉しいのか分からない。米田の補題の手前で止まっている。
レベル3：得牛
とつぜん悟りが開ける。すべてが射と対象に見えてくる。輸血においてO型が始対象、AB型が終対象であることに喜ぶ。集合論に対し圏論マウントを、手続き型に対し関数型マウントを始める。ただし言い換えと再解釈に留まり生産的なことは何一つできない。
レベル4：牧牛
双対性やコホモロジーに執心する。Homが集合であることに純潔を汚された気持ちになり、それで豊穣圏の存在を知る。Rosetta Stoneの内容はだいたいわかる。あの方やこの方、こんな方の記事をよく見かける。量子力学を学ぶならクック＆キッシンジャーっしょと思うが、「Lensは余状態余モナドの余代数である」と言われるとまだビビる。
レベル5：騎牛帰家
函手こそが圏論の主人公だと思う。グロタンディーク哲学（圏の問題を米田埋め込みを通じ函手圏で考えること）の片鱗に触れ、米田の補題の深みを味わう。見慣れないデータ構造に出くわしたときは圏論で定式化し実装するが、たいていはHackageかCatlab.jlにあった。Pythonにしてもjavascriptにしても気付いたらモナドを実装している。集合論はトポスでモデル化されるし、手続き型プログラミングもこの世界を引数に隠しているだけなのだから、かつてのマウンティングが恥ずかしい。圏の対象を足したり掛けたり、べき乗を取るのはもちろんのこと、積分したり微分したりしても驚かない。TikZでどんな図式も描ける。
レベル6：忘牛存人
すべては圏と言うまでもなく圏であり、わざわざ圏とも言わない。ゲーデルの不完全性定理はLawvereの不動点定理の例だし、何ならYanofskyの図式を描けばいい。あらゆる繰り返し処理は始代数か終余代数だ。方程式の解は射で、解ける方程式は数学的構造の変形である（佐藤の哲学）。フーリエ変換はポントリャーギン双対で、BRST量子化はKoszul-Tate分解。Maclaneの言う通り「すべてがKan拡張」だ。あらゆるモノゴトが代数と幾何の双対性に見えている。
レベル7：人牛倶忘
圏論が無意識のバックグラウンドになっており新しい概念を定義したり問題解決ができる。ただし成果物を説明するのに圏論が必ずしも必要なく、論文に記しても蛇足なため世に出ていない。単なる考え方に留まる歯がゆさがある。
レベル8：返本還源
圏論を必然的かつ生産的に用いる。すなわち：
- 既知の圏論的構造の類似物を構成することで未知の対象を定義したり、研究手法を開発する。たとえば
- エレメンタリートポスの類似物としての量子論理の構成（トポス量子論）
- グロタンディークによる代数幾何学から数論幾何学の構築
- Synthetic differential geometryなど
- 何らかの不変量として圏や函手を定義する。たとえば
- 柏原正樹のリーマン・ヒルベルト対応
- 物理系の等価性を圏同値へ帰着させるホモロジカルミラーシンメトリー予想
- 群的な構造とその表現の圏の淡中クレイン型対応（例：プログラミング意味論）
レベル9：入鄽垂手
別分野の専門家でありつつ圏論をマスターしている。そこで独自の小分野を開拓しており、○○で圏論といえばこの人、と言われる。Bartosz Milewskiのようにevangelistとしても活動している。
Discussion