2021-03-30
ふりかえり用アセット
見てきた範囲
参加者によるメモ
オマケのプログラム (Scala による Hom 函手の実装例)：
code:scala
// Scala では値のように振る舞う関数を定義することができる
// この場合 homFunctor という名称の値で、かつ型 X を遅延評価するような挙動をする
implicit def homFunctorX = new EndoFunctor[HomX, *] { }
米田の補題では$ \mathrm{Nat}(\mathrm{Hom}(X, \_), \mathbf{F})と$ \mathbf{F}(X)が一対一に対応することを述べているが、一対一対応が存在するとしても、その 対応のつけ方 は複数ある
p.49 で具体的な一対一対応を与えているが、これは米田の補題の証明で具体的に与えている対応方法をなぞらえたもの
米田の補題の証明に登場する具体的な一対一対応がその他の多数ありえる対応のつけ方に対して より自然なものである と言えるか？
あるいは一対一の対応のつけ方は何らかの意味で本質的に一意である、といったような議論は可能か？
Re: 圏論的には、全単射が存在することを、$ \mathbf{Sets}において同型射が 2 対象に存在する と言います
この同型射という概念がミソで、同型射で結びついた 2 対象は、圏論的には区別をしません
逆に言えば、全単射の作り方がどうであるかは圏論的には区別しない，ということも言えます
米田の補題によると、函手$ \mathbf{F} : \mathbb{C} \rightsquigarrow \mathbf{Sets}について、圏$ \mathbb{C}の任意の対象$ X \in \mathrm{Obj}(\mathbb{C})の$ \mathbf{F}による 行き先 が函手圏$ \mathbf{Sets}^\mathbb{C}の特定の Hom 集合に対応する。
圏$ \mathbb{C}の射$ f \in \mathrm{Hom}(A, B)の 行き先 $ \mathrm{map}_\mathbf{F}(f)について、同様の対応物が存在することは言えないか？
Re:$ \mathbf{F}(X)の$ X部分を任意にとった場合、それが$ \mathrm{Hom}(X, -)と$ \mathbf{F}の成す自然変換全体の集合と一対一に対応することから、$ \mathbf{F}による行き先がなんらかの函手圏における Hom 集合に対応する，という主張ですよね
結論から言えば、この議論こそが米田の補題で展開したかった流れであり、米田埋め込み と呼ばれる函手によって、$ \mathrm{map}_\mathbf{F}(f)は特定の自然変換と一対一に対応することが言えます
米田の補題を考えるにあたって函手や自然変換がどの辺にいるのかが気になる
米田の補題の対象となっている（ローカリースモールな）圏$ \mathbb{C}の対象の "あつまり"$ \mathrm{Obj}(\mathbb{C})はなんらかのグロタンデーク宇宙$ Uの部分集合と考える。すなわち$ \mathrm{Obj}(\mathbb{C}) \subset U($ \mathrm{Obj}(\mathbb{C}) \in Uとは限らない)
圏$ \mathbb{C}はローカリースモールなので、対象$ A, Bの間の射の "あつまり" は集合。すなわち、$ \mathrm{Hom}(A, B) \in U
あるいは、あらかじめ考えているグロタンディーク宇宙は、圏$ \mathbb{C}の対象と射を "含む" 程度におおきい
集合圏$ \mathbf{Sets}の対象は集合であるので、その対象の "あつまり" とはすなわち$ Uである。
圏$ \mathbb{C}から$ \mathbf{Sets}への函手とは、$ \mathrm{Obj}(\mathbb{C})から$ U(=\mathrm{Obj}(\mathbf{Sets}))への写像$ \mathbf{F} : \mathrm{Obj}(\mathbb{C}) \rightarrow Uと、対象$ A, B \in \mathrm{Obj}(\mathbb{C})ごとに決まる、写像$ \mathrm{map}_F : \mathrm{Hom}(A, B) \rightarrow \mathrm{Hom}(\mathbf{F}(A), \mathbf{F}(B))を考えている。
いっぱんに写像$ f : X \rightarrow Yとは、$ X \times{} Yの部分集合として考えられる
具体的に書くと、$ \mathbf{F} \subset \mathrm{Obj}(\mathbb{C})\times{}U
$ \mathbf{F}は$ Uの元とは限らず、宇宙である$ Uを超えているように見える
$ \mathrm{map}_Fは対象$ A, Bごとに決まる写像（＝集合）なので、$ \mathrm{map}_F \subset (\mathrm{Obj}(\mathbb{C})\times{}\mathrm{Obj}(\mathbb{C}))\times{}U
$ \mathrm{map}_Fも宇宙$ Uを超えている
このように単純に考えると、函手圏$ \mathbf{Sets}^\mathbb{C}を考えると、もともとの宇宙$ Uを超えてしまう。
圏$ \mathbb{C}の対象と射を含むようなグロタンディーク宇宙$ Uを考えたとして、函手圏をかんがえるには、宇宙$ Uの部分集合を再び「集合」として持つ よりおおきな宇宙$ \widetilde{U}のような存在が必要ではないか
果たして 安全な議論ができているのか不安になる。このように恣意的に「おおきな」宇宙を考えることに瑕疵はないのか
Re: 函手や自然変換が登場するので、函手圏の定式化が気になっているのかなと推察しましたが、実際のところ Locally Small という条件さえ言えれば$ \mathbf{Sets}に閉じた議論になるので、基数の大小関係は ($ \mathbf{Sets}の範囲までしか) 気にしなくて良いように思います 🤔
あとは、部分とみなすのか属するとみなすのかで議論の行く末が変わりそうですが、残念ながら私の答えられる範疇ではないので、専門家を別途あたっていただければと 🙏
個人的には、非加算無限の直積の基数が$ \alephの範囲で収まることから類推するに、宇宙に関する議論でも同様なことが言えないかは気になりますね
残っている疑問・質問事項
圏論の外延が「圏論で取り扱えるものの範囲」を指すのであれば、対象と射で規定できるものに限る，と考えてよいです
はい、記述が微妙に異なるだけでやっていることは一緒です 👍
圏論で扱う定理は "図式" によって定式化をしているため、異なる圏であっても同様な図式が成立するなら、その定理によって説明できる，という趣ですね 👨🏫
対象や射の性質が、圏を分け隔てるものと考えて問題ありません
$ \mathbf{Sets}を$ \mathbf{Sets}たらしめている対象や射の性質とは、対象が "集合"，射が "集合論的な意味での関数" で全てですね
すごい！👏✨