世界一やさしい圏論勉強会 #0 (Open β) を受けた

  • Chatwork の 高瀬 和之さん による 世界一やさしい圏論勉強会 に行ってきました(オンライン)
  • connpass へのリンク を見ると分かるように、授業ではなく対話を通じて理解を深めるスタイルで、実際に単純な例やこれはどうなの？という素朴な疑問に答えていて質問しやすい雰囲気でした。
  • 内容はスライドを見れば分かるので、なるべく素朴な疑問を中心に書いていきます。

概要

軽いまとめ

  • 圏論は、点と矢印に意味を持たせて話を展開する。点: 対象、矢印: 射 と呼ぶ。(有向グラフをイメージするとわかりやすい。)
  • 圏となる条件: 合成射の存在 (これは公理)
  • 合成射の存在から、Hom(A,B)の要素 f が一つでも存在するならば、Hom(X,A)の任意の要素 a について、Hom(X,B)のある要素 b が存在して、b=f○aとなる。
  • 矢印ではなく集合として扱えるのは大事で、集合の考え方が米田の補題の理解で重要な役割を果たす。

登場した質問たち

  • Q. A -> B へ複数やじるしがあってもいいのか？
    • A. OK。なくてもいい。A->B への矢印の集まりを Hom 集合と呼び、Hom(A,B)と表現する。矢印がない場合、Hom(A,B)は空集合になる
  • Q. Hom 集合は集合で制限されるのか？
    • A. 集合以外も考えられて圏を作れるかもしれないが解析は困難になるので、今回は集合とする。locally small という専門用語が登場した。
    • 自分で調べてみたら、locally small は圏の大きさを表す言葉で、要は Hom 集合として集合で制限する場合、圏の種類を局所的に小さいと分類付けているみたいだった(自信なし)
  • Q. 可換はイメージ的に結合じゃないの？
    • A. 可換図式という圏論の言葉があって、確かに結合っぽく見えるけど言葉的にはこれは可換です。結合もまた別の概念として圏論の世界に存在する。
  • Q. ,って意味的にはどうなるの？
    • A. 日本語の文の区切りと同じ捉えでよい。ただ、順番を入れ替えると意味が変わる例があり、全称量化と存在量化で調べてみよう！
  • Q. Scala のFunction1[A,B]が Hom(A,B)に対応するの？
    • A. 正しい。ただ、数学の話とプログラムの世界の話で埋め込めるかどうかは数学的に強い条件なので注意が必要。
    • 自分で考えると、プログラムの世界で表現可能な関数の集合より数学の世界の集合の方がやばい例が作れそうな気がして、広い世界から狭い世界への適用という意味で埋め込みという言葉を使っているのかなと思った(ここでの埋め込みは専門用語っぽい)
  • Q. Hom(Unit, Unit)は、Unit -> Int, Int -> Uint を作ればひとつではないのでは？
    • A.副作用がない場合に限って話をすると、結局 Int を経由する場合も() -> ()になるのでひとつと言える。
    • 副作用のない前提(print とかしない前提)は結構大事で、この副作用のない世界だと圏論が使えて嬉しくてそれと現実世界の折り合いをつけるために Monad が役に立つらしい。Monad よくわからないもの代表だったけどちょっと親近感がわきました。

自分の理解と疑問

  • 定義によると思うが、射が等しいと判定する条件がいまいちのみこめてない。Int を経由して Unit の話と、中身の実装の違いは考えない話から、今回は射の定義域と終域が同じなら同じ射とみなすということなのだろうか？というか射って写像っぽいしそうなる気がする。
  • 最後のステートメントは、Hom(X,A)と Hom(X,B)に対応がつくところが嬉しい感じがする。
  • プログラムの例で ∀a は [A](λ: A): A というのが出てきてここが分からなかった。数学サイドは分かるけど、プログラムの例が分からない。 → これについて Twitter で しけちあ, Siketyan さん に教えてもらって納得しました。

∀a の話，プログラミング的には例えば Rust だと fn foo<T>(arg: T) -> T みたいな関数は任意の型 T に対して定義できます．∀a ∈ A の場合 fn foo<T: A>(arg: T) -> T とすると型 T がトレイト A を実装している = A として扱える型の集合の一つ と解釈できるかなと思います

  • つまり、本質的に <T: A> 部分が重要で、引数の型と返り値の型が T であることは本質ではない。ということでした。プログラミングの世界だと色々くっついてくるところが分からなくなる原因だということがはっきりしました(Rust で書いてもらったおかげで、自分に馴染みのあるフィールドに来て検討を行う速度があがって助かった)

感想

  • 僕は高校時代に数学が好きで慣れていて、内容自体でつまづくことはなかったです。しかし、個人的な悩みとして「数学が分かった気になって基礎をおろそかにしてしまう」というのがあり、きちんと納得するためには素朴な疑問を思いつく訓練が必要だと思って参加しました。結果的に、しりとりの圏や型と関数の圏の簡単な例を通じてあたまをひねって素朴な疑問を思いつく訓練や、定義や公理のような簡単な出発点から考えを展開して検討する訓練ができてよかったです。