2021-03-02_#4
ふりかえり用アセット
見てきた範囲
参加者によるメモ
型とプログラムの圏$ \mathbb{C}で函手とはいわば$ \mathtt{Seq}のような一つの型を受け取って、別の型を返すものに相当する、では二つの型を受け取る$ \mathtt{Either}のようなものは型とプログラムの圏ではどのような位置にあるのか
単純に考えると、何か型$ \mathtt{Int}を固定して$ \mathtt{Either}[\mathtt{Int}, \_]のようなものが、型をひとつ受け取って、別の型を返すから、函手圏$ \mathbb{C}^{\mathbb{C}}の対象に相当するのかな？
上記で固定した$ \mathtt{Int}がいろいろ動くと考えると、$ \mathtt{Either}は$ \mathbb{C}から$ \mathbb{C}^{\mathbb{C}}への函手、ということになるのか？
さらに一般の圏$ \mathbb{C},$ \mathbb{D},$ \mathbb{E}に対して、圏$ \mathbb{C}から函手圏$ \mathbb{E}^{\mathbb{D}}への函手を考えることが、圏$ \mathbb{C}と圏$ \mathbb{D}に対して圏$ \mathbb{E}の対象と、射を対応づけるような何ものかに該当する、と解釈することは可能か？
あるいは、記号だけの推察で、上記の何ものかとは$ (\mathbb{E}^{\mathbb{D}})^{\mathbb{C}}の何かであり、これは函手圏$ \mathbb{E}^{\mathbb{D}\times\mathbb{C}}の対象、函手である、と解釈可能な新たな圏$ \mathbb{D}\times\mathbb{C}を考えることは可能か？
Re: 2 つの圏$ \mathbb{C}と$ \mathbb{D}に対して、デカルト積をそれぞれの対象と射について考えることで、積圏 と呼ばれるものを構成することができます
Either のような型引数を 2 つ取るカインドは、自己積圏$ \mathbb{C} \times \mathbb{C}から圏$ \mathbb{C}への 双函手 というもので与えられます
ここで注意点としては、圏$ (\mathbb{C}^{\mathbb{C}})^{\mathbb{C}}と圏$ \mathbb{C}^{\mathbb{C} \times \mathbb{C}}が一致する訳ではないということです (ただし、これらの間には函手を通じた一対一対応を考えられる場合があります)
補足としては、自己函手圏$ \cancel{\mathbb{C}^{\mathbb{C}}}Hom 集合および自己積圏$ \mathbb{C} \times \mathbb{C}における対象や射を、$ \mathbb{C}内部に埋め込める場合を デカルト閉圏 と呼びます (より厳密には、もう少し条件が必要ですが)
なお、型とプログラムの圏はデカルト閉圏としての性質を持ち、なおかつ対象$ (C^B)^A \Leftrightarrow C^{A \times B}の対応は curry / uncurry の組として知られています
対象が２つの離散圏$ 2^\bullet(対象が$ 0と$ 1で、射が恒等射$ \mathrm{id}_0と$ \mathrm{id}_1のみ)を考えると
函手$ \mathbf{F} : 2^\bullet \rightsquigarrow \mathbb{C}とは、圏$ \mathbb{C}から（重複を許して）２つの対象$ A_0と$ A_1を取り出しているのみ（射の対応は恒等射同士の対応しかないので無視できる）
函手$ \mathbf{F} : 2^\bullet \rightsquigarrow \mathbb{C}と$ \mathbf{G} : 2^\bullet \rightsquigarrow \mathbb{C}の自然変換$ \theta : \mathbf{F} \rightarrow \mathbf{G}とは、圏$ \mathbb{C}から（$ \mathbf{F}によって）取り出した対象$ A_0,$ A_1と（$ \mathbf{G}によって）取り出した対象$ B_0,$ B_1の各々の間に射$ \theta_0 : A_0 \rightarrow B_0,$ \theta_1 : A_1 \rightarrow B_1を考えることに他ならない。（図式の可換性も恒等射しかないので明らか）
つまり元の圏$ \mathbb{C}から２つの対象と２つの射を取り出して、ペアにしたものが$ \mathbb{C}^{2^\bullet}であり、記号的な整合性がとれていることが確認できる
Re: はい、おっしゃる通り$ \mathbb{C}^{2^\bullet}と$ \mathbb{C} \times \mathbb{C}には対応関係がつくれますが、あくまで函手を通じた対応関係にしかならないというところに注意が必要ですね 👨🏫
別の例も考えた
対象が２つで、その間の射が１つだけある圏$ 2を考える
対象は$ 0と$ 1
射は恒等射$ (0, 0),$ (1, 1)と$ 0から$ 1への射$ (0, 1)
射の合成は自明
圏$ 2から別の圏$ \mathbb{C}への函手$ \mathbf{F}を考える
対象の対応は圏$ \mathbb{C}の２つの対象$ A_0と$ A_1を選ぶことに相当する
射$ (0, 1)の函手$ \mathbf{F}による移り先は$ A_0から$ A_1への射$ f : A_0 \rightarrow A_1に対応する。
圏$ 2から圏$ \mathbb{C}への函手$ \mathbf{F}を圏$ \mathbb{C}の射$ fと同一視できるのではないか？
函手$ \mathbf{F}による射$ (0, 1)の移る先が$ f
逆に圏$ \mathbb{C}の射$ g : A \rightarrow Bに対して、$ 0を$ Aに対応させ、$ 1を$ Bに対応させ、$ (0, 1)を$ gに対応させる$ 2から$ \mathbb{C}への函手$ \mathbf{G}を考えることができる
圏$ 2から圏$ \mathbb{C}への函手$ \mathbf{F}と$ \mathbf{G}の間の自然変換$ \thetaを考える
函手$ \mathbf{F},$ \mathbf{G}各々による$ (0, 1)の移り先となる射を$ f : A_0 \rightarrow A_1,$ g : B_0 \rightarrow B_1とすると、自然変換$ \thetaは$ A_0から$ B_0への射$ \theta_0と$ A_1から$ B_1への射$ \theta_1から成り、$ \theta_1\circ f = g \circ \theta_0となっている
先の同一視の下で圏$ 2から圏$ \mathbb{C}への函手圏$ \mathbb{C}^2とは、$ \mathbb{C}の射を逆に「対象」とみなして、射$ f,$ gに対して、$ \theta_1\circ f = g \circ \theta_0を満足する射の組$ (\theta_0, \theta_1)を射の間の射$ (\theta_0, \theta_1) : f \rightarrow gのように考えることもできる
函手圏の定義が非常に抽象的なので、圏$ \mathbb{C}を元にして別の圏を作り出す試みの多くが函手圏として捉えなおすことができそうな気がしてくる
圏と函手の概念を得ることで、圏を「対象」として、函手を「射」とする圏の圏（なんのこっちゃ）を考えることが可能か
圏$ \mathbb{C}から圏$ \mathbb{D}への函手全体$ \mathrm{Hom}(\mathbb{C}, \mathbb{D})は集合とはならなさそうなので難しいか
Re: いえ、それは実際に 圏の圏 Cats と呼ばれるものを構成します
Hom が集合となるかは、圏論で取り扱うものにとって本質では無く、あくまで公理を満たすかのみが重要ですね 👨🏫
もちろん、(通常の意味での) 集合となる方が取り扱いやすいのは確かですが 🙄
残っている疑問・質問事項
※ 函手への見解を述べるとき、特に断りなく "グロタンディーク宇宙" を仮定します
しりとりの圏において、50 音間の関数はそれぞれ区別がつけられないのでは？
Re: しりとりの圏で用いている射は、(集合論的な意味での) 関数では無いですね
また、対象も集合ではないです (なので、ひらがなを 1 つだけ含む単集合を表してはいません)
というわけで、確かに集合論的には「単集合から単集合への関数」は 1 つしか存在しないですが、しりとりの圏のセッティングにおいては何も問題はありません
Hom 集合は関数の集合では無いんですか？
Re: はい、違います
(集合論的な意味での) 関数の集合となるのは、集合の圏 Sets においてのみです
劣自然変換の例でも、縦向きの射をうまくとれば自然変換になる気がしますね
Re: はい、正しいです
例えば、$ \theta_\bullet =りんごし，$ \theta_\star =ごしりとり，のように取ると、自然変換になりますね
函手圏の表記を$ \mathbb{D}^\mathbb{C}のようにしているのは、関数の集合と似たような表記を採用したから？
Re: はい、ベースアイデアは間違いなく配置集合 (関数の集合) の表記から取っていると思います 👨🏫
「圏として同じである」とはどのように定義されるのでしょうか？
Re: 対象集合と射集合を定めて、外延性の公理を用いて検証すれば良いかと思います
もう少し弱めてもよければ、圏$ \mathbb{C}と圏$ \mathbb{D}に函手 / 逆函手$ F : \mathbb{C} \leftrightsquigarrow \mathbb{D} : F^{-1}を定められるとき、圏同型 と呼びます
(余談) なぜか圏論では "圏同値" の方が "圏同型" より弱い条件になっています 🤔
函手が一致するとはなにか？
Re: 対象集合に対する写像の一致と、射集合に対する準同型写像の一致を調べれば良いですね
「合成函手」や「恒等函手」のようなものをどのように定式化するか？
Re: 恒等函手は、対象集合への恒等関数 / 射集合への恒等関数，その 2 つ組として得れば良いです
合成函手は、対象集合への合成関数 / 射集合への合成準同型写像，その 2 つ組として得れば良いです
はい、函手圏では対象が "函手で移した構造全体"，射が "自然変換" で、それ以外には構成要素は存在しないという認識で問題ありません
函手 F と G は任意に取って問題ないので、F と G の双方に同じ函手を割り当てる場合も問題ありません
F で移した構造自身に戻る射として書いた方がわかりやすければ、もちろんそれで問題ありません 👍
Re: $ \forall X. \theta_X \circ \forall X. id_{F(X)}は、射として函手圏のものを考えていて、なおかつ合成演算$ \circも函手圏における射の合成を考えていますよね
なので、どちらかというと$ \forall X. \theta_X \circ \forall X. id_{F(X)} = \forall X. \theta_X \circ_{\textcolor{red}{\mathbb{D}}} id_{F(X)}という等式自体が、函手圏における合成の定義 と捉えてあげると良いかと思います
Re:Re: ありがとうございます。
一つには自然変換の可換性とかが効いているのかもとも思ったのですが函手圏だと 1 函手 1 対象で対象が 1 つにまとまっているので関係なさそうですね。
もう一つは ↓ 3 つ以上の函手による函手圏がある前提で、図で$ ψ_A \circ φ_B みたいなものを考えるのかという気持ちだったのですが$ G[A] = G[B] なので単に表記上交差しているように感じるだけな気がしてきました。あるいはこんな構成ができないかも？
https://gyazo.com/f7d876b199d4c8b0a95f1c2a6b804aa7
同様に、資料上は 2 つの函手についての函手圏ですが 3 つ以上の函手について函手圏を考えることはあるのでしょうか？その場合、3 つの対象の間で射 (自然変換) がどう繋がっているかについても複数の可能性 (三角形，直線) がありそうですが。
Re:Re:Re: 可換となる領域が (対象を潰したとしても) 四角形であるかは本質ではなく、あくまで添え字づけられた対象それぞれに閉領域を可換とする射を用意できるか？，というところが大事ですね 👨🏫
というわけで、例で挙げていただいているくびれた図式も、自然変換が 2 つあることを示す図式として問題ないです 👍
また、複数函手があれば複数自然変換がありえますし、可換となる領域が複数あることになりますが、これは帰納的にどの経路を辿っても可換であることが言えます