haskell-jp / math #11 at 2023-01-13 23:18:26 +0900

対象が集合で射が関数の圏と対象が同じく集合だが射が包含関係の圏の間には関手はあるでしょうか?

ちょっとは圏論に慣れ親しんでこれたと思うので、調子に乗って大学数学の本を読みつつ圏論で考えるとどういう感じだろう?というのをまとめてみたいと思って、まず集合論の基本的なところを読んでいたところです。
読んでいる本の冒頭では集合の和や共通部分を取ったり包含関係をみたりなどの演算から始まっているのですが、これを圏としてみた時には対象が集合で射が包含関係になると思います。

ただ、今まで集合の圏として慣れ親しんできたのは射が関数の圏です。
そこでふと、この二つの圏を結ぶ関手は(あるとして)どういうものになるかと思いまして。。

こんな質問を出しておいてなんですが、今の考え的には包含関係を関数に写すこともその逆も出来なさそうなので直接の関手は無いのではないかと考えています。
あるとして対象が集合の離散圏からそれぞれに埋め込む関手があるくらいなのかなと思っています。

こちら認識が合っているかご教授いただけましすと幸いです。
射が関数の圏から射が包含関係の圏への関手は定関手しかないような気がします(空でない圏への定関手は必ず存在する)。
射が包含関係の圏から射が関数の圏へは包含関係から集合の埋め込み関数を作れますね。(他にも定関手を含めいろいろありそうです)
前者はもう少しあって、空集合の送り先 X と、そのほかの対象の送り先 Y を選択して、さらに X から Y への埋め込みの選択の分くらいありますね。
お二方ともありがとうございます!
定関手の存在初めて知りました!が二つの圏の関係性を何か表すことは無いものそうですね。。
そして埋め込み関数はなるほどでした!これは両者の関係性を見せてくれている感じがします。。!
空集合の送り先とそれ以外の送り先の関手が作れるのは、空集合から出る射だけがあって空集合に入る射が絶対にないからという感じでしょうか?
絶対にX→Yという形になり、かつこういう関係性が射が包含関係の圏に存在するはずという認識をしましたがあっていますでしょうか?
Set から SetOrd へ対象をそのまま保つ関手が作れないのは、包含関係がないとき Set の射を対応させる先がないからですよね。SetOrd をいじって「包含関係がない」という射 n を各 Hom に持たせると、包含関係がないときは Set の射を n に対応させられます。n は他の射と合成するとまた n になるとします。
すると、Set から SetOrd (改) に対象をそのまま移し、射については包含写像があればそれに、なければ n を対応させるという関手が作れるんじゃないかなあと。

全然圏論に詳しくないので思いつきですが… 射の対応について Maybe みたいのがあればなんとかなるんじゃないかと思いまして。
ありがとうございます!
確かにいけそう!と思ったのですが、仮にA⊂Bの時に⊂:B→Aとn:A→Bを合成して⊂∘n=n:A→Aができてしまい各対象が自分自身と比較できないことを示す射ができてしまうのでちょっと難しそうでしょうか。。
n は SetOrd (改) の全てのホムセットに入っているので、n に加えてほかの射があれば包含関係があると考えればいけませんか?
SetOrd(A, A) = { n, id }, SetOrd(A, B) = { n, ⊂ } が包含関係あり、SetOrd(A, B) = { n } を包含関係なしと考えます。⊂∘n=n:A→A の規則はそのままで。
いけそうですね!ありがとうございます。。!
これならSetからSetOrd(改)に上記の関手ができますね。
SetOrd(改)からSetOrdへは割り当てられない射の話のままなので、こちらは定関手などだけになりそうでしょうか。

しかしnはあちこち合成できるので、結果的にすべての対象間に存在しそうなので包含関係なしを超えて何か別の意味合いがありそうで面白そうです。。
暗黙的にすべての対象間を結ぶネットワーク的な何かな感じでしょうか?とりあえずお互いが「ある」ことだけ認識してる感じのような。。
どこにでも含まれるという点は、 Haskell の ⊥ (ボトム, undefined) みたいですね。