2021-03-16_#5
ふりかえり用アセット
見てきた範囲
運営者の個人的な所感
質問の中には、かなり数学的な背景に踏み込んだものも多くなっている
今までの回ではすべての質問を解説してきたが、質問者のバックグラウンドを加味して、踏み込んだ質問に関しては Scrapbox 上での議論に留めるでも良いのかもしれない 🤔
逆に、これはぜひみなさんに理解して欲しいという質問は、今までの回と同様に口頭と図で補足するなど
この辺の運用，みなさん的にはどうでしょうか？ 🙏
Re: (参加者メモ欄に長々書いているのが私です)
コンセプトが「授業ではなく、対話」という趣旨なので、原則書いた（発言した）内容がなんでもすべて拾われる状態の方がよいように感じる
このページがもっといろんな人が編集しているのであれば、特に聞きたい質問に他の人が顔文字 "🤔" とかでリアクションをつけて、多いものに対して手厚く回答する、といった案もあるが
Re:Re: 👍
参加者によるメモ
米田の補題をScalaの圏(以下$ \mathbf{Scala})で翻訳するところが非常に大きなギャップがあると感じた（今も感じている）
文字通り解釈すれば米田の補題は、任意の圏$ \mathbb{C}と集合圏$ \mathbf{Sets}に対する特定の言明となっている
なので、任意の圏$ \mathbb{C}のところを具体的な圏$ \mathbf{Scala}で考えてみる、という作業はわかりやすい
補題の主張の集合圏$ \mathbf{Sets}のところも$ \mathbf{Scala}に置き換わってしまうところがまずハードル高い
$ \mathbf{Scala}が何らかの方法で集合圏$ \mathbf{Sets}に埋め込まれる、という事実をふんわり$ \mathbf{Scala}\hookrightarrow\mathbf{Sets}のような感じだと解したとして、米田の補題が主張している$ \mathrm{Nat}(\_,\_)と$ \mathbf{F}(X)の間の全単射が、$ \mathbf{Scala}圏の何らかのプログラムとして存在している、とは単純には言えないと感じる
Re: まず、米田の補題を$ \mathbf{Scala}で考えるときに行っていることは、ある種の$ \partial \mathbf{Sets} \hookrightarrow \mathbf{Scala}($ \mathbf{Sets}の部分圏から、$ \mathbf{Scala}への単射的函手) を考えることに相当します (なので、考えている向きが逆ですね)
この時大事なことは、米田の補題を構成する対象や射が$ \partial \mathbf{Sets}において、どのような図式をつくるか？ になります
圏論の大きな利点は、図式の構造さえ同じであれば、異なる圏においても同様な主張ができる という点にあります
コアアイデアとしては、Hom 集合を 指数対象 と呼ばれる構造を用いて表現し、なおかつそれが$ \mathbf{Scala}でも再現できるという点にあります
また、全単射という条件も、圏論においては 同型射 と呼ばれる構造を用いて表現することができ、こちらも同様に$ \mathbf{Scala}で再現ができます
Re:Re: "図式の構造さえ同じであれば、異なる圏においても同様の主張ができる"の部分がまだ腑に落ちない
図式の構造が同じである、とは何を意味しているのか？圏同値（函手によって互いに移りあう）ということか？
構造が同じであった場合に、同様の主張ができる、と言える根拠は何か？
例えば圏の公理や通常の三段論法のような論理の積み重ねの末に米田の補題を（任意の圏と集合圏の命題として）得る、その論理展開そのものの構造が命題の対象となる圏とは別にあるように考えている
圏の構造が同じであることから、論理の積み重ねの構造がそのままうまいこと平行移動するかのようにScala圏の命題としての主張が成立していることの証明として機能する、というようなことが主張されているのか？
Re:Re:Re: より正確にいえば、圏論で表現される諸概念は (射の等価性などを除いて) 図式の構造が定義 である，ということですね (なお、図式の構造とは対象と射によるグラフ構造を意味します)
指数対象と呼ばれるものや、同型射と呼ばれるものはある図式の構造が定義であり、圏を変えた時にどんなに非直感的な結果を生んだとしても、図式の構造が同じであれば、同じものとして捉えます (その抽象性が、圏論を強力な道具としている訳ですね)
ただ欠点としては、(対象や射の内部を調べない限り) 圏論の諸概念は構造の違いでしか捉えられないとも言えるので、そのあたりに誤りを犯しやすいとは言えますね 🤔
44 ページで Hom 函手と集合値函手を使って自然変換が成立することを説明していますが、そもそもここで何故 Hom 函手と集合値函手が出てきているんでしょうか？
Re: 資料上は、米田の補題の話をするために Hom 函手と集合値函手の関連性が必要だったため、話の流れで登場しているだけではありますね
ただ、Hom 函手は 任意の (Locally Small な) 圏から$ \mathbf{Sets}への函手 という非常に良い性質を持つものなので、それを詳しく調べてみたいというモチベーションは、米田さんにとっても自然な流れだったのかなと思います
なおかつ、函手の性質を圏論的に調べるのであれば、函手圏は非常に都合が良いので、自然変換を考えるに至ったのも、同様に自然な流れだったのかなと 📋
米田の補題の建てつけで、(Locally Small な) 圏$ \mathbb{C}から集合圏$ \mathbf{Sets}への函手が作る函手圏$ \mathbf{Sets}^{\mathbb{C}}の一般の函手$ \mathbf{F},\ \mathbf{G}\in{}\mathrm{Obj}(\mathbf{Sets}^\mathbb{C})に対して、それらの間の自然変換の "あつまり"$ \mathrm{Hom}(\mathbf{F},\mathbf{G})が集合であるとは一般には言えない？
より一般論に寄せて、Locally Small な２つの圏$ \mathbb{C},$ \mathbb{D}に対して、その函手圏$ \mathbb{D}^\mathbb{C}は Locally Small になるとは限らない？
米田の補題によって、$ \mathbf{F}として、共変$ \mathrm{Hom}函手$ h_Xをとった場合に限り、$ \mathrm{Hom}(h_X, \mathbf{G})が$ \mathbf{G}(X)と一対一に対応することで、限定的に 集合 になっている、ことが言える？ ⇒ この推察で正しいです
あるいは、米田の補題とは別に$ \mathrm{Hom}(h_X, \mathbf{G})が集合であることは言える？
Re: 直感的には、元の圏$ \mathbb{C}が Locally Small であるならば、圏$ \mathbb{D}で函手によって対応づけた射に対して Hom 集合を考えても Locally Small であることが言えて、なおかつ Locally Small な Hom 集合同士を全て可換とする自然変換もたかだか Locally Small な範囲で与えられることから、自然変換の "あつまり" も Locally Small に与えられる，という認識ですね
米田の補題は前提に Locally Small 性を置いているので、米田の補題とは独立にこのことを証明しなければだと思いますが、概ね上記の流れでいけるかなと
よくよく調べたら、これはダメっぽい 🙅♂️
Re:Re: とうてい 直観 でカバーできる範囲ではないような
自然変換は$ \theta_Aのように、圏$ \mathbb{C}の対象$ Aである意味 “添え字づけられた“ 射のあつまりであり、$ \mathbb{C}の対象ぜんたい$ \mathrm{Obj}(\mathbb{C})は集合ではないので、最初のステップとして$ \theta_Aを束ねた自然変換$ \thetaのあつまりも集合ではないように感じられます
Re:Re:Re: いちおう、その辺の厳密なお話は nlab さんに載っていたので、もしよければご参考まで 📋 結論から言うと、圏$ \mathbb{C}に Small 性，圏$ \mathbb{D}に Locally Small 性があれば十分，だそうな
というわけで、Hom 函手との自然変換を考える場合に限り$ \mathrm{Nat}(\mathrm{Hom}(X, -), F)も集合であることが言えて、圏$ \mathbb{C}の条件づけも Locally Small で良くなるわけですね (米田の補題，すごいや！)
残っている疑問・質問事項
メモ欄への回答にまとめました 📋
なお、埋め込み という言葉は一般に 構造を保つような単射 という意味しかないですね
2021-03-30 の冒頭でも補足しますが、米田の補題自体は$ \mathbf{Sets}に閉じる形で証明可能です その上で、$ \mathbf{Sets}で成立する図式を、$ \mathbf{Scala}で表現するとどうなるか？というのがサンプルプログラムの趣旨です
"気持ち" というのが「で、結局なにに使えばいいのさ？ 🤔」という意味であれば、以下の応用が知られています 👨🏫：
1. Church Encoding
2. 継続，および継続への変換
3. Free Monad との組み合わせによる Operational Monad の実現