TakuLabo

圏というのは非常に広い範囲で応用され、一般に何であるのかを簡潔に述べることは難しい。ということでまずは特殊な種類の圏の例を幾つか挙げ、それらがどういった用途で使用されるのかを紹介する。

亜群の中の対象を必要最低限のものだけを使って抽象的かつ詳細に調べることができるように亜群を強化することで得られる一つの形。

より具体的には、対象間の「同じである」という情報が既に組み込まれている「亜群」という構造の上から「不可逆な射をも含めた射のレイヤー」を適切に重ね合わせることで、「同じである」以外にも、どの対象群がどういった特別な意味を持つ空間群であるのかをラベル付けたり、数学的構造の一つとしてどういった特別な性質を持ち得るのかを明らかにしたりする。この時、新たに重ねたレイヤー上で定まる「対象が同じであること」と元々の亜群が持っている「対象が同じであること」は同じ意味でなければならない。)

そのレイヤーが重ねられる構造として使用している「亜群」の代わりに「集合 (ホモトピー0型)」を使ってはいけないのかと疑問に思うかもしれないが、許容自体はされているものの、その種類の圏は「Strict 圏」と呼ばれ、「数学的構造の対象を研究するためのフレームワーク」という用途には向かない。

実際、集合や群を始めとする数学的構造の対象を集めた空間というのは (ホモトピー型理論の土台の上では) どうしても「亜群」になってしまう。(数学的構造の対象全体の "集合" なんてものを一般に構成できない。)

この観点からは、圏というのは「数学的構造の対象を抽象的に取り扱うための便利な枠組み」という見方ができる。

集合 (点の集まり) 内の点同士の間に矢印を組み込んで得られる有向グラフの内、矢印同士の間の合成演算が矛盾なく定義されているもの。

この観点からは、圏は「群に似た数学的構造の一種」という見方ができる。

(..)

このノートでも Saunders Mac Lane の有名な圏論の教科書 (CWM: Categories for the Working Mathematician / 圏論の基礎) と同様、まずは圏を公理的に定義する。

(hom 集合を用いたより理想的な圏の定義は、ホモトピー型理論を基礎として導入した後にまた改めて説明する。)

ちなみに本来であれば、「対象」と「射」を分けて圏を定義する方が自然であるのだが、以下の点を考慮して敢えて single-sorted の公理化を採用することにする。

先ほど一階述語論理の言葉を用いた圏の公理化を書き下したが、少しわかりにくい可能性があるので補足しておく。

(ちなみにこの略記は今後も頻繁に使用していく)

つまりは $f$ を射としたとき、$f:X\to Y$ と書けるような $X,Y$ が一意的に定まるということと、$f:X\to Y$ であるとき、$X:X\to X$ かつ $Y:Y\to Y$ であるということを云っている。(またドメイン・コドメインとして割り当てられる射を、今後しばしば「対象 (object)」と呼ぶ。)

つまり、射 $f:X\to Y$, $g:Y\to Z$ が与えられたとき、それらは合成可能であり、その合成射は何らかの一意的な射 $(f\mathsf{⨟}g):X\to Z$ として割り当てられるということと、$f$ と $g$ の合成射 $(f\mathsf{⨟}g):A\to B$ が与えられるとき、$f,g$ はある射 $X$ があってそれぞれ $f:A\to X$, $g:X\to B$ とそれぞれ書かれるということを云っている。

つまり、射 $f:X\to Y$ が与えられたとき、$X\mathsf{⨟}f=f$ と $f\mathsf{⨟}Y=f$ が常に成り立つ。(この公理化の下では対象 $X$ は $X:X\to X$ を満たす自明な振舞いをする射として扱われるのだが、そのような射は従来の圏の定義の中では「恒等射 (identity arrow)」と呼ばれる射に該当する。実際「対象」と呼ぶより「恒等射」と呼んだ方がわかりやすくなる場面も多いので、今後対象を恒等射の意味合いで用いていることを明示したい時のために ${\mathrm{i}\mathrm{d}}_X:=X$ という記号を定義しておく。)

