分断圏、離散圏とその利用
どうってことないようで使い途がある。
任意の圏Cに対して、Iso(C)は弱分断圏になる。End(C)を次のように定義すると強分断圏となる。
- |End(C)| = |C|
- End(C)(A, A) = C(A, A)
- A ≠ B ならば、End(C)(A, B) = 空集合
- 結合はCから引き継ぐ。
二重圏Dがあるとき、横方向に(水平圏に対して)End(D1h) を取る。homセット(endセット)は2-セルを持つので圏となる。よって、縦方向の垂直圏をインデキシング圏とするインデックス圏を作ることができる。
横方向に分断されるので、非対角(A≠Bな)ホムセットが全部削除(drop)されて対角成分(endセット)だけが残る。対象ごとに孤立した世界を考えて、相互変換には縦射(垂直圏)を使う構成法になる。
Iso(C)やEnd(C)よりさらに極端な構成がDisc(C)で、非恒等な射をすべて捨てる。
二重圏Dがあるとき、縦方向に(垂直圏に対して)Disc(D1v) を取る。このときも横方向に伸びるhomセットは2-セルを持つので圏となる。これは2-圏となる。二重圏から2-圏、双圏が出てくるメカニズムはこれが多いだろう。