美少女と学ぶ圏論(2)

本来ならば図式を交えて説明するべきところを図式を用意していないので非常に分かりにくいです(特に証明の部分など). 自分で可換図式を書きながら議論を追って読まれることをおすすめします.

1.2 SpecialなObjectたち

　レポートをやるというのは話を切り上げるための口実で, 実際ほとんどできていたので仕上げには全然時間がかかなかった.
　ゼミのために買ったホモロジー代数の本をパラパラめくっていると, 導来関手という文字が度々目に入った. そういえば, 千景に渡されたpdfには"関手と自然変換"というセクションがあった. 僕はカバンから紙の束を取り出して机にのせる.
　1.1は圏の定義と例で, 今日話したようなことが載っているだけだった. 1.2に進もう.

Definition 射\(f : A \to B \)に対し射\(g : B \to A \)が存在して\(f \circ g =1_B, g \circ f = 1_A\)を満たす時, \(f\)を同型射(isomorphism)という. またこのとき\(A,B\)は同型ともいう.

　同型はよく見る定義だ. 写像が全単射であることと写像が上の意味で同型であることは同値だから, 上の定義は理解しやすくて良い.
　ただ, 全単射の定義とは違ってdomainやcodomainの元がどうなるかについては触れていない. これが千景の言っていた"元の取れない圏論"なのだろうか. 確かに元に触れずに同型射を定義しているので, なんとなく抽象的な感じはする.

Definition 射\(f : A \to B \)がepimorphism(epi)であるとは, 任意の\(g \circ f = h \circ f \)を満たす射\(g,h : B \to C \)に対して\(g = h\)が成り立つ.
　このとき\(f : A \twoheadrightarrow B \)とかく.
Definition 射\(f : A \to B \)がmonomorphism(mono, monic)であるとは, 任意の\(f \circ g = f \circ h \)を満たす射\(g,h : C \to A \)に対して\(g = h\)が成り立つ.
　このとき\(f : A \rightarrowtail B \)とかく.

　epimorphismとmonomorphismはどうやら逆の概念であるらしい. そう, よく見れば上の定義にある\(f,g,h\)の射の"向きを反転"させれば下の定義に一致する. これが千景の言っていた双対に違いない.
　ネットによると, それぞれの射にはエピ射, モノ射という訳が当てられるらしい.　千景は, 双対には"余"という漢字が当てられると言っていたが必ずしもそういうわけでもないのか.

　ところでepiやmonoが何を表しているかをもうちょっとよく考えよう.
　分かりやすいところで写像, つまりSet圏を考えることにする. \(f\)がepiなら, \(g(f(x)) = h(f(x)) \;\; (\forall x \in A)\)のとき\(g = h\)が言える. \(g,h\)が\(Im f\)上で一致するなら\(B\)上全体で一致するということで, これが成り立つということは\(f\)が全射ということに違いない.
　同じく, \(f\)がmonoなら, \(f(g(x)) = f(h(x)) \;\; (x \in C)\)のとき\(g = h\)だから\(f\)は単射になる.
　なるほど, どうやらepiとmonoは全射, 単射に対応するらしい.

　僕は手を止めて紅茶を一口飲んだ. ハーブティーは心を落ち着けてくれる. 温かい紅茶が心に染み入るように, epiとmonoの定義は僕の脳内に染みこんでくるようだ.
　ここに千景がいたら, きっとこんな風に語りかけてくるだろう.
『さぁ, 次はisoについても考えてみよう. 集合では全射かつ単射と同型は同値. ではepiかつmonoとisoは同値？』
　そんな僕の考えを予想しているかのように, 次のページには千景が書いたと思われる走り書きがしてあった.

　isoならばmonoかつepi. しかし逆は成り立たない. 反例は？

　isoならばmonoかつepiは定義から明らかだ. さて, 反例は….

---

「それで？ 反例は見つかったの？」
　午後. 僕はまた, 千景と教室の黒板前にいた. 学部生控室というのは便利なもので, 自由に使える黒板や椅子や机がある. こんなに素晴らしい環境の割には人も少ない.
　僕は昨日考えたことを千景に話すことにした. 人に説明すると, 頭の中も整理される.
「意外なところにあったよ. 群とか加群じゃ見つからなかった」

