mathink氏とぱぶりさんの圏論カウンセリング

k @mathink

自己弁護のために今ツイヰトしておきますが，勉強中の身です．問答により自分の理解を深めることが目的(の一つ)です．

あいや🐕 @public_ai000ya

@mathink ありがとうございます！ 嬉しいです！ ではでは…確認させてください。 圏の定義は "(全ての射の集まり)と(全ての対象の集まり)の集まり" であってますでしょうか。

k @mathink

@public_ai000ya 「全て」が指す範囲はどこでしょう ?

あいや🐕 @public_ai000ya

@mathink あ、これはHask圏での話と混じって考えていました…！ 圏論の圏での「全て」はまだわかりません…。(続

あいや🐕 @public_ai000ya

@mathink Hask圏ならば、 全ての関数の集まりとは "Haskellの持つ関数全て"、 全ての型の集まりとは "(Maybe aなどの一種の型の集まり)を含めた、Haskellの持つ型全て" であってますか？

k @mathink

@public_ai000ya 概ね OK です．

あいや🐕 @public_ai000ya

@mathink やった！！ そして、 f :: Int -> Bool における対象は IntとBoolの2つ。 「fは対象Intを定義域とし対象Boolを値域とする射」 あっていますか？

k @mathink

@public_ai000ya 後半部はよいのですが，前半部の「f :: Int -> Bool における対象は」という言い回しが少し気になります． 各対象そのものは，射があろうとなかろうと存在しています．

あいや🐕 @public_ai000ya

@mathink ！！ "射f は 対象Intを定義域とし対象Boolを値域とする射です" こうでしょうか。

k @mathink

@public_ai000ya そういうことです! 細かい話をすると，全ての対象は恒等射を持つので，つまり射があってこその対象じゃないか，と言えなくもないのですが，一応は射と対象はそれぞれ独立に存在していて，圏はそれらの間の関係を記述している，と考えると良いです．

あいや🐕 @public_ai000ya

@mathink ！ では……ここがとても知りたかったところなのですが……この段階で質問してしまっていいのかな。 実際にHask圏における圏とは、 どのような状態であれば圏と呼べるのでしょうか…。

k @mathink

@public_ai000ya ぼちぼちかな，と思っていたのでちょうどよいかもですね． これから数度の問答で応えていきたいと思います． まずは，基礎の部分から見直していきましょう． 圏とは何か，を述べてみてください．

あいや🐕 @public_ai000ya

@mathink 圏とは… "(射の集まり)と(対象の集まり)の集まり" でした…よね…。

k @mathink

@public_ai000ya はい，そうです． 今の質問は確認のためでもありますが，定義というものは都度思い出しておくことが大事ですので，そんな意味合いもあります．

あいや🐕 @public_ai000ya

@mathink はい、 定義は重い、定義は重い、定義は…大切！！

k @mathink

@public_ai000ya 数学絡みでわからない用語があった場合は，定義と具体例，両者を参照しましょう．大抵の場合はどんどんとわからない用語が増えますが，わからない度は下がっている(はず)なので，頑張って遡るといつか知ってるところまで辿り着く(可能性が多分高い)と思います．

あいや🐕 @public_ai000ya

@mathink ！！ はいっ！！

k @mathink

@public_ai000ya (注釈は現実を反映しています)． さて，改めて圏の定義を述べますね． 圏とは「 "(射の集まり)と(対象の集まり)の集まり" で幾つかの性質を満たすもの」です． ”幾つかの性質を〜” の件は今は気にしなくて良いと以前言ったのを覚えていますか ?

あいや🐕 @public_ai000ya

@mathink はい。 ええと…何か……恒等射が1つ以上あることと……えーと…

k @mathink

@public_ai000ya 存在さえ覚えているのなら OK です． その性質たちについては今は気にしないでおきましょう． Hask 圏の話の途中で具体例で以って触れるのがわかりやすいので，その時に説明しますね．

あいや🐕 @public_ai000ya

@mathink はい！！

k @mathink

@public_ai000ya では，ぼちぼち「Hask 圏」について考えてみますか． さきほど，"Haskellの持つ関数全て" と "Haskellの持つ型全て" という 2 つの「集まり」が出てきましたね． まずは，ここから何が思い浮かぶか考えてみましょう．

あいや🐕 @public_ai000ya

@mathink はい！ ………えっ！？ えーと……思い浮かびすぎて……わかりません…。

k @mathink

@public_ai000ya いっぱい思い浮かんでいますか． では，その状態で改めて圏の定義を考えてみてください．

あいや🐕 @public_ai000ya

@mathink うーあー…… "(全ての関数の集まり)と(全ての型の集まり)の集まり"…。 多相型も "型の集まり" …。 ということは… 思い浮かぶのは… 多相型を対象にした関数もやはり"関数の集まり"になるのかな… ってところでしょうか…。