圏の変種、包含部分圏

イイカゲンな型システムを求めて - 檜山正幸のキマイラ飼育記 (はてなBlog) に出てきた圏の変種に2通りの定式化を与えてみる。

1つ目は、イイカゲンな型システムを求めて - 檜山正幸のキマイラ飼育記 (はてなBlog)に書いてあることを素直にそのまま反映させた形。対象の集合Oに順序関係⊆が入っているとする。Mが射の集合だとして：

1. dom, cod:M→O
2. id:O→M
3. (;):M×M⊃→M （部分写像）

これは普通の圏と同じだが、普通の圏では：

• f;gが定義可能 ⇔ cod(f) = dom(g)

であるところを、次のように修正する。

• f;gが定義可能 ⇔ cod(f) ⊆ dom(g)

1. id(dom(f));f = f
2. f;id(cod(f)) = f
3. (f;g);h = f;(g;h)

などはそのまま成立する。

---

別な定式化としては、圏Cにまず包含部分圏を定義する。Cの部分圏が包含部分圏だとは：

1. Iは広大部分圏（すべてのid(a)がIに入る）
2. f∈I ならば、fはCのモノ射
3. Iはとてもやせた圏

包含部分圏Iを与えるとことと、|C|に順序構造を入れることは同じ。

圏Cの結合;以外に、;; と書かれる演算があって。

• f;;g が定義可能 ⇔ cod(f)→dom(g) となるi∈Iがある
• f;;g = f;i;g

であるとする。f;gが定義可能なら、当然に f;;g も定義可能だが逆は成立しない。

f;g と f;;g の2つの結合があったほうが普通の圏論の範囲で議論しやすいから、第2の定義のほうがいいかもしれない。包含部分圏を持つ圏の話は文献があるんじゃないのかな？ たーぶん。