前順序集合に関する試行錯誤
に関する議論ログ
木が複雑で辛いのでおよそ時間軸にした
議論に関係なさそうなものを切り落とした
きっかけ
たかだか1個=0個 or 1個
集合と関係の組(S,\le)が前順序集合であるとは、以下を満たすことと等しい
反射律：\forall A\in S.A\le A
推移律：\forall A,B,C\in S. A\le B\land B\le C\implies A\le C
\forall A,B\in{\rm ob}({\bf A})にて{\bf A}(A,B)\neq\varnothingをA\le Bと対応させる
単位法則より\forall A\in{\rm ob}({\bf A}).{\bf A}(A, A)\neq\varnothingだから反射律を満たすのは自明
推移律は次の推論で求まる
\forall A,B,C\in{\rm ob}({\bf A}).
{\bf A}(A,B)\neq\varnothing\land {\bf A}(B,C)\neq\varnothing
\iff\exist f\in{\bf A}(A,B)\land\exist g\in{\bf A}(B,C)
\iff\exist f\in{\bf A}(A,B)\exist g\in{\bf A}(B,C).g\circ f\in{\bf A}(A,C)
\implies{\bf A}(A,C)\neq\varnothing
\underline{\therefore\forall A,B,C\in{\rm ob}({\bf A}).{\bf A}(A,B)\neq\varnothing\land {\bf A}(B,C)\neq\varnothing\implies{\bf A}(A,C)\neq\varnothing\quad}_\blacksquare
以上より、任意の\bf Aについて({\rm ob}({\bf A}),(A,B)\mapsto({\bf A}(A,B)\neq\varnothing))が前順序集合と同じ構造になることが示せた
(本当は「前順序集合になる」と言いたいのだが、{\rm ob}({\bf A})は集合でないかもしれないので、ごまかした)
あれ？射が高々1個しかないっていう条件いらなくない？
射の類が空かどうかだけで前順序の性質を導けてしまった
このツリーしか読んでないので全然わからないけど雰囲気でコメントしておく
AとBが互いに同じであるというためにはAならばBであることと、BならばAであることの両方を言わなければならないと思う
ここでは前順序集合を導くことができる、という一方向の説明しかしてないように見える
しかも「CならばB、BならばA」を示して「Cで十分Aだ！Bの条件を使ってない！」と言ってるように見える、そりゃあそっち方向はそうだろう、という気持ち
今回はB\land C\implies Aになるという説明だったけど、解いてみたらC\implies Aだったということです
逆っているのかな？
逆っているのかな
逆は「任意の全順序集合は、圏で表現できる」かな
これは全順序集合(S,\le)のSを{\rm ob}({\bf A})に、A\le Bを{\bf A}(A,B)\neq\varnothingに対応させれば圏で表現可能です
(後のコメント)これ違う。射を構成できていない(後述)
上の推論で、十分逆も示せている感じがする
前順序の表現の違い？
i: テキストでは、A \le Bの真偽を{\bf A}(A,B)の個数に対応させている
trueなら1個、falseなら0個
後ほどテキストを確認したところ、jと同じく存在条件だけを対応させていた
「射が高々1個」だと事前に書かれていたので、それと合わせてiになっていた感じ
j: は、A\le Bの真偽を{\bf A}(A,B)が空でないかどうかに対応させている
trueなら空、falseなら空でない
他の文献もあたって調べたほうがよさそう
ここでもし射がたかだか1個であるような圏だとすると、A\le B\land B\le AはA\cong Bと等しくなる
TODO：証明
A, B, Cの明示
>今回はB\land C\implies Aになるという説明だった
ここが事実でないと思っている
が、もう少し読んでみることにする
多分A,B,Cの指すものを明示しないと食い違うので整理
C:「すべての射の類が1個以下しか射を持たない」条件のない圏
B:すべての射の類が1個以下しか射を持たない圏
CからBへは
>\forall A,B\in{\rm ob}({\bf A})にて{\bf A}(A,B)\neq\varnothingをA\le Bと対応させる
にて可能
条件を追加した厳しいものへの変換を行なっている
C\implies B
A: 前順序集合
BとAが「本質的に同じ」とは「Bの条件からAが導けて、かつAの条件からBが導ける」という意味
B \implies AとA \implies Bの両方を言う必要がある
今回はC \implies BとB \implies AからC \implies Aを導いて「射が高々1個しかないっていう条件いらなくない？」と言っているが、その条件は A \implies Bを言うために必要
BとCは「本質的に同じ」ではないので、B \implies Cは言えない
❌述語論理に書き換えた
(書き換えて戻したのでどちらがどちらの発言かわからなくなった、上の\impliesもどちらが書いたかわからない)
「本質的に同じ」とは？
>BとAが「本質的に同じ」とは「Bの条件からAが導けて、かつAの条件からBが導ける」という意味
> B \implies AとA \implies Bの両方を言う必要がある
たぶんそうではないです
自分もこれ解いているときは理解していなかったのですが、おそらく「X,Yが本質的に同じ」とは「XとYに一対一対応が存在する」ということだと思います
言い換え
XでYを構成できるし、YからXも構成できる
矢印で表現したかった概念はこれ
「BからCが構成できないよね？」ということが言いたかった
XとYとの間に全単射な函数が存在する
全単射があるだけではなくて、その「函数」が構造を維持する写像であることが必要かと
たしかに(前述)
例
数列a_iと無限次元vector(a_0.a_1,\cdots)は本質的に同じ
a_iを全部並べて組にすればvector(a_0.a_1,\cdots)になるし
自然数iからその番号にあたるvectorの成分a_iを返す函数を作れば、それが数列になる
より正確には圏同値だと思う
+1
定義はまだまだ先のほうにあるやつなのでお預け
[*** \impliesの意味]
>今回はB\land C\implies Aになるという説明だったけど、解いてみたらC\implies Aだったということです
こう返信したときは「CならばB」を論理含意と捉えていたが、そこそこまあまあ精密に読む『ベーシック圏論 普遍性からの速習コース』#65dae9f01280f000005a51d2によると「CからBを構成できる」という意味だったっぽい？
>矢印で表現したかった概念はこれ
\impliesは構成を意味していたんですね。理解しました
含意のことかと勘違いしていました
そもそも僕が最初に書いた時には\impliesを使っていなかったはずなので、自分で書き換えたのでは？
マジですか、確かに自分が書き換えたかも。ごめんなさい……
「射が高々1個しかない」は前順序集合から圏を構成するために必要かも
で、ここまで書いて気づいたのですが、「射が高々1個しかない」は前順序集合から圏を構成するために必要かもしれません
前順序集合で圏を表現するのは無理かも
射が高々1個しかない圏なら前順序集合で表現できそう
構成方法
{\bf A}(A,B)=\{(A,B)\}\lor{\bf A}(A,B)=\varnothing
(A,B)\in{\bf A}(A,B)\iff A\le B
組(A,B)を射とし、(A,B)があることをA\le Bと対応付ける
この構成方法だと射は必然的に1個以下になる
上の用語を使うと、(A)から(B)を構成する手続きをやっている
>今回はC \implies BとB \implies AからC \implies Aを導いて「射が高々1個しかないっていう条件いらなくない？」と言っているが、その条件は A \implies Bを言うために必要
>BとCは「本質的に同じ」ではないので、B \implies Cは言えない
途中で前順序集合で圏を表現するのは無理かもそこそこまあまあ精密に読む『ベーシック圏論 普遍性からの速習コース』#65dae9f01280f000005a51de と気づきましたが、それをここで指摘されていたんですね
圏(C)で前順序集合(A)を構成できるが、前順序集合(A)で構成できるのは射が高々1個しかない圏(B)までで、任意の圏(C)は(多分)構成できない
「多分」と濁したのは、「前順序集合から構成できない圏が存在する」ことをまだ証明していないから
多分あるんだろうけど、どう証明したものか……
気が向いたらそのうちやる
↑の認識がそこそこまあまあ精密に読む『ベーシック圏論 普遍性からの速習コース』#65db407eaff09e0000e4a2efと一致する、という認識
図を描いた
図を描いた
>\forall A,B\in{\rm ob}({\bf A})にて{\bf A}(A,B)\neq\varnothingをA\le Bと対応させる
このタイミングでCからBへの変換が行われており、その後BとAが「本質的に同じ」であることからほぼ無意識にBとAを同一視してて、その結果
>射が高々1個しかないっていう条件いらなくない？
という発言に至っている
しかし「射が高々1個しかないっていう条件」なしに「本質的に同じ」と主張するのであればBからCに戻せる必要がある
「そんなことできないよね？」が指摘したいこと
当初はこれもできると思っていましたそこそこまあまあ精密に読む『ベーシック圏論 普遍性からの速習コース』#65da9b46aff09e0000182e16が、途中でできないことに気づきました
あー、わかってきた
僕はテキストを持ってないのでどこがテキストに書かれている内容か知らないから、予断なく「これはおかしい」って言うんだけど、それがテキストに書いてある文言の場合takkerさんの方は「間違っているはずがない」って思うわけね
でも実際には解釈や使い方や文脈が間違ってたりすることがある
「{\bf A}(A,B)\neq\varnothingをA\le Bと対応させる」とテキストに書いているなら、それは「任意の圏について」という文脈ではなく「すべての射の類が1個以下しか射を持たない圏について」という文脈であったはず(僕の図で言うところのB)
あってます
なのにそこに「(射が高々1個しかないっていう条件のない)任意の圏」(C)を入れてしまった
これがおかしい
(C)を入れたというより、「そのうち(B)の条件つかうんだろうなあ」と思いながら解いたら、どこでも使わずに解けてしまったので「なにこれ」と疑問に思った次第
理由は↓
しかしたまたま\neq\varnothingが射が複数個あってもエラーにならない書き方なのでそのまま進んでしまった
そうそう
その結果前順序の性質を導けてしまった
>あれ？射が高々1個しかないっていう条件いらなくない？
>射の類が空かどうかだけで前順序の性質を導けてしまった
それだとCからAが導けてはいるけど、AからCが導けるはずがないので僕からはこう見えた:
>AとBが互いに同じであるというためにはAならばBであることと、BならばAであることの両方を言わなければならないと思う
>ここでは前順序集合を導くことができる、という一方向の説明しかしてないように見える
>しかも「CならばB、BならばA」を示して「Cで十分Aだ！Bの条件を使ってない！」と言ってるように見える、そりゃあそっち方向はそうだろう、という気持ち
「すべての射の類が1個以下しか射を持たない圏について」の「{\bf A}(A,B)\neq\varnothingをA\le Bと対応させる」は、より厳密にいうなら
\#{\bf A}(A,B)=1をA\le B
\#{\bf A}(A,B)=0をA\not\le B
とする、ということ。こう書いていれば誤解の余地はなかった
そういうことですね。たぶん認識あいました
テキストからAからCへの証明の必要性が読みとれなかったこと(たぶん書いてない)、最初にnishioさんに指摘されたとき、AからCも導けると間違えてしまったことが混乱に拍車をかけてしまったっぽい
念のためテキストの該当部分を後ほど引用しておきます
(TODO:このページのどこに配置するか考える)
『ベーシック圏論 普遍性からの速習コース』 p.18-19
>前順序集合は，各A,B\in\mathscr AについてAからBへの射が高々一つであるような圏\mathscr Aとみなすことができる．これを理解するために，この性質を満たす圏\mathscr Aを考えよう．対象A から対象Bへのただ一つの射をどの文字を用いて表示するかは重要でない．記録しておくべきなのは，どの対象の組(A,B)に射A\to Bが存在するという性質があるかということである．そこで射A\to Bが存在することをA\le Bと書くことにしよう．
ここで「射A\to Bが存在する」とあったので、それだけ使って証明してしまった
(は{\bf A}(A,B)\neq\varnothingと言い換えて使っている)
> \mathscr Aは圏だから，射の合成がある．つまりA\le B\le CならばA\le C．圏はまた恒等射を持つから，任意のAについてA\le A．つまり結合法則と単位法則が自動的に従うので，\mathscr Aは推移的かつ反射的な二項関係，すなわち前順序をもつ対象の集まりと同じである．ただ一つの射A\to Bは，A\le Bという言明または主張と考えることができる．
それもあって、逆の証明が必要であることに気づかなかった
テキストでは一方方向しか説明していない
「PならばQ」という形をしていれば、すぐ逆が示されていないことに気づいたのだろうが、「aはbと本質的に同じ」「aはbとみなせる」という論理的含意を使っていない形だったため、逆があることに気づかなかった
「本質的に同じ」を論理式でどのように定式化するか不明だったのもある
厳密な定式化には圏同値が必要らしいがまだアンロックされていない
厳密な定義から積み上げるのではなく色々な分野とのアナロジーで進める本なので、僕は「本質的に同じ」を「同型みたいなもの」と解釈した
これも同じニュアンス
なるなる
整理し直した後のコメント
>前順序の表現の違い？
これが正しい気づきだったがその気づきが書かれていることに気づいてなかった
>構成/含意
この議論においては区別する意味はなさそう
取り扱っているものが項か命題かで混乱したけど、やってることはまあ一緒
A,B,Cの定義の疑問
>C:「すべての射の類が1個以下しか射を持たない」条件のない圏
「なんの条件も課せられていない任意の圏」ということであってますか？
yes
「すべての射の類が1個以下しか射を持たない圏」と対比してる
>B:すべての射の類が1個以下しか射を持たない圏
>CからBへは
>\forall A,B\in{\rm ob}({\bf A})にて{\bf A}(A,B)\neq\varnothingをA\le Bと対応させる
>にて可能
>条件を追加した厳しいものへの変換を行なっている
ここちょっとわかっていない
「CならばB」は「CからBを構成可能である」と同じ意味 (なはず)
yes、なので構成/含意 この議論においては区別する意味はなさそうと思った
だが[" \forall A,B\in{\rm ob}({\bf A})にて{\bf A}(A,B)\neq\varnothingをA\le Bと対応させる]はCからAを構成する方法であって、CからBを構成する方法ではない
yes
「C→BとB→AをまとめてC→Aをやってしまっていて、B→AはいいけどC→Bはダメ」と言いたくて分割した
CからBを構成できるかはちょっと頑張ってみたけどだめそう
枝葉
単位法則より\forall A\in{\rm ob}({\bf A}).{\bf A}(A,\sout BA)\neq\varnothingだから反射律を満たすのは自明
↑{\bf A}(A,A)\neq\varnothingかな？
です。指摘サンクスです