Counterexample \(X\)を2点以上の位相空間とする. さらに\(X_i\)は\(X\)に密着位相を入れたもの, \(X_d\)は\(X\)に離散位相を入れたものとする.
　集合として恒等写像である連続写像\(id : X_d \to X_i; \; x \mapsto x \)は全単射で, 位相空間の圏の射としてepiかつmono. しかしこの逆写像は連続でないから, 位相空間の圏の射にはならない. よって\(id\)は位相空間の圏の中でepiかつmonoだがisoではない.

「よく出来ました. 言ってなかったけど, isoとepiかつmonoが同値になる圏をbalancedという」
「ふむ？」
「一般にAbel圏はbalancedなんだ. だからAbel群や加群では同値になるよ」
「うん, それに気がついてから, 位相空間の圏で探してみたら見つかった」
「他に何か気がついたことはある？」
「そうだな…. posetを圏とみなす, というのをやったよね. この圏では全ての射はepiかつmonoで, isoな対象は等しいことが反対称律から分かる, とか」
「そうだね. それもepiかつmonoだがisoでないような例の一つね」
「あまり面白い反例とは言えないかもしれないけどね」
　千景は満足そうにニヤついて, 僕を見た.
「さて, 先に進もう. 1.2くらいは読んできた？」
「う, うん. でも, 関手と自然変換まではたどり着かなかったよ」
「いや, 別にいいよ. 昨日のアレは言ってみただけ」
　千景は僕にチョークを渡して, 一番前の席についた. 先生ではなく生徒として聞き手に回る, という意思表示. 渡されたチョークはほとんど使ってなくて, 先がほんの少しだけ欠けていた.
「1.2の残りでは圏の特別な対象を定義して, それらの例を見るって感じだね. まずはproduct」

Definition

\(A \xleftarrow{p_A} P \xrightarrow{p_B} B \)が直積(積, product)の図式である, または対象\(P\)がproductであるとは, 以下を満たすことである.

• (UMP) 任意の\(A \xleftarrow{f} Z \xrightarrow{g} B\)なる図式に対し, \(p_A \circ h = f\)かつ\(p_B \circ h = g\)を満たす\(h : Z \to P \)が一意的に存在する. \(f,g\)から定まる射\(h\)のことを, \(h = \langle f,g \rangle\)と書く.

「ここでいう"一意的に存在する"というのは, 存在して, かつ一意的であるってことね. 条件として2つあるってことに注意してね」
「オッケー. じゃあ双対のcoproductも一緒に定義を述べるよ」

Definition

\(A \xrightarrow{i_A} Q \xleftarrow{i_B} B \)が直和(余積, coproduct)の図式である, または対象\(Q\)がcoproductであるとは, 以下を満たすことである.

• (UMP) 任意の\(A \xrightarrow{f} Z \xleftarrow{g} B\)なる図式に対し, \(h \circ i_A = f\)かつ\(h \circ i_B = g\)を満たす\(h : Q \to Z \)が一意的に存在する.

「定義はこれだけなんだけど……UMPってなんのことかな？この条件の名前？」
「うん, UMPの説明は特にしてなかったね. UMPはUniversal Mapping Propertyの略で, 簡単に言えば"ある射が一意的に存在する"っていう性質のこと」
「〜の条件を満たす\(h\)が一意的に存在する, って条件のことだね」
「そう. universalityと言ったりもする. productのuniversalityと言えば, 上の条件のことだと思って」
「了解. じゃあもう少し例を続けるよ」

Definition

対象\(0\)が始対象(initial object)とは, 以下を満たすことである.

• (UMP) 任意の対象\(X\)に対して\(0 \to X \)なる射が一意的に存在する

対象\(1\)が終対象(terminal object)とは, 以下を満たすことである.

• (UMP) 任意の対象\(X\)に対して\(X \to 1 \)なる射が一意的に存在する

「例は挙げられる？」
「うん」
　昨日ノートにまとめたことを, 黒板に書いていく.

圏	initial object	terminal object	product	coproduct
\(\mathbf{Set}\)	空集合 \(\emptyset\)	1点集合\(\{* \}\)	直積	直和(disjoint union)
\(\mathbf{Top}\)	\((\emptyset, \{\emptyset\})\)	\((\{* \}, \{\emptyset, \{* \}\})\)	直積空間	直和
\(\mathrm{R}-\mathbf{Mod}\)	1点加群 \(\{0\}\)	1点群 \(\{0\}\)	直積	直和(=直積)
poset \(P\)	\(P\)の最小元	\(P\)の最大元	sup(最小上界)	inf(最大下界)

