圏論：米田埋め込みと射の社会性 - 檜山正幸のキマイラ飼育記 (はてなBlog)

[追記]このエントリー「圏論：米田埋め込みと射の社会性」は、まったくのトンチンカンでした。ryoさんのご指摘のとおり、∀k.(k;f = k;g) を仮定するなら、kにidを入れれば即座に f = g が出るので、それ以上の議論は論理的には何の意味もありません。

「論理的には何の意味もない」のですが、なんか気分的には、あるいはスローガン的には意味があるような気がしなくもないので、このエントリーはそのまんまで残しておきます。事情と言い訳は「昨日の内容への謝罪＋圏もどきから圏を作る話」に書いてあります。[/追記]

圏の射とはなにか？ -- 圏の定義からは、この疑問に何一つ答えることができません。具体的な圏の例が与えられれば、射は写像だとか図形だとか物理過程だとか言えるでしょうが、一般的には「なんでもいい」としか言いようがありません。

しかし、次の事実は「射がなんであるか」にヒントを与えてくれる気がします。（以下、「⇒」は含意記号です。）

∀k.(k;f = k;g) ⇒ f = g

この命題が言っていることは、射を「他の射への（結合を介した）働き」と見て、同じ働きをするならそれは同じ射だということです。つまり、射の同定（あるいは識別）は、他の射との関係性でなされる、ということです。もし他の射との関係を完全に捉えることができたなら、それにより射の同一性の判断ができることになります。

またこのことは、「射がなんであるか」に対して、個々の射の実体を持ち出しても無意味だということを再確認しているようにも思えます。射（個人）の同一性は、圏全体（社会）のなかでの役割で規定されているのであって、「圏＝社会」と無関係な「個人＝射」の特性は問題にされないのです。

もう少し正確に社会性を述べると

「∀k.(k;f = k;g) ⇒ f = g」は大雑把な書き方なので、もう少し精密にしましょう。この命題のなかのfとgは同じ域と余域を持ちます。f, g:A→B とします。kは X→A の型です。等式 k;f = k;g が意味を持つためには、これらの条件が要求されます。

k;f が意味を持つなら、cod(k) = dom(f)
k;g が意味を持つなら、cod(k) = dom(g)
k;f = k;g が意味を持つなら、cod(k;f) = cod(k;g)

これらから、dom(f) = dom(g) と cod(f) = cod(g) は出ます。

以上のことを明示的に書くと、次のようになります。

∀k:X→A.(k;f = k;g :X→B) ⇒ (f = g :A→B)

対象Xも任意なので、それも書くと：

∀X.[∀k:X→A.(k;f = k;g :X→B)] ⇒ (f = g :A→B)

今考えている圏をCとして、ホムセットを使って記述すると次のようです。

∀X∈|C|.[∀k∈C(X, A).(k;f = k;g :X→B)] ⇒ (f = g :A→B)

米田埋め込み

米田埋め込みを復習します。圏のベキ D^C を [C, D] とも書くことにします。C^op はCの反対圏です。Y:C→[C^op,Set] という関手を次のように定義します。

Y(A) = C(-, A):C^op→Set
Y(f:A→B) = C(-, f:A→B)::C(-, A)⇒C(-, B):C^op→Set

Y(A)は、対象Aによる反変主表現、Y(f)は反変主表現のあいだの変換となっています。表記を簡単にするために、Y(A) = A~, Y(f) = f~ と書くことにします。この記法で、Yの定義をもう一度書いてみます。f:A→B in C とします。

A~(X) = C(X, A) ∈|Set|
B~(X) = C(X, B) ∈|Set|
f~_X:C(X, A)→C(X, B) in Set
f~_X(k) = k;f

最後の2行の部分を次のように書くことにします。

f~_X:C(X, A)→C(X, B); k |→ k;f

射の社会性は、米田埋め込みの存在

冒頭に挙げた ∀k.(k;f = k;g) ⇒ f = g は、射が社会的存在であり、全体との関係性のなかで同一性が規定されていることを示します。このことは、米田埋め込みが存在することと内容的に同一です。

前節に示した関手 Y:C→[C^op, Set] （Y(-) = (-)~）は、米田埋め込みと呼ばれますが、これが実際に埋め込みであるとは、次のことを意味します。

A|→A~ : |C|→[C^op, Set] が単射である。
各A, Bに対して、f|→f~ :C(A, B)→[C^op, Set](A~, B~) が単射である。

2番目のほうの条件は忠実性と呼ばれたりもします。圏のベキ（関手圏）[C^op, Set]のホムセットは、自然変換の集合なので、Nat(A~, B~) のようにも書きます。すると、関手Yの忠実性は次のように述べることができます。

Nat(A~, B~) のなかで f~ = g~ ならば、C(A, B) のなかで f = g である。

ところで、f~とg~は自然変換なので、それが等しいことは各成分が等しいことです。

f~ = g~ ⇔ ∀X.(f~_X = g~_X)

f~_X:C(X, A)→C(X, B); k |→ k;f を思い起こすと、f~_X = g~_X は次のように書けます。

∀k∈C(X, A).(k;f = k;g :X→B)

もう一度 f~ = g~ のあからさまな表現を書いてみると：

f~ = g~ ⇔ ∀X∈|C|.∀k∈C(X, A).(k;f = k;g :X→B)

これと、(-)~ の忠実性「f~ = g~ ⇒ f = g」を組み合わせると：

∀X∈|C|.[∀k∈C(X, A).(k;f = k;g :X→B)] ⇒ f = g

となり、射の社会性が出てきました。

「同じ」の定義

普通の集合論だと、2つの集合が同じことを次のように規定します。

a = b ⇔ ∀x.(x∈a ⇔ x∈b)

これは「外延性の原理」ですが、集合が同じかどうかは、含まれる要素で決まってしまうということです。

ライプニッツは、次のようなことを言っていたみたいです。（詳しいことは知りません！） a, bはモノで、pが性質（属性）だとすると：

a = b ⇔ ∀p.(p(a) = p(b))

つまり、同じ性質を持つ2つのモノは、性質から区別できないから同じモノだということでしょう。

今日話題にした圏論における「同じ」をあえて書くなら次のようです。

f = g ⇔ ∀k.(k;f = k;g)

形は、外延性の原理やライプニッツの原理と似ています。使われている基本記号が所属や性質ではなくて、結合（合成； composition）です。結合という演算を介した他者（他射）との関わりのみで「同じ」が決まってしまうことを主張しています。

こういう基本原理が、米田埋め込みと事実上同じ主張だということから、米田埋め込み（やその元になる米田の補題）が、圏論の本質的な部分を構成していることが見てとれます。