昨日の内容への謝罪＋圏もどきから圏を作る話 - 檜山正幸のキマイラ飼育記 (はてなBlog)

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

「論理的には何の意味もない」のですが、なんか気分的には、あるいはスローガン的には意味があるような気がしなくもないので、昨日のエントリーはそのまんまで残しておきます。

さてところで、k;f = k;g のkのところにidを入れればいい、と僕が発想できなかった事情を言い訳に書いておきましょう。実は、ここ数日、idがなかったり、idがあってもうまく機能しなかったりする状況を扱っていたのでした。∀k.(k;f = k;g) とか ∀k.(f;k = g;k ) のような条件は、idなしの状況で使っていたのですが、圏だったらidがあるから、このテの条件が表面に出てくることもないんですよね。ウガー。

圏もどき

圏に似てるけど圏ではないものが色々あります。

有向グラフ -- dom, codはあるが、idも結合もない。
半圏 -- 結合はあるがidがない。
プレ圏 -- 結合が（cod(f) = dom(g)であっても）部分的にしか定義されてない。
E-圏 -- 法則が等式では成立せず、同値関係のレベルでしか成立しない。

これらを総称的にかつ曖昧に圏もどきと呼んでおきます。圏もどきは圏じゃないので、計算がうまくいかなくてイライラするときがあります。圏のなかに埋め込みたいなー、と思います。対象はそのままでいいとして、射を付け足したり、複数の射を同一視して束ねたりすると、圏になってくれることもあります。

有向グラフから圏を作る方法は、「圏論番外：有向グラフのパスの圏（実装付き）」で紹介しました。これは、うまく圏が作れて、そこに圏もどきを埋め込める例です。

「はじめての圏論第6歩：有限変換キューと半圏」では、半圏のなかから部分圏を見つける話をしました。最近僕が出会った状況では、半圏（実際には半圏にもなってない）全体を、より大きな圏のなかに埋め込みたかったのです。

半圏から圏を作る

半圏を圏に埋め込む問題に対して、パスの圏（自由圏）と同様な構成が使えます。Sが半圏だとして、次のようなモノを考えます。

A∈|S| に対して、[A, A] という2項タプル
f:A→B という射に対して、[A, f, B] という3項タプル

これらのタプルの全体に対して次のような定義をします。

dom([A, A]) = cod([A, A]) = A
dom([A, f, B]) = A, cod([A, f, B]) = B
id_A = [A, A]
[A, A];[A, f, B] = [A, f, B]
[A, f, B];[B, B] = [A, f, B]
[A, f, B];[B, g, C] = [A, f;g, B]

タプルの全体をMor(C)として、Obj(C) = |C| = |S| として、圏Cを定義します。S→C という埋め込みを f |→ [A, f, B] として定義すると、半圏Sは圏Cに埋め込まれることになります。

なんか変だぞ

いま述べた構成では、f←→[A, f, B] という対応があるので、もともとSにあった射はCにも存在します。しかし、[A, A] はSの射とは対応しないので、Cで増えた射です。Cで新たに加えられた [A, A] が恒等を与えています。

Sが最初から圏であった場合を考えましょう。Sの対象Aごとにid_Aがあります。id_A←→[A, id_A, B] と対応するので、Sの恒等id_AはCでは恒等ではなくなります。実際：

[A, A];[A, id_A, A] = [A, id_A, A]
[A, id_A, A];[A, A] = [A, id_A, A]

です。ただし、[A, A] 以外に対しては、[A, id_A, A] も恒等のように振る舞います。従来からいたメンバーに対して考えれば、[A, id_A, A] は恒等と言っていいのです。

半圏Sが、まったく恒等を欠いているなら、新たに恒等を付け加えればいいのですが、最初から恒等を（部分的にでも）持っていたとき、以前の恒等が恒等でなくなってしまうのは、どうも不都合に思えました。

従来メンバーから見て同じなら同じ

Sは半圏ですが、部分的に、あるいは全面的に恒等を持っているかもしれないとします。パスの圏と似た方法で作った圏をCとします。SをCに埋め込めるんで、S⊆C のように考えましょう。

Cのなかの2本の射 f, g:A→B の同値性（記号「〜」を使います）を次のように定義します。

f〜g ⇔ ∀k∈S.(k;f = k;g)

このとき、[A, A] と [A, id_A, A] は同一視できるでしょうか？ k∈S は、正確には、k:X→A in S に対して、[X, k, A]の形のCの射を考えることになります。

[X, k, A];[A, A] = [X, k, A] （Cの結合の定義より）
[X, k, A];[A, id_A, A] = [X, k;id_A, A] = [X, k, A] （Cの結合の定義と、Sの結合の定義より）

つまり、もともとSにいた従来メンバー全体の目線からみて、[A, A] = [A, id_A, A] と見えるのです。これを [A, A] 〜 [A, id_A, A] と書くわけです。

今定義した同値関係〜で射を束ねると、Sの構造が歪んでCに埋め込まれることはありません。念のために、プレ結合とポスト結合の両方の条件を揃えれば：

f〜g ⇔ (∀k∈S.(k;f = k;g) ∧ ∀s∈S.(f;s = g;s))

半圏でさえない一般的な状況では、この強い条件が必要かもしれません。

機能と行動により同定すること

「f〜g ⇔ (∀k∈S.(k;f = k;g) ∧ ∀s∈S.(f;s = g;s))」という定義は、Sが「判断に関与する他者達」の範囲を決めていて、Sの連中から見て違いが分からないなら、fとgは同じとみなしましょう、と言っています。

僕としては、このような「機能と行動だけによる同定」の方法が面白いなー、と感じたわけです。圏の場合は、射のイコールが先に与えられて話がはじまるので、しかも恒等も最初から備わっているので、∀k∈C.(k;f = k;g) と f = g の関係は自明なんですが、冒頭で書いたように、「なんか気分的には、あるいはスローガン的には意味があるような気がしなくもない」のです。

事情の説明と言い訳は、これでオシマイ。失礼いたしました。