「注意としては, 一般に加群の直積と直和は一致しないけど, 今定義した直積と直和が有限(二項)直積/直和しか定義していないからだね. そういえば, 今の定義じゃ二項直積/直和しかないけど, 一般の直積や直和も定義できるのかな…？」
「もちろん. 一般の集合\(I\)上の直積も定義できるよ」

Definition

\(P \xrightarrow{p_i} X_i \; (i \in I)\)または\(P\)が直積とは, 以下の満たすことである.

• (UMP) 任意の\(Z \xrightarrow{f_i} X_i\)なる図式に対し, \(p_i \circ h = f_i \;\; (i \in I)\)を満たす\(h : Z \to P \)が一意的に存在する.

「表をみていて気がついたことはある？」
「terminal objectとinitial objectが一致する圏があるね. 加群の圏とか, Abel群の圏がそうだね」
「terminal objectとinitial objectが一致する時, それをzero objectという. Abel圏にはzero objectをもつことが要請される」
「確か…加群の圏とかAbel群の圏がAbel圏だったね」
「あとはベクトル空間の圏もね」
「他には, posetではterminal objectが最大元でproductがsupになるんだね」
「posetは例として分かりやすくていいよね. うん, 私も好きだよ」
「じゃあ次に進むよ…って言っても, 次はあんまりピッタリ来る例がないんだけど」
「equalizerとpullbackね. こちらは定義だけやろう, とりあえず後で出てくるまで覚えておいてくれればいいよ」

Definition

平行射\(f,g : A \rightrightarrows B \)に対し, \(e : E \to A \)が\(f,g\)のequalizerであるとは, 以下を満たすことである.

• (図式の可換性) \(f \circ e = g \circ e \).
  
• (UMP) 任意の\(z : Z \to A \)で\(f \circ z = g \circ z \)を満たすものに対し, \(z = e \circ h \)を満たす\(h : Z \to E \)が一意的に存在する.

Definition

\(A \xleftarrow{q_A} P \xrightarrow{q_B} B \)が図式\(A \xrightarrow{p_A} C \xleftarrow{p_B} B \)のpullbackとは, 以下を満たすことである.

• (図式の可換性) \(p_A \circ q_A = p_B \circ q_B \).
  
• (UMP) 任意の\(z_A : Z \to A, z_B: Z \to B \)で\(p_A \circ z_A = p_B \circ z_B\)を満たすものに対し, \(q_A \circ h = f, q_B \circ h = g\)を満たす\(h : Z \to P \)が一意的に存在する.

「coequalizer, pushoutがequalizer, pullbackの双対概念として定義されるよ」
「これらの概念に関していくつか性質を確認しておこう」
「うん」
「じゃあ, 次のことを証明して」

Prop terminal object, initial object, product, coproduct, equalizer, coequalizer, pullback, pushoutは同型を除いて一意的である

「同型を除いて一意的」
「つまり, 2つあったとすると同型になるってことね. 同型を同一視すると存在は一意的ということ. もちろん一般の圏がこれらを持つとは限らないけどね」
「とりあえずterminal objectの一意性をやろうか」

証明 \(1, 1'\)をterminal objectとする. \(1\)のterminal objectのUMPから, \(p': 1' \to 1 \)なる存在する. 同様にして\(p : 1 \to 1'\)も存在する.
　\(p,p'\)が同型, すなわち\(p \circ p' = id_{1'}, p' \circ p = id_{1}\)を示せば\(1 \cong 1'\)であることが分かる.

　\(p \circ p', id_{1'}\)はともに\(1' \to 1' \)なる射であるが, \(1'\)のterminal objectのUMPより\(1'\)に向かう射は一意的である. 即ち\(p\circ p', id_{1'}\)は一致するので\(p \circ p' = id_{1'}\)が分かる. 同様にして\(p' \circ p = id_1\)もわかるので, \(1 \cong 1'\)が示された. (QED)

「これでいいかな？ UMPは存在+一意性という2つの条件のことだから, それを上手く使ったよ. 射を作るのに存在を, 射が等しいことを示すのに一意性を使う感じだね」
「うん, オッケー. あとについては大体同じ感じでできるからやっておいて」
「う, うん」
　大体同じ感じ……っていうのはさすがにどうだろう. あとでちゃんとチェックしないと.
「この命題はどうかな？」

