こんにちはphi16です。rogy Advent Calendar 2017の20日目の記事です。数学でよく出て来るwell-definedのはなしをします。
well-definedが必要な理由
よく商集合を考えるときにwell-definedが必要って言われることが多いと思います。これは当たり前の要求ではありますが、その存在は非自明に見えてしまいます。
例えば X = \{0,1,2\}, Y = \{-1,1\} としたとき、適当に X \to Y の写像を x \mapsto (-1)^x で取ることには誰も文句を言いません。
でも X = \mathbb{Z}/3\mathbb{Z}, Y = \{-1,1\} のときに x \mapsto (-1)^x って結構やばいのです。
何がやばいかというと \mathbb{Z}/3\mathbb{Z} は別に \{0,1,2\} ではないということです。ちゃんと書くと \{0+3\mathbb{Z}, 1+3\mathbb{Z}, 2+3\mathbb{Z}\} という表現になりますね。
この状況では x = 1+3\mathbb{Z} と x = 4+3\mathbb{Z} は全く同じことを言っていて、区別できない、区別してはいけないのです。
つまり、さっきの写像があると (-1)^1 = (-1)^4 であることになります。これは明らかにおかしい。というわけで「まず写像ではない」のですね。
では何故写像ではなくなってしまったのでしょうか？気持ちとしては単純に元を移したかっただけのはずで、何かそこに根本的な問題があるのでしょうか。
写像と空間的解釈
集合は大体点の集まりで表現できます。そして写像は点から点へのマッピングで表現できます。
今回、もともと点たち \{0,1,2\} は離散的なので、そこからのマッピングというのは各元に対して「好きに」とれます。
では \mathbb{Z}/3\mathbb{Z} はどうでしょうか？
これは違いますよね。 \{0,1,2\} です。
これは \mathbb{Z} です。
これは当たり前ですが、何もおもしろいことを表現しません。もっと元の気持ちから、「何が起きているのか」を言いたいのです。
で、出てくる表現がこれです。
これは「等しいはずの数が紐でつながれている」という状態です。これは確かに「3つの元 (=連結成分) を持つ集合」であり、「もともとの集合の元が見えている」というわけです。
では、ここから \{-1,1\} への写像とは何でしょうか。本来集合には「紐」なんてないんですが、気持ちとしては紐はつながったまま移るべきということがわかるとおもいます。
でも、 1 と 4 の間に紐があるにもかかわらず -1 と 1 の間には紐がありません。もともとつながっていない空間には紐は引けません。
これは明らかにwell-definedではないと言えます。逆につまり、well-definedであるということは紐が繋がったまま写像で移るという条件そのものなのです。
論理の具象化
何故この「紐」が見えなくなってしまうのかというと、集合には論理の情報を自明に反映させることができないということがあります。
mod 3での値を拾いたいだけなのに、 \{0+3\mathbb{Z}, 1+3\mathbb{Z}, 2+3\mathbb{Z}\} と同値類を使わないといけない理由は「後から元を同一視する」ような仕組みが自明には集合にはないということですね。
そこで、論理をそのまま書き下せる環境というものを考えてみたいのです。 \mathbb{Z}/3\mathbb{Z} は次のような性質を持つはずです:
- n \in \mathbb{Z} について、 i(n) \in \mathbb{Z}/3\mathbb{Z} ( x \mapsto x + 3\mathbb{Z} )
- n, m \in \mathbb{Z} について、 n = m\mod 3 ならば i(n) = i(m)
これを以って \mathbb{Z}/3\mathbb{Z} を定義します。できることにします。
そして \mathbb{Z}/3\mathbb{Z} からの写像 f を定義しようとするときに、次の定義を要求されることにします。
- n\in\mathbb{Z} について、 f(i(n)) の値
- n, m\in \mathbb{Z} について、 n = m\mod 3 ならば f(i(n)) = f(i(m)) の証明
これはとても自然なことです。 \mathbb{Z}/3\mathbb{Z} の各定義に対して定義を書くというのはパターンマッチの基本概念ですね。
このとき、well-defined性は自然に出てきます。もともともそうでしたが、well-definedであることを言わなければ写像ですらないのです。
今回もたしかに f(i(n)) = f(i(m)) を示さなければまず写像が定義できない、ということがよくわかるとおもいます。
というわけで、論理を具体的に書き下せる世界がなんだか楽しそうな気がしてきません？
例: [-\pi,\pi) と S^1
2次元上での角度を扱いたい時、単純に考えると [-\pi,\pi) (または [0,2\pi] ) の元として角度を拾うことが多いと思います。
しかし、これでは (よく知られているように) x,y \in [-\pi,\pi) の「距離」は |x-y| ではありません。 \pi 付近では空間がつながっていないからです。
そこで S^1 = \{(\cos\theta,\sin\theta)\mid\theta\in\mathbb{R}\} を使うことでこの間を連続にし、計算も容易になったりするわけです。
が、これは結局 \mathbb{R} の上で \forall x. x = x+2\pi で同一視を入れているわけで、その同一視が入っているという気持ちの元で距離を計算してあげれば \mathbb{R} でもよく振る舞うはずなわけです。
空間上の演算を考えるときはその連続性などに関しても気をつけようということです。更に言うとこの場合は群なので群演算に関してもcompatibleにするとうれしいですよね。
プログラムではなかなかこの辺りのプロパティは表現できないので難しいですが。
何の話だったのか
HoTT のHigher Inductive Typesの話です。もっと「同値性」みたいなものをそのまま空間に取り入れることが出来ると直接的な表現力がだいぶ増えて、扱いが容易になる気がするのです。
色々類似した例とか面白い話とかもあるので読むと幸せになれます。多分。
おわり。
明日はらりおさんの「何か書きたい人生だった」です。