つまり、$(f\mathsf{⨟}g)\mathsf{⨟}h=f\mathsf{⨟}(g\mathsf{⨟}h)$ が常に成り立つ。(その一意的な射は $f\mathsf{⨟}g\mathsf{⨟}h$ と表記される。)

まず注意点を挙げておくと、「圏の公理を満たす理論 (以下に挙げるような圏の examples)」と「特定の公理を課した圏の一般論を行う舞台 (圏の公理系, トポスの公理系, ETCS 集合論の公理系)」とを混同しないように注意してほしい。
後者は「その公理系を満たす任意の理論に並行して行われる一般論を展開する枠組み」であり、前者は「圏の公理系を満たす理論の例」つまり「圏の一般論が適用可能な具体的な理論」である。

ETCS を公理化する際にも再度同じことを注意喚起すると思うが、ETCS は ZFC 同様あくまで「集合の公理系」であり、ETCS の場合は圏の "一種" であっても「具体的な一つの圏」を一般に定めない。つまり、例えば ETCS や ZFC のモデルを作ったときに、公理系に含めていない情報 (ETCS の場合: 具体圏か否か等、ZFC の場合: 連続体仮説が成立するか否かなど) が入り込む隙が残っている。(もちろんある圏を構成したとき、その圏が ETCS 公理系を満たしていれば、それは ETCS 公理系を満たす「具体的な一つの圏」ではある。よりわかりやすい例を挙げると、以下に挙げる「終圏」はトポスの公理を満たすことになるため「具体的な一つのトポス」である一方、「トポス」それ自体は圏の種類であって「具体的な一つの圏」を意味していない。)

以下の3つの公理からなる一階の理論は圏をなす。この圏は 空圏 (empty category) と呼ばれ、$\varnothing$ や $\mathbf{0}$ といった記号で表す。

Haskell を使ってこのデータ群が圏の公理を全て満たすかを確認すると以下のように True を返す

以下の4つの公理からなる一階の理論は圏をなす。この圏は 終圏 (terminal category / final category) や 自明な圏 (trivial category) などとと呼ばれ、$1$ または $\mathbf{1}$ などといった記号で表す。

というように公理化することもできる。

Haskell を使ってこのデータ群が圏の公理を全て満たすかを確認すると以下のように True を返す

以下の公理からなる一階の理論は圏をなす。(ここではその圏を $2$ とラベル付けることにする。)

以下の公理からなる一階の理論として、具体的な有限の有向グラフの形をした圏が得られる。この圏は 区間圏 (interval category) と呼ばれ、$\mathbb{2}$ または $(\cdot \to \cdot )$ などといった記号で表す。

(有限グラフからなる圏は技術的には全てのパターンに対する真偽を愚直に書き並べることで、圏である一階の理論として書き下すことができるが、射の総数が増えてくると非常に長くなってしまうため以降は省略し、圏の全体像となる有向グラフと合成の規則だけを示すだけにさせてもらう。)

Haskell を使ってこのデータ群が圏の公理を全て満たすかを確認すると以下のように True を返す

ちなみに射 $h$ を取り除いた場合、$f$ と $g$ の合成射を割り当てられないため圏を成さない。実際にそのようなデータ群を作って圏の公理を満たすかを確認すると以下のように False を返す

(ソースコードを見ればわかるように False となっている5番目の公理は「射 $f,g$ について、$f$ のコドメインと $g$ のドメインが共通であるとき、それらは合成可能であり、それらの合成射 $h$ は一意的に定まる」という公理である。)

実際にそれらの合成射を調べてみると以下のようになる

どのように矢印の合成を定義しているのかはソースコードを参照。
(ソースコードで行われている定義は「_ -> False」のおかげで一見短くみえるが、実際に一階の理論として公理を全て書き下そうとすると、その総数は 28800 個以上にもなる。)

Haskell を使ってこのデータ群が圏の公理を全て満たすかを確認すると以下のように True を返す

但しデータ数が多いため、量化子が多く使用されている結合性公理の総当たりによる確認には時間がかかる。
実際、上の結果を得るために 12分42秒 かかっている。