Prop \(A \times (B \times C) \cong (A \times B) \times C \)

「直積の結合律だね. 証明は, すぐには思いつかなさそうだなぁ」
「じゃあ, これは私が示そうか. 証明は先と似たような感じでできるよ. ポイントは, UMPを使って射を構成するところと, 一意性から射が等しいことを導くところかな.」

証明 \(A \times (B \times C) \to (A \times B) \times C \)を構成する. \(p^{A \times B}_A : A \times B \to A \)を射影(直積に付随する射)とする.
　\(p^{A \times (B \times C)}_A : A \times (B \times C) \to A \), \(p^{B \times C}_B \circ p^{A \times (B \times C)}_{B \times C} : A \times (B \times C) \to B \)に対し, \(\langle p_A, p_B \circ p_{B \times C} \rangle : A \times (B \times C) \to A \times B \)なる射がある. また, \(p^{B \times C}_C \circ p^{A \times (B \times C)}_{B \times C} : A \times (B \times C) \to C \)と合わせて, \(h_1 = \langle \langle p_A, p_B \circ p_{B \times C} \rangle, p_C \circ p_{B \times C} \rangle : A \times (B \times C) \to (A \times B) \times C \)なる射を得る.

　逆向きの射を作ろう. 上と同じ議論により, \(h_2 = \langle p_A \circ p_{A\times B}, \langle p_B \circ p_{A \times B}, p_C \rangle \rangle : (A \times B) \times C \to A \times (B \times C)\)を得る.

　射が構成できたので, あとはこれらが同型を与えることを見ればよい. すなわち, \(h_1 \circ h_2 = 1, h_2 \circ h_1 = 1\)を示す.

　\(h_2 \circ h_1, 1\)がともに\(f\)に対して\(p_A \circ f = p_A, \; p_{B \times C} \circ f = p_{B \times C}\)という関係式を満たすことを言えば, \((A \times B) \times C　\)の直積のUMPを図式\(A\times B \leftarrow (A \times B) \times C \rightarrow C \)に対して使うことで, 射の一意性より\(\langle p_{A\times B}, p_C \rangle = h_2 \circ h_1 = 1\)が分かる.
　\(p_A \circ 1 = p_A, \; p_{B \times C} \circ 1 = p_{B \times C}\)はよいから, \(p_A \circ (h_2 \circ h_1) = p_A, \; p_{B \times C} \circ (h_2 \circ h_1) = p_{B \times C}\)を示す.

\[ \begin{eqnarray} p_A \circ (h_2 \circ h_1) &=& p_A \circ \langle p_A \circ p_{A\times B}, \langle p_B \circ p_{A \times B}, p_C \rangle \rangle \circ h_1 \\ &=& p_A \circ p_{A \times B} \circ h_1 \\ &=& p_A \circ p_{A \times B} \circ \langle \langle p_A, p_B \circ p_{B \times C} \rangle, p_C \circ p_{B \times C} \rangle \\ &=& p_A \circ \langle p_A, p_B \circ p_{B \times C} \rangle \\ &=& p_A \end{eqnarray} \]

　同様にして\(p_{B \times C} \circ (h_2 \circ h_1) = p_{B \times C}\)および\(h_2 \circ h_1 = 1\)も分かる. よって\(A \times (B \times C) \cong (A \times B) \times C \)である. (QED)

「最後は一気にはしょったね」
「ただのdiagram chaseだからね, 自分で手を動かして確かめるしかないよ」
「まぁそれもそうかもね. しかし, 集合の時は元の対応を見るだけで明らかだったのに, 圏だと大変だなぁ……」
「直積が図式を使って間接的にしか定義されないからだね. 基本的にdiagram chaseは大変面倒くさい. でも圏論はなんでもかんでもエレガントにできるわけじゃない. 泥臭いことも勉強の一つ」
「自分で一度証明を追ってみるよ」
「それがいい. ついでにもう一つ宿題を出しておこう」

Prop(宿題)

\[ \begin{array}{c} \bullet & \rightarrow & \bullet & \rightarrow & \bullet \\ \downarrow & (a) & \downarrow & (b) & \downarrow \\ \bullet & \rightarrow & \bullet & \rightarrow & \bullet \\ \end{array} \]

