前順序集合に関する試行錯誤
に関する議論ログ
木が複雑で辛いのでおよそ時間軸にした
議論に関係なさそうなものを切り落とした
きっかけ
たかだか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個しかないっていう条件いらなくない？takker.icon
射の類が空かどうかだけで前順序の性質を導けてしまった
このツリーしか読んでないので全然わからないけど雰囲気でコメントしておくnishio.icon
AとBが互いに同じであるというためにはAならばBであることと、BならばAであることの両方を言わなければならないと思う
ここでは前順序集合を導くことができる、という一方向の説明しかしてないように見える
しかも「CならばB、BならばA」を示して「Cで十分Aだ！Bの条件を使ってない！」と言ってるように見える、そりゃあそっち方向はそうだろう、という気持ち
今回は$ B\land C\implies Aになるという説明だったけど、解いてみたら$ C\implies Aだったということですtakker.icon
逆っているのかな？
逆っているのかなtakker.icon
逆は「任意の全順序集合は、圏で表現できる」かな
これは全順序集合$ (S,\le)の$ Sを$ {\rm ob}({\bf A})に、$ A\le Bを$ {\bf A}(A,B)\neq\varnothingに対応させれば圏で表現可能です
(後のコメント)これ違う。射を構成できていない(後述)takker.icon
上の推論で、十分逆も示せている感じがする
前順序の表現の違い？
前順序$ \le を圏の道具でどう表現するかの違いだろうかtakker.icon i: テキストでは、$ A \le Bの真偽を$ {\bf A}(A,B)の個数に対応させている
trueなら1個、falseなら0個
後ほどテキストを確認したところ、jと同じく存在条件だけを対応させていた
「射が高々1個」だと事前に書かれていたので、それと合わせてiになっていた感じ
j: takker.iconは、$ A\le Bの真偽を$ {\bf A}(A,B)が空でないかどうかに対応させている
trueなら空、falseなら空でない
他の文献もあたって調べたほうがよさそう
前順序$ \leが反対称律$ \forall A,B\in S. A\le B\land B\le A\implies A=Bを満たす時、$ (S,\le)を半順序集合(poset)と呼ぶ ここでもし射がたかだか1個であるような圏だとすると、$ A\le B\land B\le Aは$ A\cong Bと等しくなる
TODO：証明
A, B, Cの明示
今回は$ B\land C\implies Aになるという説明だった
ここが事実でないと思っているnishio.icon
が、もう少し読んでみることにする
多分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の両方を言う必要がある
たぶんそうではないですtakker.icon
自分もこれ解いているときは理解していなかったのですが、おそらく「X,Yが本質的に同じ」とは「XとYに一対一対応が存在する」ということだと思います
言い換え
XでYを構成できるし、YからXも構成できる
矢印で表現したかった概念はこれnishio.icon
「BからCが構成できないよね？」ということが言いたかった
XとYとの間に全単射な函数が存在する
全単射があるだけではなくて、その「函数」が構造を維持する写像であることが必要かとnishio.icon
たしかに(前述)takker.icon
例
数列$ a_iと無限次元vector$ (a_0.a_1,\cdots)は本質的に同じ
$ a_iを全部並べて組にすればvector$ (a_0.a_1,\cdots)になるし
自然数$ iからその番号にあたるvectorの成分$ a_iを返す函数を作れば、それが数列になる
+1nishio.icon
定義はまだまだ先のほうにあるやつなのでお預け
$ \impliesの意味
今回は$ B\land C\implies Aになるという説明だったけど、解いてみたら$ C\implies Aだったということですtakker.icon
矢印で表現したかった概念はこれnishio.icon
$ \impliesは構成を意味していたんですね。理解しましたtakker.icon
そもそも僕が最初に書いた時には$ \impliesを使っていなかったはずなので、自分で書き換えたのでは？nishio.icon
マジですか、確かに自分が書き換えたかも。ごめんなさい……takker.icon
「射が高々1個しかない」は前順序集合から圏を構成するために必要かも
で、ここまで書いて気づいたのですが、「射が高々1個しかない」は前順序集合から圏を構成するために必要かもしれませんtakker.icon
前順序集合で圏を表現するのは無理かも
射が高々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は言えない
圏(C)で前順序集合(A)を構成できるが、前順序集合(A)で構成できるのは射が高々1個しかない圏(B)までで、任意の圏(C)は(多分)構成できない
「多分」と濁したのは、「前順序集合から構成できない圏が存在する」ことをまだ証明していないから
多分あるんだろうけど、どう証明したものか……
気が向いたらそのうちやる
図を描いた
図を描いたnishio.icon
https://gyazo.com/ce0f87369fd20824d89d8d5ee86bec79
$ \forall A,B\in{\rm ob}({\bf A})にて$ {\bf A}(A,B)\neq\varnothingを$ A\le Bと対応させるtakker.icon
このタイミングでCからBへの変換が行われており、その後BとAが「本質的に同じ」であることからほぼ無意識にBとAを同一視してて、その結果
射が高々1個しかないっていう条件いらなくない？takker.icon
という発言に至っている
しかし「射が高々1個しかないっていう条件」なしに「本質的に同じ」と主張するのであればBからCに戻せる必要がある
「そんなことできないよね？」が指摘したいこと
あー、わかってきた
僕はテキストを持ってないのでどこがテキストに書かれている内容か知らないから、予断なく「これはおかしい」って言うんだけど、それがテキストに書いてある文言の場合takkerさんの方は「間違っているはずがない」って思うわけね
でも実際には解釈や使い方や文脈が間違ってたりすることがある
「$ {\bf A}(A,B)\neq\varnothingを$ A\le Bと対応させる」とテキストに書いているなら、それは「任意の圏について」という文脈ではなく「すべての射の類が1個以下しか射を持たない圏について」という文脈であったはず(僕の図で言うところのB)
あってますtakker.icon
なのにそこに「(射が高々1個しかないっていう条件のない)任意の圏」(C)を入れてしまった
これがおかしい
(C)を入れたというより、「そのうち(B)の条件つかうんだろうなあ」と思いながら解いたら、どこでも使わずに解けてしまったので「なにこれ」と疑問に思った次第takker.icon
理由は↓
しかしたまたま$ \neq\varnothingが射が複数個あってもエラーにならない書き方なのでそのまま進んでしまった
そうそうtakker.icon
その結果前順序の性質を導けてしまった
あれ？射が高々1個しかないっていう条件いらなくない？takker.icon
射の類が空かどうかだけで前順序の性質を導けてしまった
それだとCからAが導けてはいるけど、AからCが導けるはずがないので僕からはこう見えた:
AとBが互いに同じであるというためにはAならばBであることと、BならばAであることの両方を言わなければならないと思うnishio.icon
ここでは前順序集合を導くことができる、という一方向の説明しかしてないように見える
しかも「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
とする、ということ。こう書いていれば誤解の余地はなかった
そういうことですね。たぶん認識あいましたtakker.icon
テキストからAからCへの証明の必要性が読みとれなかったこと(たぶん書いてない)、最初にnishioさんに指摘されたとき、AからCも導けると間違えてしまったことが混乱に拍車をかけてしまったっぽい
念のためテキストの該当部分を後ほど引用しておきますtakker.icon
(TODO:このページのどこに配置するか考える)
前順序集合は，各$ 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が存在する」とあったので、それだけ使って証明してしまった
(takker.iconは$ {\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という言明または主張と考えることができる．
takker.iconの読解能力だと、ここまでで「前順序集合から射が高々一つしかない圏を構成する」旨の話がでていなかった
それもあって、逆の証明が必要であることに気づかなかった
テキストでは一方方向しか説明していない
「PならばQ」という形をしていれば、すぐ逆が示されていないことに気づいたのだろうが、「aはbと本質的に同じ」「aはbとみなせる」という論理的含意を使っていない形だったため、逆があることに気づかなかった
「本質的に同じ」を論理式でどのように定式化するか不明だったのもある
厳密な定式化には圏同値が必要らしいがまだアンロックされていない
厳密な定義から積み上げるのではなく色々な分野とのアナロジーで進める本なので、僕は「本質的に同じ」を「同型みたいなもの」と解釈したnishio.icon https://gyazo.com/b21ce0b948e839931a56c67852ef3041
これも同じニュアンス
なるなるtakker.icon
整理し直した後のコメント
前順序の表現の違い？
これが正しい気づきだったがその気づきが書かれていることに気づいてなかったnishio.icon
構成/含意
この議論においては区別する意味はなさそうnishio.icon
取り扱っているものが項か命題かで混乱したけど、やってることはまあ一緒takker.icon
A,B,Cの定義の疑問takker.icon
C:「すべての射の類が1個以下しか射を持たない」条件のない圏
「なんの条件も課せられていない任意の圏」ということであってますか？takker.icon
yesnishio.icon
「すべての射の類が1個以下しか射を持たない圏」と対比してる
B:すべての射の類が1個以下しか射を持たない圏
CからBへは
$ \forall A,B\in{\rm ob}({\bf A})にて$ {\bf A}(A,B)\neq\varnothingを$ A\le Bと対応させる
にて可能
条件を追加した厳しいものへの変換を行なっている
ここちょっとわかっていないtakker.icon
「CならばB」は「CからBを構成可能である」と同じ意味 (なはず)
yes、なので構成/含意 この議論においては区別する意味はなさそうと思ったnishio.icon
だが$ \forall A,B\in{\rm ob}({\bf A})にて$ {\bf A}(A,B)\neq\varnothingを$ A\le Bと対応させるはCからAを構成する方法であって、CからBを構成する方法ではない
yesnishio.icon
「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かな？mrsekut.icon
です。指摘サンクスですtakker.icon