well-definedness と universal map

well-definedness 周りの議論ってわりと何してるのかわかりにくくない? と思って考えてたら universality のほうがわかりやすい気がしてきりしたので書いてみた。

以下  A,  B は集合, E A 上の同値関係。

well-defined とは

写像  f: A/E \to B が well-defined であるとはどういうことか,ということから一応。

まず well-defined であるという述語は,写像そのものに適用されるものというよりは,その定義に適用されるものであることに注意する。確かに言葉の上では「この写像は well-defined である」などという言い方をするのだが,このような言明は普通,写像の定義に伴って表れるものであり,その実際の内容は「今述べた定義は確かに写像を一つ定めている」ということである。したがって意味的には well-defined とは数学的対象に関する概念ではなくその記述方法というメタなレベルのことがらに関する概念であるということになる。

では  f([a]) = e\{a\}写像  f の定義だとしよう。ここで  a は変数であり  [a]  E に関する同値類を表す。右辺の  e\{a\}*1 a を含む式である。変数とは何かとか式とは何かとか言い出すと面倒なことになりそうなので,細かいことは言わないで素朴に解釈することにしてほしい。それと,別に式を使って等式の形で定義を述べなければならないわけではないが,話を簡単にするためにそうした。

これが well-defined であるとはどういうことか。写像  f に渡されるものは  A/E の要素であり,すなわち同値類なのだから,少なくとも建前としてはまず同値類  x \in A/E が与えられ(この時点では代表元は与えられていない), f(x) を定めなければならない。そのために同値類から代表元  a \in x を取って云々,とやるのだから, a のとり方を変えたときに式  e が違う値になってしまうといけない。そのような問題が起きない,ということが well-defined であるということである。正確に書けば  a E a' \implies e\{a\} = e\{a'\} でなければならない。これが確かめられればさっきの  f が確かに写像として定義される,すなわち well-defined であるということが結論できる。こういう話であった。

写像の分解と見る

さっき  e\{a\} は「式である」と雑な言い方をしたが,要するに  a A の元を指示する変数であり, e\{a\} B の元を表すのだから, e\{a\} と書いたのは結局のところ写像  e : A \to B であると思ってもよさそうである。(このあたりはずいぶんいい加減なようだが,そもそも大雑把な話をしているということで見逃してほしい)

そうるすとさっきやったことは見方を変えてこのように理解できる。写像  e : A \to B を与え,それが性質  a E a' \implies e(a) = e(a') を持つことを確認せよ。それができれば確かに  f: A/E \to B が定義されたことになる。これが商集合上の写像が well-defined であると言うときに行われていることである。

ついでに言うとこの  f は, \pi : A \to A/E を射影として  f \circ \pi = e を満たす。つまり,最初に与えた写像  e を射影によって分解することで欲しい写像を得ているのである。

よく見てみると,こちらの見方の中には「定義の記述」のようなものが現れないことがわかる。そうではなくて,いきなり定義しようとしている写像の定義域  A/E を考えないで,まずは商をとる前の  A からの写像を定めよ,そしてそれがある性質を満たしていることを確認せよ,そうすれば望む写像が得られる,と言っている。つまり,いきなり商集合の上の写像を定義しようとするとそれがちゃんと定まるかどうかがわからないので「その定義は well-defined であるかどうか」というメタな話が出てくるのに対して,商をとる前の集合を相手にすることで「別のある写像が要求された性質を満たすかどうか」という数学的対象についての話に置き換わったわけだ。

メタレベルを意識しなくても理解が可能な分,後者の説明のしかたのほうがすっきりしていて分かりやすいように思われる。初学者にとってどうかはわからないが,僕にとってはこちらのほうが納得がいくように感じる。

普遍写像

ところで,これに似たような状況は数学でよく出てくる。いわゆる普遍写像性というやつである。

その言葉でさっきの話をきちんと書くとこうなる。関手  \Delta: \mathbf{Set} \to \mathbf{Setoid} \Delta(X) = (X, \Delta_X) (つまり集合をその上の普通の意味の等しさと組にして setoid とみなす)で定めたとき,setoid  (A, E) から  \Delta への universal arrow が射影  \pi: A \to A/E である。

随伴関手の言葉にすると,上の  \Delta は setoid  (A, E) から商集合  A/E を作る関手の右随伴であると言うことができる。すなわち  \mathbf{Set}(A/E, B) \simeq \mathbf{Setoid}( (A, E), \Delta(B) ) である。また,この同型は  \pi: A\to A/E による引き戻しで与えられる。

普通の議論のしかたをこの表現と対応付けてみる。いま写像  f : A \to B があり,これが  a E a' \implies f(a) = f(a') を満たすとする。これはすなわち, f \in \mathbf{Setoid}( (A, E), \Delta(B) ) を仮定するということに他ならない。このとき, \bar f : A/E \to B であって, \bar f \circ \pi = f を満たすものが一意的に存在する。これは, \pi による引き戻しが全単射であるという上に述べた事実の単なる言い換えである。

*1:あまり標準的でない記法なのは他の括弧を使うと紛らわしかったため