という図式に対して, 以下を示せ.

• 1. 左右の四角(a),(b)がpullbackのとき, 全体もpullback
     
• 2. 右の四角(b)と全体がpullbackのとき, 左の四角(a)もpullback

「さてとりあえずこれでspecial objectの話は終わり」
「special object？」
「うん. ここでやった概念は覚えておくといいよ. あとでまた出てくるから」
「なるほどね」
　千景はそう言って, 椅子から立ち上がった. ゆっくりとした足取りで黒板の前に立つ. ぼうっとしている僕からチョークをひったくって黒板に向かった.
「私たちは圏とその上のspecial objectを定義した. まだ話していなかったけど, 関手は圏から圏への変換のことね」
「関手と自然変換って概念があるって言ってたね. 自然変換は？」
「自然変換は関手から関手への変換」
「変換ばっかりだね」
「圏論ではこうやって, 色んな物が抽象的に定義されていく. 関手や自然変換がどの意味で"抽象的"なのかはまだ言わないけど, とにかく圏, 関手, 自然変換と進むに連れて, 視点はどんどん広くなるの」
　千景は黒板に不思議な絵を書いた. 一番右下に圏, その上に矢印を引っ張って関手, さらにその上に矢印を引っ張って自然変換と記した.
「けれど, 視点の広さは変えないで, 色んな物をより深く, より精密に見ることもできる」
「どういう意味？」
「例えばspecial objectね. 抽象度は上げないままで, 圏の上で条件をつけたりしながら特別な概念を追求する」
　圏と書かれたところから左に矢印を引っ張って, "special object"と書いた. さらに千景はその下に, "終対象, 直積, equalizer, pullbackなど"と付け足した.
「左に向かうのは理論の緻密さ, 上に向かうのは理論の高さ. 緻密な理論ほど細かい条件に対応できるし, 高い理論ほど抽象的に話が進む」
「ふむ」
　一体彼女は何がいいたいのだろう. いや楽しそうなのはすごく伝わってくるんだけどね.
「じゃあ, 関手くらいの高さで, special objectくらいの緻密さのある概念は何？」
「は？」
「言葉を変えようか. special objectを関手の言葉を使って一般化できるかな. あるいは, 関手の言葉を使ってspecial objectに対応するものは作れるかな」
「えっと, 何を言ってるのかさっぱりわからないんだけど」
「結論から言おう, それにはちゃんと名前がついてる. その説明をする前に……」
　千景はチラッと僕を見た.
「関手と自然変換の定義をしてしまおう. これでようやく, 圏のまともな絵がかける」
「うーん」
　日本語でお願いします. って言いたかったけど, 千景の楽しそうな話に水を差したくなかったので黙っていた.
　攻守交代, 僕は一番前の席に腰掛けて, 千景の話に耳を傾けた. 日暮れ前の空は紫色でなんとも得体の知れない色をしていたけれど, 僕にはそんな空もいつもと同じく綺麗に見えた.

補足

千景が出した"宿題"は, two pullbacks lemmaと呼ばれます. 証明は https://proofwiki.org/wiki/Pullback_Lemma などを参照してください.

美少女と学ぶ圏論

ここまで書いて飽きました.

1章 圏とその構造

1.1 圏の定義と千景の講義

「4月からのゼミはもう決めた？」
「うん. とりあえず,クラスの子とホモロジー代数ゼミをやろうと思ってるよ. 春休みのうちに予習を進めないと」
「ふぅん,ホモロジー代数ね」
　千景は読んでいた本をパタンと閉じて, 勢い良く立ち上がったと思ったら大きく伸びをして, つかつかと足を引っ掛けるようにして黒板の前まで歩き, そのあと立ち止まってからくるりと振り返ってこちらを見た.
「homologyはいいね. 複雑な空間から単純だけど重要な情報を抜き出せる. 複雑に絡み合った網の中の, 本当に大切なものを拾い上げるようにして情報が得られる. homologyはとてもいいよね」
「千景はホモロジー代数もやってるの？」
「必要な時に扱うだけね. Abelian categoryはそんなに詳しくないし」
「あーべりあんかてごりー？」
「そうか, 君はcategory theoryはやってないんだっけ？」
「カテゴリー…あーうん, 圏論か. 聞いたことはあるよ. 触れたことはないけどね. 元がとれないとかなんとか…」
　千景はスッとこちらを見て, ふらふらとした足取りでこちらへやってきた. そして顔を覗きこんでくる.
「圏というのは群とか体と同じような構造の名前. でも, 君のよく知っている構造とは少し違うかな. 圏は群や体よりもう少し広域的な視点なの. 言ってみれば, "群"そのものじゃなく, "群全体の構造"みたいな」
「どういう意味？」
　千景はまた黒板の方に向き直る. 今度はキビキビとした動作で黒板の前を陣取って, チョークを手に持った.
　背が高いとはお世辞にも言えない体では, 一番上から文字を書くのはつらそうだ. けれどそのことを言うと彼女はへそを曲げてしまう. 夕焼けが黒板の左半分を紅く照らしていた. 日暮れ時の風が窓から吹き込んで, カーテンと千景のサラサラした長い髪を巻き上げて逃げていった.
「例えばだけど, 圏の例はそれこそ山ほどあるの. そのうちの一つが群の圏. 圏それ自体は言ってみれば無味乾燥なんだけど, 細かい条件をつけると色々なことができるようになる」
「例えば？」
「Abel群の直積と直和は一致する. Abel圏の直積と直和も一致する」
「Abel圏はAbel群の一般化ということ？」
「そうね. Abel圏はAbel群や, R加群の圏の一般化. ホモロジー代数が展開できるような圏ってこと. だから重要」
「なるほど」
「圏論それ自体が, 他の分野とつながっていることはよくあるの. 今言ったみたいに, Abel圏上ではホモロジー代数ができる. 同じようにホモトピー論ができる圏や, コホモロジー論ができる圏なんかもあるね」
「全然想像つかないや」
「応用例なら計算機科学分野にもよく見られるかな」
「計算機科学？」
「computer scienceね. さっき君が言ったように, 圏論は"元がとれない"と言われる. それは相手にするものが集合とは限らないからなの. 集合とは限らないものに対して議論をするから, 集合論を前提にしていない分野に応用されることもある」
「それが計算機科学ってこと？」
「もちろん他にもあるけどね」
　教室はしんと静まり返っていて, まるでたくさんの人たちが彼女の話に耳を傾けているような気になった.
「あるいはもっと純粋な圏論もある. 圏論それ自体を研究する分野. 極限まで抽象化を重ねたその先にあるのはなんだろう, とかね」
「そこに何かがあるわけ？」
「どうかな. でも, 広大な圏論がたった一つの概念で全て説明できたら面白いと思わない？」
「…そんなに上手くいくかなぁ」
「上手くいかない理由があるわけじゃないでしょ. あと最近の流れでは, 圏論をベースに数学を置き換えるなんてことをしている人もいるみたい. ある圏の上で集合を模倣する, 集合論ができる圏みたいなものがあって, それを使うと集合論ベースだった数学は全部圏の言葉で書き直せるんじゃないかってね」
「数学を置き換える？それって大変じゃないの？」
「まぁそりゃあそうでしょうね. でも圏論の言葉で書くから分かることもあるよ. 本質的なことが何かってことが見えやすかったり, 抽象的な議論で済ませることができたりね」
「なるほどね」
「話を戻そうか. 圏というのは, 例えば群と群準同型, みたいなものの集まりね. 点と矢印の集まりみたいな感じ」
　千景が点をたくさん打ってから, 点と点の間にめちゃくちゃに矢印を書いた.
「つまり, 群が点で, 矢印一つ一つが群準同型になるような圏があるわけだね」
「そうね. それは圏の例の一つ. でも圏の例は他にももっとたくさんあるよ. 定義を書こうか」
　千景はすらすらと, 黒板に定義を書いた.

Definition \(\mathcal{C}\)が圏とは, 対象, 射, dom, codom, 合成の組からなるものであって, 以下を満たすもののことである.

• (dom, codom) dom, codomは射から対象への対応とする. 射\(f\)であって, \(\mathrm{dom}(f)=A, \mathrm{codom}(f)=B\)であるようなものを\(f : A \to B \)と表記する.
  
• (合成の存在) 任意の射\(f,g\)に対し, \(\mathrm{dom}(f) = \mathrm{codom}(g)\)を満たすならば, 射\(f \circ g : \mathrm{dom}(g) \to \mathrm{codom}(f)\)が定義される.
  
• (identityの存在) 任意の対象\(X\)に対し, 射\(1_X : X \to X \)が存在する. これをidentity arrowとよぶ.
  
• (identity laws) 任意の射\(f : A \to B \)に対し, \(f \circ 1_A = f = 1_B \circ f \).
  
• (associativity law) 合成が定義できるような射\(f,g,h\)に対し, \(f \circ (g \circ h) = (f \circ g) \circ h \).

Definition \(\mathrm{Hom}_\mathcal{C}(A,B) = \{f : A \to B; f \text{は} \mathcal{C} \text{の射} \}\) (\(f : A \to B \)の形の射全体をHomで表す.)

「始めの3つはあとの公理を成り立たせるために必要な条件を述べているだけね. 公理として機能するのは最後の2つ」
「identity lawとassociativity law…モノイドみたいだね」
「monoidは底集合に対して単位元が1つ存在. 圏は全ての対象に対して恒等射が存在」
「ならモノイドとはかなり違うかぁ. モノイドは圏じゃないんだね…」
「待ちなさい」
　千景はキリッとした顔をこちらに向ける. 大きな目の奥が一瞬, キラリと光ったように見えた.
「圏になるかどうかはどういう対象とどういう射を考えるかに依る. 圏の例をいくつか見て, 圏という構造に慣れましょう」

Example

• \(\mathbf{Set}\): 対象を集合, 射を集合から集合への写像とする圏. dom, codは写像のdomain, codomainとし, 合成は写像の合成, 恒等射は恒等写像と考える.

「これはいいわね？」
「えっと, 任意の集合が対象になるんだね. 恒等写像に対してなら恒等射律も言えるし, 写像の合成に関して結合律も言えるね. いいよ」

• \(\mathbf{Group} \; (\mathbf{Mon}, \mathbf{Ring}, \mathbf{Vec}_\mathbb{C}, \mathbf{Ab}) \): 対象を群(resp. モノイド, 環, \(\mathbb{C}\)上のベクトル空間, アーベル群), 射を準同型とする圏.
  
• \(\mathbf{Top}\): 対象を位相空間, 射を連続写像全体とする圏.

「これもいい？」
「群の圏…さっき言ってたやつのことだね. モノイドとか環とかも確かに圏になるね」

• poset \(P\): \(P\)を半順序集合(partially ordered set)とする. 対象は\(P\)の元, 射は\(a \leq b \iff a \to b \)によって, "順序関係があること"によって定める.

「じゃあ, これはどう？」
「えーっと, 確認だけど, 半順序っていうのは反射律と推移律と反対称律が成り立つ順序だよね？」
「そう. 全順序じゃないことがポイントね. 任意の2元は大小関係が"ある"or"ない"のどちらかだから, 前者は射がある, 後者は射がないとみなすってこと」
「ふむ」
「\(a,b \in P \)に対し, \(a \leq b \)なら\(\mathrm{Hom}(a,b)\)は1点集合. そうでなければ空集合」
「なるほど, なんとなくわかった気がする」
「このように, Homがたかだか1点しかない圏を痩せた(thin)圏と言う. 射が少ないから痩せてるんだね」

• group \(G\): \(G\)を群とする. 対象は\(G\)のみ, 射は\(g \in G \)に対し\(G \to G; x \mapsto x \star g \)全体を考える.

「さて, これはどうかな」
「対象は$G\(1つしかないんだね」 「そう. その代わり, 射が\)G\(の元の数だけある. \)G$の単位元から定まる射が恒等射になる」
「なるほど」
「これと同じ理屈で, モノイドも圏になるよ」
「"単位元がある"から恒等射が作れるって話か」
「こんなのもある」

• 双対圏 \(\mathcal{C}^{op}\): \(\mathcal{C}\)を圏とする. 対象は\(\mathcal{C}\)と同じ, 射は\(\mathcal{C}\)の射を向きだけ反転させて得られる圏\(\mathcal{C}^{op}\)を双対圏という.

「射の向きだけ反転？」
「そう. 圏を点と矢印で書くと, その矢印の向きをひっくり返したものが双対圏. 他の分野の"双対"って言葉はここから来ている. 双対には"余"という漢字を当てることもあるよ」
「僕が知っているのはベクトル空間の双対空間くらいかな. そういえば, 多様体の接空間と余接空間は, 双対空間だけど"余"という漢字を当ててるね」
「そうね. とりあえずこのくらい分かってもらえればいいかな」
「よく出てくる圏はこれくらいなの？」
「いや, そんなことないよ. もっと面白い圏に触れるためには色々準備が必要だから」
　千景はニコニコしながら, こちらを見ている.
「圏の例を挙げたけど, これだけじゃあ何もわからないでしょうね」
「そうだね. 圏になることは分かるんだけど, これをどうやって使うのかは全然イメージが沸かないな」
「例えば」
　千景がチョークを持った手でこっちを指さす.
「いくつかの圏では共通することがあるね. 例えばだけど…集合, 加群, 環, 位相空間. これらには全て"直和"が定義される」
「集合の直和っていうのは, 添字をつけてdisjoint unionを取るんだっけ. 加群の直和は形式的な有限和に加群の構造を入れたもので, 環はテンソル積で, 位相空間は集合として直和を取って位相をいれるんだね」
「そう. でもこれらはあまり似ているとは思えないのに, "直和"と名前が付いているのはどうしてかな」
「うーん…気にはなってたけど, 理由は知らないなぁ」
「実は, 一般の圏に"直和"(coproduct)という概念が定義できて, 集合の圏や加群の圏だと今君が言った直和と一致するからなんだ」
「え？本当に？」
「そう. 他にもこうやって一般の圏で考えることで見えてくるものはあるよ. 一般化によって高い視点で物事を捉えられる. 異なる構造に共通する部分を見つけたり, より本質的なことを考えたり」
「なるほどねえ」
「どう, 少しは興味が沸いてきた？」
　千景がキラキラした目でこちらを見つめてきた. こういうときの彼女はすごく楽しそうで, 僕としてもそんな彼女を見ているのはとても好きなんだけど, 残念ながらもう帰る時間だ.
　すでに日は暮れて, あたりは暗くなっていた.
「どうだろうね. それより, 帰ってレポート仕上げなくちゃ」
「えー」
「そんな顔しないでよ」
「んー. じゃあ今日のところは勘弁してあげよう. その代わり, 来週までにこれの関手と自然変換のセクションまで読んできて」
　そう言って, 千景はカバンからホッチキス留めされた紙の束を取り出した.
「なにこれ…何かのpdf？」
「まぁそんなところ. それじゃあ, よろしく！」
　千景は長い髪をひらひらさせながら, 教室を飛び出していった.
　僕は黒板を綺麗に消してから, 教室を後にした.

参考

千景が言っている"色々な"圏論については以下のキーワードなどを参照してみてください.

• ホモロジー代数: Abel圏, 導来圏
• ホモトピー論: model圏, Categorical Homotopy Theory
• コホモロジー論: Sheaf, Site, Grothendieck Topology
• 計算機科学: Homotopy Type Theory, Algebra(Monad, Comonad, F-Algebra, T-Algebra, DiAlgebra)
• 純粋な圏論: Kan Extension, Higher Category
• 集合論: Topos Theory, Higher Topos Theory(HTT)

objective覚書

objective-0.6.1

O' = data Object e m
= forall x. e x -> m (x, Object e m)
= hom(e, m . (-,O'))   (as Nat)

functor Kを用いてe = hom(a,K-) = forall x. a -> K xと書けるとき(Data.Functor.Kan.Ranを見よ)

O' = hom(hom(a,K-), m . (-,O'))
= hom(K^-1(hom(a,-)), m . (-,O'))
  -- by K^-1 -| Ran K
= hom(hom(a,-), Ran K (m . (-,O')))
  -- covariant yoneda
= Ran K (m . (-,O')) a
= forall r. (a -> K r) -> m (r,O')

Object e mがわかっているとき, eと適当な型の直積をとっても良い:

O' = data Object (forall x. (a,e x)) m
= hom((a×-) . e, m . (-,O'))
= hom(e , hom(a,-) . m . (-,O'))
= data Object e (forall x. a -> m x)

eとして Request a b r = (a,b->r) を取ったものはProcessとして定義されている.

P' = data Process a b m
= Object (Request a b) m
= hom((a×-) . hom(b,-), m . (-,P'))
= hom(hom(b,-), hom(a,-) . m . (-,P'))
= a -> m (b, P')

左Kan拡張を使ってもいいけれど同値な式以上の意味はなさそう.
Lanがより単純な項に書き換えられるなら何かあるのかも？

O' = data Object e m = Hom(Lan (-,O') e, m)