Steve Awodey の Category Theory を読む : Chapter 3

Steve Awodey の Category Theory を読む シリーズトップ

3.2 Coproducts

Example 3.5

を の UMP より を満たすただ一つの arrow とする。同様に を定める。このとき、 が 、 の coproduct となることを示す。
任意の と任意の に対して、 と を考えると、 の UMP より が存在する。すると の UMP より が存在して、 を満たす。この に対して、

\begin{align*}
\left| [f,g] \circ i_{M(A)} \right| \circ \eta_{A} &= \left| [f,g] \right| \circ \left| i_{M(A)} \right| \circ \eta_{A} \\
&= \left| [f,g] \right| \circ \eta_{A+B} \circ i_{A} \\
&= [\left| f \right| \circ \eta_{A}, \left| g \right| \circ \eta_{B}] \circ i_{A} \\
&= \left| f \right| \circ \eta_{A}
\end{align*}

が成り立つので、 の UMP より が成り立つ。同様に が成り立つので、 は diagram を可換にする。
次に、任意の が diagram を可換にするとする。すると

\begin{align*}
\left| h \right| \circ \eta_{A+B} \circ i_{A} &= \left| h \right| \circ \left| i_{M(A)} \right| \circ \eta_{A} \\
&= \left| h \circ i_{M(A)} \right| \circ \eta_{A} \\
&= \left| f \right| \circ \eta_{A}
\end{align*}

が成り立つ。同様に が成り立つので、 の UMP より、 である。よって の UMP より が成り立つので、 は 、 の coproduct である。

free monoid の UMP や、coproduct の UMP を適宜使用する必要があってちゃんと証明しようとすると複雑ですね。coproduct の UMP を証明するために、diagram を可換にする arrow が存在することと、それがただ一つに決まることの2つを証明していることを確認してください。

Example 3.6

一般に 、 が位相空間のとき、 の位相は で定義されます。

任意の と任意の に対して、 を Example 3.4 と同様に定義すると、可換性と唯一性は Example 3.4 で証明済みなので が continuous であることを示せばよい。
任意の に対して、 であるが、、 が continuous であることより、、 が成り立つ。 の定義より となるから、 は continuous である。

Example 3.9

この Example の証明は非形式的な証明でさらっと流されていますが、形式的に証明しようとすると結構大変です。
書籍では、binary relation は4つの等式を含んだ最小の equivalence relation であるとだけ書かれていますが、具体的にどのように構成するのか書かれていません。4つの等式を 上の二項関係と表現したときに生成される最小の equivalence relation の構成については下の記事に書いたのでそちらを参照してください。
www.orecoli.com

、 が homomorphism となることは明らかなので省略します。 と が において一致して、かつ の単位元になる必要があるので、4つの等式の上の二つを含む equivalence relation で割る必要があるということを確認してください。
ここでは、書籍にあるように で定義される が well-defined であることを証明します。

\begin{equation}
\forall [v], [w] \in M(\left| A \right| + \left| B \right|)\, / \sim,\, [v] = [w] \Rightarrow [f,g]([v]) = [f,g]([w])
\end{equation}

4つの等式を表現する 上の二項関係を とする。
先に参照した記事の内容より、 が成り立つ。よって が存在して、、 かつ が成り立つ。 に関する帰納法により示す。

• のとき

の場合は明らか。 のとき、 を 上の任意の word とすると、 の場合を考える。このとき、

\begin{align*}
[f,g]'(su_{A}s') &= [f,g]'(s) \cdot f(u_{A}) \cdot [f,g]'(s') \\
&= [f,g]'(s) \cdot u_{M} \cdot [f,g]'(s') \\
&= [f,g]'(s) \cdot [f,g]'(s') \\
&= [f,g]'(ss')
\end{align*}

が成り立つので、 が成り立つ。 の場合も同様である。
のとき、

\begin{align*}
[f,g]'(saa's') &= [f,g]'(s) \cdot f(a) \cdot f(a') \cdot [f,g]'(s') \\
&= [f,g]'(s) \cdot f(a \cdot_{A} a') \cdot [f,g]'(s') \\
&= [f,g]'(s) \cdot [f,g]'(a \cdot_{A} a') \cdot [f,g]'(s') \\
&= [f,g]'(s(a \cdot_{A} a')s')
\end{align*}

が成り立つので、 が成り立つ。 の場合も同様である。
の場合も同様に成り立つ。

• のとき

帰納法の仮定より、 が成り立つ。また の場合と同様の議論により、 が成り立つ。よって が成り立つ。

が homomorphism であることは が homomorphism であることから明らかです。
また を自然な homomorphism とすると、 が成り立ちます。任意の が を満たすなら が成り立つことも簡単に確かめられます。
最後に が 、 を満たすただ一つの arrow であることを証明します。

\begin{equation}
\forall h \colon M(\left| A \right| + \left| B \right|)\, / \sim \to M,\, h \circ i_{A} = f \land h \circ i_{B} = g \Rightarrow h = [f,g]
\end{equation}

を示せばよい。それには の UMP より、 を示せばよい。それには の UMP より、 かつ を示せばよい。
任意の に対して、

\begin{align*}
(\left| h \circ \pi \right| \circ \eta_{\left| A \right| + \left| B \right|} \circ i_{\left| A \right|})(a) &= h([a]) \\
&= \left| h \circ i_{A} \right| (a) \\
&= \left| f \right| (a)
\end{align*}

が成り立つ。同様に、 が成り立つので が成り立つ。

Example 3.10

任意の と任意の に対して、 を で定義する。すると が成り立つ。同様に が成り立つので、 は diagram を可換にする。
一方、任意の が diagram を可換にするとすると、任意の に対して、 が成り立つ。よって は 、 の coproduct である。

Proposition 3.11

証明の中で zero homomorphism という言葉が出てきます。 においては は initial object かつ terminal object となり、そのような対象を zero object と呼びます。
この zero object を用いると、任意の対象 間に なる arrow が存在することがわかります。( の箇所では が terminal object であることを利用し、 の箇所では が initial object であることを利用しています。)

3.4 Coequalizers

Example 3.20

集合圏 において任意の に対して coequalizer を具体的に構成します。
を で定義される 上の二項関係とし、 を から生成される equivalence relation とします。このとき、 を任意の に対して で定義します。

任意の に対して、、 であるから、 つまり を示せばよい。これは の定義より、、、 とすれば、 であるから が成り立つ。

次に任意の が を満たすとき、 を で定義します。このとき、 が well-defined であることを証明します。

\begin{equation}
\forall b,b' \in B,\, [b] = [b'] \Rightarrow \overline{h}([b]) = \overline{h}([b'])
\end{equation}

であるから である。よって が存在して、、 かつ が成り立つ。 に関する帰納法により示す。

• のとき

なら は明らかである。
なら が存在して、 かつ であるから、 が成り立つ。
なら が存在して、 かつ であるから、 が成り立つ。

• のとき

帰納法の仮定より が成り立つ。 に対して、 の場合と同様の議論により が成り立つ。よって が成り立つ。

が成り立つことは定義より明らかです。また が epic であるから、 はただ一つに決まります。よって は の coequalizer になります。

参考書籍

Category Theory (Oxford Logic Guides)

圏論 原著第2版

Steve Awodey の Category Theory を読む : Chapter 2

Steve Awodey の Category Theory を読む シリーズトップ

2.1 Epis and monos

Example 2.4

poset category において、任意の 間の arrow は ならばただ一つ存在すると定義されました。

• が monic であること。

任意の に対して、 を示せば良いが、 から への arrow は定義よりただ一つに決まるので、 が成り立つ。よって は monic である。

• が epic であること。

任意の に対して、 を示せば良いが、 から への arrow は定義よりただ一つに決まるので、 が成り立つ。よって は epic である。

a function is epic iff surjective in

背理法により示す。 が surjective ではないと仮定すると、 が成り立つ。一方、 であるから、 が存在する。ここで function を次のように定義する。
\begin{equation}
g(b) = \begin{cases}
f(a') & b = b' \\
b & b \neq b' \\
\end{cases}
\end{equation}
明らかに が成り立つ。任意の に対して、 より が成り立つが、 が epic であるから が成り立つ。これは と矛盾する。よって は surjective である。

任意の と任意の に対して、 を示せばよい。そのためには、任意の に対して、 を示せばよい。 が surjective であることより、 が成り立つので、 が成り立つ。よって は epic である。

any epi into a projective object splits

diagram を描ければいいのですが難しそうなので、証明を読む際は手元で diagram を書きながら読んでください。
以下の証明では、任意の圏 において を projective object であるとします。

と に対して、 が projective であることより、 が存在して が成り立つ。よって は split epi である。

any retract of a projective object is projective

任意の epic と任意の に対して、 を示す。 が の rectact であることより、 が成り立つ。一方、 が projective であることより と に対して、 が存在して、 が成り立つ。 を で定義すると、 が成り立つ。よって は projective である。

2.3 Generalized elements

ultrafilter に関する lemma

• only if case

任意の に対して、 とする。 とすると、 が filter であることより、 が成り立つ。よって となるが、これは が ultrafilter であることと矛盾する。
次に とする。このとき、 であることを背理示す。
であるとする。集合 を考え、この集合から filter を構成する。このとき が成り立つ。 であるとすると、 が成り立つ。つまり、 が成り立つ。よって が成り立つが、 が filter であることより が成り立ち、これは と矛盾する。よって が成り立ち、 が成り立つ。これは が maximal であることと矛盾する。よって が成り立つ。

• if case

が仮定を満たすような filter であるとき、 を示す。
より、 が存在する。すると の仮定より、 が成り立つ。 より であるから、 が成り立つ。 が filter であることより、 である。よって となるので、 は maximal filter である。

Example 2.12

• only if case

より は明らかに成り立つ。

• if case

仮定が成り立つとすると、 として を取ると が成り立つ。

2.5 Examples of products

3

において、任意の圏 の product が存在することを示します。証明することがたくさんあるので一つずつ確認していきましょう。

が圏であること

、、、 で を定義する。
すると圏 の性質より、 と が associativity と unit low を満たすことは明らかである。よって は圏となる。

が functor であること

を 任意の と任意の に対して、、 で定義する。
すると、 が成り立つので、 は functor の条件 (a) を満たす。
が成り立つので、 は functor の条件 (b) を満たす。
任意の に対して、 が成り立つので、 は functor の条件 (c) を満たす。よって は functor である。
に関しても同様である。

が product であること

任意の と、任意の に対して、 を 、 で定義する。
すると、

\begin{align*}
\left< F,G \right>_{1}(f \colon x \to x') &= (F_{1}(f), G_{1}(f) ) \colon (F_{0}(x), G_{0}(x) ) \to (F_{0}(x'), G_{0}(x') ) \\
&= (F_{1}(f), G_{1}(f) ) \colon \left< F,G \right>_{0}(x) \to \left< F,G \right>_{0}(x')
\end{align*}

が成り立つので、 は functor の条件 (a) を満たす。
が成り立つので、 は functor の条件 (b) を満たす。
任意の に対して、

\begin{align*}
\left< F,G \right>_{1}(f' \circ_{\bf{X}} f) &= (F_{1}(f' \circ_{\bf{X}} f), G_{1}(f' \circ_{\bf{X}} f) ) \\
&= (F_{1}(f') \circ_{\bf{C}} F_{1}(f), G_{1}(f') \circ_{\bf{D}} G_{1}(f) ) \\
&= (F_{1}(f'), G_{1}(f') ) \circ_{\bf{C} \times \bf{D}} (F_{1}(f), G_{1}(f) ) \\
&= \left< F,G \right>_{1}(f') \circ_{\bf{C} \times \bf{D}} \left< F,G \right>_{1}(f)
\end{align*}

が成り立つので、 は functor の条件 (c) を満たす。よって は functor である。
このとき、 と が成り立つので、diagram は可換となる。
また、任意の に対して、 が diagram を可換とするなら、、 が成り立つ。よって、 となり diagram を可換とする functor はただ一つに決まる。
以上より、 は と の product である。

product of posets constructed in

の要素である poset それ自体を圏としてみた場合、poset 間の写像が functor であることと、monotone function であることは同一視できるのでした。よってここで確認するべきことは、先の product の定義が poset になるかどうかということです。
任意の poset 、 に対して、 は 、 で定義される。一方、Hom の定義は と同値です。
このように に順序を入れた時に、 が poset となることは 、 がそれぞれ poset であることより明らかです。
よって、 において構成した product が において product になることが確認できました。
の場合も同様です。

2.6 Categories with products

is a functor

任意の product と 任意の に対して、 を 、 で定義する。
が成り立つので、 は functor の条件 (a) を満たす。
次に、 であるが、これは定義より 、 を満たす。一方で も 、 を満たす。よって、 の UMP より、 が成り立つので、 は functor の条件 (b) を満たす。
最後に、任意の product と に対して、 である。これは、定義より 、 を満たす。
一方で、 に対して、

\begin{align*}
r_{1} \circ ((g \times g') \circ (f \times f') ) &= (r_{1} \circ (g \times g') ) \circ (f \times f') \\
&= (g \circ q_{1}) \circ (f \times f') \\
&= g \circ (q_{1} \circ (f \times f') ) \\
&= g \circ f \circ p_{1}
\end{align*}

が成り立ち、同様に が成り立つ。よって の UMP より が成り立つ。よって は functor の条件 (c) を満たす。

product of -indexed family of object

と の組み が の product であるとは、任意の と 任意の に対して、ただ一つの が存在して、任意の に対して、 が成り立つこととして定義されます。

参考書籍

Category Theory (Oxford Logic Guides)

圏論 原著第2版

Steve Awodey の Category Theory を読む : Chapter 1

Steve Awodey の Category Theory を読む シリーズトップ

はじめに

Chapter 1 では以降の章では省略するような証明であっても省略せずに詳細に書いていきます。
数学書を自分で読み進める場合にはこの位細かい箇所にも注意を払いながら読まないといけないんだなと感じながら読んでもらえればと思います。

1.2 Functions of sets

ここでは集合とその間の関数が以下のような性質を満たすことを確認しています。

• 関数の合成 が定義できること
• 関数の合成 が associativity を満たすこと
• 全ての集合上に identity function を定義できること
• 関数の合成 と identitiy function が unit low を満たすこと

圏はここから集合や関数を object や arrowとして抽象し、上の性質のみに着目することで得られます。

関数の定義が既知であるとして述べられていないので確認しておきます。
集合 から集合 への関数とは、集合 と 集合 の直積集合 の部分集合 で以下の性質を満たすようなものです。
\begin{equation}
\forall a \in A,\ \left( \exists b \in B,\ (a,b) \in R \right) \land \left( \forall b,b' \in B,\ (a, b) \in R \land (a, b') \in R \Rightarrow b = b' \right)
\end{equation}
このことから任意の に対して対応する の要素がただ一つ決まるのでそれを と書くことができます。 よって が関数であるなら以下の論理式が成り立ちます。
\begin{equation}
\forall a,a' \in A,\ a = a' \Rightarrow f(a) = f(a')
\end{equation}
ある対応が与えられてそれが関数になるかどうかを確認しなければならない場合は、上の論理式を満たしていることを確認すればいいということです。

本文では , の二つの関数の合成 を以下のように定義してます。
\begin{equation}
(g \circ f)(a) = g(f(a)) \qquad a \in A
\end{equation}
この時実際に が関数になることを確認しなければなりません。そうでないと今定義した は集合圏 の外の存在になってしまいます。そのような場合は、合成演算 が閉じていないという言い方もします。
確認するべきことは以下のことです。

関数の合成 の定義よりこれは と同値である。 が関数であることより が成り立つ。 という仮定より、 が成り立つ。つぎに が関数であることにより、 が成り立つが、今 を で置き換えると、 であることから が成り立つ。よって、 は関数である。

本文中で関数の等しさについて言及されています。関数は直積集合の部分集合であると定義したので、関数が等しいとはこの部分集合が集合として等しいことであると定義します。つまり関数 が与えられた時にこの二つの関数が等しいとは が成り立つことであると定義します。これを理解していれば関数の合成演算 が associativity を満たすこと、つまり が成り立つことを証明するためには が成り立つことを証明すればよいということがわかります。

一点注意ですが、 が associative であることを示した際の等式 の は左辺と右辺は等しいという意味ですが、(1.1) の は左辺を右辺で定義するという意味なので、同じ でも意味が違います。定義するという意味で を使用することは数学ではよくあることなので注意して読んでください。

1.4 Examples of categories

有限集合を object、injective な関数を arrow とした時に圏 になることを確認しましょう。
合成関数 と は集合圏 より引き継ぐので、 と が associativity と unit low を満たすことなどは確認済みです。改めて証明する必要はありません。ここで確認するべきことは と の2点です。つまり injective な関数を合成したものが injective であることと、 を持ってきてもよいということです。
関数 が injective であるということは
\[ \forall (a\,a' : A),\ f(a) = f(a') \Rightarrow a = a' \]
が成り立つということです。これが inejctive であるという条件を正しく表現していることを確認してみてください。

任意の に関して であるとすると、 の定義より が成り立つ。この時 が injective であることより が成り立つ。また が injective であることより が成り立つ。よって は injective である。

が inejctive であることはほぼ自明ですが、念のため証明しておきます。

任意の に関して なら、 の定義より が成り立つ。よって は injective である。

任意の関数 と任意の に関して が高々2つの要素を持つような関数のみに限定した場合、圏になるでしょうか？答えは、圏になりません。関数の合成が定義できないからです。確認してみてください。

ここに挙げられている例の幾つかはこの後に出てくるので、そこで詳しく見ればいいと思います。この中で topological space と continuous mapping が作る圏 は重要な圏ですが、本文で詳細に言及されていないので圏になることを確認しておきます。
位相空間の定義自体は Wikipedia を確認してください。難しく考える必要はありません。ここで挙げられている他の例と同様に、集合 が与えられた時にその になんらかの構造が与えられているというだけです。ここでは3つの条件を満たす開集合系 が与えられています。圏 の対象は集合 だけではなくて、 との組み になります。当然 に対して開集合系の条件を満たす は一つではないので、もし別の が与えられたなら と は圏 における別の対象です。
構造を持つ対象間の関数は構造を保存しなければなりません。構造を保存しないような関数も集合圏 から持ってきて圏をつくれないのか？と思うかもしれませんが、そのような圏は数学の研究対象として面白くないのです。なので、構造を保存するような関数のみを arrow として考えて圏を構成します。
圏 においてはそれは連続写像 continuous mapping と呼ばれるものになります。関数 が から への連続写像であるとは、
\begin{equation}
\forall O \in \mathcal{O}(B),\ f^{-1}(O) \in \mathcal{O}(A)
\end{equation}
が成り立つということです。
位相空間の関数の合成と は集合圏 より引き継ぐので と が associativity と unit low を満たすことなどは確認済みです。よってここでは写像を合成しても連続写像になることと、 が連続写像であることを確認しましょう。

連続写像の定義より、任意の開集合 に関して、 となることを示せばよい。つまり を示す。
が連続写像であることにより である。また が連続写像であることにより が成り立つ。よって は連続写像である。

任意の開集合 に関して であるから は連続写像である。

ここまでは圏の arrow は構造を保存するような関数でした。ここでのポイントは圏における arrow は必ずしも関数ではないということです。
において arrow を の部分集合と定義し、 と を書籍にあるように定義した場合に が圏になることを確認しましょう。確認するべきことは

• が における arrow であること
• かつ である時に が arrow であること
• が associativity を満たすこと
• と が unit low をみたすこと

の4点です。上の二つは定義より明らかです。また は関数ですが、 は一般に関数にならないことも確認しておいてください。

証明するべきことは と が の部分集合として等しいということである。集合 , が同じ集合であるということは が成り立つこととして定義される。よってここでは かつ を示せばよい。2つを別々に示すのは面倒なので、 という記号を用いて一度に示す。

\begin{align*}
(a,d) \in T \circ (S \circ R) & \iff \exists c \in C,\ (a,c) \in (S \circ R) \land (c,d) \in T \\
&\iff \exists c \in C,\exists b \in B,\ (a,b) \in R \land (b,c) \in S \land (c,d) \in T \\
&\iff \exists b \in B,\exists c \in C,\ (a,b) \in R \land (b,c) \in S \land (c,d) \in T \\
&\iff \exists b \in B,\ (a,b) \in R \land (b,d) \in (T \circ S) \\
&\iff (a,d) \in (T \circ S) \circ R
\end{align*}

が成り立つ。よって である。

ここで存在量化子 の順番を入れ替えていることを確認してください。このような順番の入れ替えは数学の証明における正当な操作なのでしょうか？正しいのですが、数学の素養がないと確信がもてないと思います。
ここでは1ステップで交換していますが、実際には存在量化子の除去則を2回適用した後に続けて存在量化子の導入則を2回適用しています。存在量化子の除去則や導入則がどのようなものかは論理学の書籍などを参照してください。
同様に全称量化子に関しても順番を入れ替えることは可能です。しかし全称量化子と存在量化子の順番を自由に入れ替えることはできません。具体的には は証明できますが は証明できません。この量化子の順序によって表現する命題の意味が変わるということを認識できなかったことが、Cauchy が各点収束と一様収束の違いを認識できなかったことと関係しているそうです。
このように正確な演繹の手順を示さずに行う証明を informal な証明と言います。数学書などにある証明はほとんどすべて informal な証明です。informal な証明であっても、対応する formal な証明が存在すればそれは正しい証明なのですが、対応する formal な証明が構成できないのであれば、その証明は間違っています。数学書を読むときには informal な証明を可能な限り自分で formal な証明に置き換えながら読む必要があります。十分に formal な証明が記述されているかどうかはいい数学書を見分けるための重要な指標です。

なら がなりたつ。 より が成り立つので、 である。逆に、 とすると、 より が成り立つ。よって である。 の場合も同様である。

圏

を 、 を 、 を とする。圏の定義より が存在する。一方で、 から への arrow はただ1つのみ存在するので、 が成り立つ。

Definition 1.2

Functor は object から object, arrow から arrow への mapping であると書かれています。圏 の object の集まりを 、arrow の集まりを で表すとすると、表記の上では と記述されていますが、実際には は と の組 です。複数の mapping の組みを一つの表記で表すということは数学ではよくあることなのですが、数学の素養のない人には奇妙に映る点かもしれません。
Functor の満たすべき条件が書籍に書かれていますが、この区別を明確にした上で条件を書き直すと以下のようになります。

• (a)
• (b)
• (c)

(c) に関してはどの圏における合成なのかがわかるように のように圏を明示するようにしました。少し先取りになりますが、この条件は P.22 にある diagram が可換 commutative であるということと同じです。こちらの diagram を覚える方が覚えやすいかもしれません。
Functor を具体的に構成しなさいといわれた場合や、圏 から圏 への mapping が与えられて、この mapping が Functor であることを確認しなさいといわれた場合には、まず object から object への mapping と arrow から arrow への mapping を定義する、あるいは明確にした上で上の条件を満たしていることを確認します。

poset category

3で出てきた、poset とその間の monotone function の圏 と poset category との区別はついていますか？
圏 において object は poset、arrow は monotone function です。poset category において object は の要素で、arrow は以下で定義される の要素間の関係です。
\begin{equation}
\forall a,b \in P,\ a \to b \text{ if and only if } a \leq b
\end{equation}
圏 の object の内部それぞれに、また圏の構造が入っているということです。poset category のように異なる2つの object の間に、高々1つしか arrow が存在しない圏を痩せた圏 thin category と呼びます。ちなみに、異なる2つの object 間には一切 arrow の存在しない圏を離散圏 discrete category と呼びます。

が poset であること

は の部分集合の集合として定義されます。部分集合間の包含関係 を とみなした場合に が poset であることを確認するには以下の3つの条件を満たしていることを確認すればいいです。

• reflexivity:
• transitivity:
• antisymmetry:

証明するべきことは と同値であってこれは明らかである。

証明するべきことは と同値である。使用できる仮定は と である。一つ目の仮定と であることより が成り立ち、これと二つ目の仮定より が得られる。よって が成り立つ。

Functor は monotone function

が monotone function であることを示すには、 に関して を示す必要がある。 を poset category としてみると poset category は thin category なので、 なる arrow がただ1つ存在する。 が Functor であることより が存在する。よって、 が成り立つ。

monotone function は Functor

を Functor としてみようとすると、 は が から への function であるということから、 自身を と考えればいいことがわかる。そこで を定義する必要がある。 が monotone function であることにより、 に対してただ1つ存在する に対してただ1つの arrow が決まる。この arrow を として定義する。この定義より が Functor の条件 (a) を満たすことは明らかである。また poset category は thin category なので任意の object 間には高々1 つの arrow しかないという事実から (b),(c) も成り立つ。よって は Functor となる。

an example from topology

specialization は preorder

reflexivity: は明らかなので、transitivity を満たすことを示す。

示すことは である。 より が成り立つ。また より が成り立つ。よって であるから specialization は transitive である。

が 空間の場合

位相空間 が 空間であるとは以下の論理式が成り立つことです。
\begin{equation}
\forall x, y \in X,\ \exists U, V \in \mathcal{O}(X),\ (x \in U \land y \notin U) \land (x \notin V \land y \in V)
\end{equation}
この時 specialization は trivial になってしまいます。つまり specialization によって を圏としてみた場合に、 は離散圏になるということです。

背理法により示す。 とすると、 が 空間であることより、 が存在する。一方、 より が成り立つが、これは であることと矛盾する。よって である。

背理法による証明が初めて出てきました。中学生の頃に背理法による証明を習ったと思いますが、背理法がどういう証明方法か正確に認識できていますか？
一般に を仮定して矛盾が導出された場合に を導出することは、単なる否定の導入則です。演繹規則のリストに載っていると思います。確認してください。
一方背理法はもう少し複雑です。命題 を証明したいときに を仮定します。そして の仮定のもと矛盾が導出されれば が証明されたとするのが背理法です。 の仮定のもとで矛盾が導出されれば、否定の導入則により が証明できます。背理法の肝は ならば であるとしている点にあります。これを二重否定の除去則といって、哲学的な議論を呼んだ点でもあります。
は演繹規則を用いることで証明することができますが、逆の は演繹規則を用いるだけでは証明することができません。つまり、背理法を用いるということは、証明規則以外に別のルールを追加しているということです。
この二重否定除去則を使わないでどの程度の数学が展開できるかといったことも研究されていますが、ここでは普通に使用していくことにしましょう。

が 空間の場合

位相空間 が 空間であるとは以下の論理式が成り立つことです。
\begin{equation}
\forall x, y \in X,\ \exists U \in \mathcal{O}(X),\ (x \in U \land y \notin U) \lor (x \notin U \land y \in U)
\end{equation}
この時 specialization が antisymmetric であることを示します。

背理法により示す。 とする。 が 空間であることより、 が存在する。 とすると、 より が成り立つが、これは と矛盾する。 とすると、 より が成り立つが、これは と矛盾する。よって である。

この証明では の除去則が使用されています。一般に を証明する際には、 と の2つを示さないといけません。これは私も演繹規則として の除去則というものを学ぶまでは全く意識したことがありませんでした。ただ単に受験勉強の範囲では、 の除去則を使って証明しないといけないような問題に出会ってなかったということなのでしょう。

discrete category は poset

の要素間の ordering を以下のように定義します。
\begin{equation}
\forall x, y \in X,\ x \leq y \iff \exists f \colon x \to y \in {\bf{Dis}}(X)_{1}
\end{equation}
すると discrete category において arrow は しか存在しないのだから、 が成り立ちます。この ordering において、 が poset であることを示します。

に対して が存在するので、定義より明らか。

より であるが上で確認したように である。同様に、 と より が成り立つことから、 が成り立つ。よって示すべきことは、 であるが、これは が存在することから明らか。

上で確認したように、 から が成り立つ。

1.5 Isomorphisms

inverses are unique

任意の圏 において任意の が inverse を持つなら、それはただ一つに決まることを示します。何を示せばよいかすぐに論理式として表現できますか？
このことから、 が inverse を持つなら、そのただ一つに決まる inverse を として表すことができます。

を示すのに に対して を示すということをしていないことに注意してください。そのような証明ができるのは、 が関数の場合だけです。今は任意の圏 を考えているので、必ずしも arrow が function であるとは限りません。よって を示すには一般の圏において成り立つ性質のみを用いて証明する必要があります。この証明において associativity、unit lowと仮定しか用いていないことを確認してください。

において が closed であること

を示さないといけません。つまり を示せということです。関数 が isomorphic であるとは、 が injective かつ surjective であることです。関数 が inejctive であるというのは の所で見ました。関数 が surjective であるとは、
\begin{equation}
\forall b \in B,\ \exists a \in A,\ f(a) = b
\end{equation}
が成り立つこととして定義されます。

が inejctive であること。
を示せばよい。仮定と の定義より、 が成り立つ。 が injective であることより、 が成り立つ。また が inejctive であることより が成り立つ。よって は injective である。
が surjective であること。
を示せばよい。 が surjective であることより、 が存在する。また が surjective であることより、 が存在する。この を用いれば、 が成り立つ。よって は surjective である。

以上より は isomorphism である。

monoid homomorphism が inverse を保存すること。

であるが、 の inverse は unique に決まるので、 が成り立つ。

この補題により、ある関数 が group homomorphism であることを示す場合は、 と を示せば十分だということがわかります。
に関して inverse が unique に決まるということを証明せずに用いましたが、証明は一般の圏における inverse の uniqueness の証明と同様に証明できるので確認してください。

Cayley の定理

証明は書籍にある通りなのですが、色々と証明が省略されているのでここでは詳しく見ておきましょう。
証明では と同型の置換群として の subgroup を定義しています。よって証明するべきことを論理式として表現すると以下のようになります。
\begin{equation}
\forall G,\ \exists \bar{G} \subseteq Aut(G),\ \exists i \colon G \to \bar{G}, j \colon \bar{G} \to G,\ i \circ j = 1_{\bar{G}} \land j \circ i = 1_{G}
\end{equation}
書籍にあるように定義された が の subgroup であること、 が group homomorphism であることを確認する必要があります。

が automorphism であること。
として を取ると、任意の に対して 、 が成り立つので、 は automorphism である。
が の subgroup であること。
であることと、 を示せばよい。
任意の に対して で であるから、 である。また は上に示したことより であるので、 が成り立つ。

任意の に対して、 が成り立つ。また、 が成り立つ。よって は group homomorphism である。

任意の に対して、 が成り立つ。また、 が成り立つ。よって は group homomorphism である。

に関して、 と が成り立つことは容易に証明できます。以上より、 が成り立ちます。

Cayley の定理(圏)

arrow 全体が集合であるような任意の圏 に対しては、object が集合で arrow が function であるような同型の圏を具体的に構成することができるという定理です。
この定理の証明では書籍に示されている構成法によって が圏になることを確認しないといけません。また と が同型であることを示すには、圏の圏 において、functor と が存在して が成り立つことを確認する必要があります。

任意の に対して、 を で定義する。また を とする。
が associative であること。
任意の に対して、 が成り立つ。
unit low を満たすこと。
任意の に対して、 が成り立つ。 も同様である。

次に functor と を、 で定義します。この時、 が確かに functor になっていることを確認する必要があります。

定義より が functor の条件 (a) を満たすことは明らかである。また であるから条件 (b) を満たす。
任意の に対して、 が成り立つ。よって は functor の条件 (c) を満たす。

定義より が functor の条件 (a) を満たすことは明らかである。また であるから条件 (b) を満たす。
任意の に対して、 が成り立つ。よって は functor の条件 (c) を満たす。

と が成り立つことは明らかです。以上より、 が成り立ちます。

1.6 Constructions on categories

product

projection functor が実際に functor であることを確認しましょう。

任意の に対して、 であるから、 は functor の条件 (a) を満たす。
次に であるから、 は functor の条件 (b) を満たす。
最後に、 が成り立つので、 は functor の条件 (c) を満たす。

dual category

書籍に書いてある定義に基づいて、dual category が圏になることを確認しましょう。

が associative であること。
任意の に対して、

が成り立つ。よって は associative である。
と が unit low を満たすこと。

が成り立つので、 と は unit low を満たす。

arrow category

複数の arror の組みを一つの arrow とみなす例がまた出てきました。 が well-defined であることを確認しておきましょう。 が well-defined であることさえ確認できれば、 が associativity と unit low を満たすことは、 がそれらを満たすことから証明できます。

任意の に対して、 となることを示せばよい。つまり、 が成り立つことを示す。

よって は well-defined である。

と が functor になることも確認してください。

slice category

確認するべきことが沢山あります。一つずつ確認していきましょう。

任意の と任意の に対して、 で定義する。この時 が成り立つので、 は well-defined である。

上の証明では同じ表記 が における arrow と における arrow の二つの意味で使われています。本来は別物なので別の表記を使用するべきですが、面倒なので同じ表記を使用しています。当然この区別は大切なので、どちらの意味で使用しているのかを意識しながら証明を読んでください。
は を用いて定義されているので、associativity を満たすことは明らかです。また任意の に対して で定義すると、unit low を満たすことも簡単に証明できます。

書籍に base object を忘れる functor が存在すると書かれています。具体的に は 、 で定義されます。実際に が functor になることを確認しましょう。

任意の と任意の に対して、 であるから、 は functor の条件 (a) を満たす。
であるから、 は functor の条件 (b) を満たす。
が成り立つので、 は functor の条件 (c) を満たす。

次に任意の に対して composition functor を 、 で定義した時に が functor になることを確認します。

任意の と任意の に対して、 が成り立つので、 が成り立つ。よって は functor の条件 (a) を満たす。
であるから、 は functor の条件 (b) を満たす。
が成り立つので、 は functor の条件 (c) を満たす。

が functor であることを証明するために一つ準備をしておきます。

任意の と任意の に対して、、 が成り立つので、 である。

任意の と任意の に対して、 が成り立つので、 は functor の条件 (a) を満たす。
が成り立つので、 は functor の条件 (b) を満たす。
が上の より成り立つので、 は functor の条件 (c) を満たす。

example 1.8

任意の に対して、 と定義し、任意の に対して、 を と定義します。 が well-defined であることを確認すれば、 と が associativity と unit low を満たすことから、 が圏になることが証明できます。

任意の に対して、 が確かに から への arrow になることを確認すればよいが、
が成り立つので、 は well-defined である。

次に を証明します。そのために functor と を定義して、 かつ を証明します。
を 、 で定義する。

任意の と に対して、 は が を満たすことより、 が成り立つので、 が成り立つ。よって、 は functor の条件 (a) を満たす。
が成り立つので、 は functor の条件 (b) を満たす。
が成り立つので、 は functor の条件 (c) を満たす。

次に、 を 、 で定義する。

任意の と に対して、 は が を満たすことより、 が成り立つので、 が成り立つ。よって は functor の条件 (a) を満たす。
が成り立つので、 は functor の条件 (b) を満たす。
が成り立つので、 は functor の条件 (c) を満たす。

ここでは集合 の要素としての と、 を満たす関数を同じ という記号で表しています。このように表すことが妥当なのは、集合 の要素と、 から への関数の集合との間に1対1対応が存在するからです。
と が成り立つことは明らかなので、 が成り立ちます。

1.7 Free categories

Proposition 1.9

証明するべきことを論理式で表現すると次のようになります。
\begin{equation}
\exists i \colon A \to A^{\ast},\ \forall N,\ \forall f \colon A \to |N|,\ \exists !\ \bar{f} \colon A^{\ast} \to N,\ |\bar{f}| \circ i = f
\end{equation}
ここでは unique に存在するということを で表しました。この場合は以下の2つを証明しなければいけません。

• を満たす が存在すること (existence)
• そのような がただ1つに決まること (uniqueness)

ただ1つに決まることを決まることを示すには、任意の が を満たすとすると が成り立つことを証明します。
書籍の証明を見ると、前半では existence を証明し、後半では uniqueness を証明していることがわかります。時々、existence のみを証明し、uniqueness を証明していない"証明"を見かけるのですが、両方必ず証明しなければいけないので気をつけて下さい。

Proposition 1.10

ある arrow が特定の条件を満たし も同様にこの条件を満たす。一方で UMP により、そのような条件を満たす arrow はただ1つしか存在しないので が成り立つ。
という証明法が山のように出てくるので、このような証明法に慣れておいてください。

UMP of

を 、、 で定義する。

任意の に対して、 が成り立つので、 は functor の条件 (a) を満たす。
定義より が成り立つので、 は functor の条件 (b) を満たす。
最後に、

\begin{align*}
\bar{h}_{1}(e'_{m} \dots e'_{1} \circ_{{\bf{C}}(G)} e_{n} \dots e_{1}) &= \bar{h}_{1}(e'_{m} \dots e'_{1} e_{n} \dots e_{1}) \\
&= h_{1}(e'_{m}) \circ_{\bf{D}} \cdots \circ_{\bf{D}} h_{1}(e'_{1}) \circ_{\bf{D}} h_{1}(e_{n}) \circ_{\bf{D}} \cdots \circ_{\bf{D}} h_{1}(e_{1}) \\
&= \bar{h}_{1}(e'_{m} \dots e'_{1}) \circ_{\bf{D}} \bar{h}_{1}(e_{n} \dots e_{1})
\end{align*}

が成り立つので、 は functor の条件 (c) を満たす。

任意の に対して、 が成り立つ。
また任意の に対して、 が成り立つ。
よって、 が成り立つ。

以上で existence の証明は終わりです。最後に uniqueness の証明をします。

任意の に対して、 が成り立つ。
また、任意の に対して、

\begin{align*}
g_{1}(e_{n} \dots e_{1}) &= g_{1}(e_{n}) \circ_{\bf{D}} \cdots \circ_{\bf{D}} g_{1}(e_{1}) \\
&= (|g|_{1} \circ i_{1})(e_{n}) \circ_{\bf{D}} \cdots \circ_{\bf{D}} (|g|_{1} \circ i_{1})(e_{1}) \\
&= (|g| \circ_{\bf{Graph}} i)_{1}(e_{n}) \circ_{\bf{D}} \cdots \circ_{\bf{D}} (|g| \circ_{\bf{Graph}} i)_{1}(e_{1}) \\
&= h_{1}(e_{n}) \circ_{\bf{D}} \cdots \circ_{\bf{D}} h_{1}(e_{1}) \\
&= \bar{h}_{1}(e_{n} \dots e_{1})
\end{align*}

が成り立つので、 である。

おわりに

Chapter 1 はページ数は少ないのですが、例が多かったですね。自分の手を動かさずに例だからと読み流してしまうと、定義の理解がいい加減になって何を証明する必要があるのかがわからなくなります。すると証明を読みながら、本当にそれが証明として正しいのかといったことの確認が自分で出来なくなります。そのような状態で頑張って読み進めても最終的に頭に何も残らなかったということになるでしょう。
ここでは、証明するべきことを明確にするために、自然言語で書かれた定義や定理などを論理式として表現しなおしてから証明をしてきました。もし論理式に正確に表現しなおす作業を自分で出来ないのであれば、まだ数学書を読むだけの素養が身に付いていないのだと思います。その場合は下の記事を読んで、数学の素養を身につけてから読み進めるといいと思います。
www.orecoli.com

Chapter 1 ではほとんど証明を省略せずに詳細に解説してきましたが、Chapter 2 以降は簡単に証明できそうな事柄は飛ばしつつ解説を書いていきます。

参考書籍

Category Theory (Oxford Logic Guides)

圏論 原著第2版

CoqのLtacでmap関数を実装する

はじめに

Ltac は、Coq において証明の探索を自動化するための Domain Specific Language です。Coq においてプログラムを記述する言語は Gallina と呼ばれていて、これは依存型を持つ普通の関数型言語で意味論も目的も Ltac とは全く別物です。
Gallina で map関数を実装することは Haskell や OCaml で map関数を実装するのとほとんど同じで普通のことです。一方、Ltac は証明の探索の自動化を目的としているので普通の関数型言語と同じようにとはいかないのですが、 proof を具体的に構成するために直接 Gallina の項を生成したり、関数の引数として扱うことが可能であることを利用して関数型言語っぽいプログラミングが可能です。
この記事では Coq 入門者のバイブル？の Adam Chlipala の Certified Programming with Dependent Types の 14章3節の内容を参考に、 Ltac で map関数を実装する方法を紹介したいと思います。実際に map関数を Ltac で実装することには実用上の意味は全くありません。実装を通して Ltac の仕様を学ぶことが目的です。

length関数を実装する

map関数を実装する前に length関数を実装することを通していくつか基本的な Ltac の仕様を確認します。

Gallina 風の実装

とりあえず Gallina 風に Ltac で length関数を実装しようとすると以下のようになります。

Ltac length ls :=
  match ls with
    | nil => O
    | _ :: ls’ => S (length ls’)
end.

これを Coq に読み込ませると以下のようなエラーになります。

Error: The reference ls’ was not found in the current environment

Ltac の match 節では、パターンマッチする変数に ? をプレフィックスとしてつける必要があります。よってここでは ls' を ?ls' に修正します。

Ltac length ls :=
  match ls with
    | nil => O
    | _ :: ?ls’ => S (length ls’)
end.

Ltac から Gallina へ

上のコードを Coq に読み込ませると次のエラーが出力されます。

Error: The reference S was not found in the current environment

これは Ltac としてパースする際に S が tactics として定義されていないといっています。ここで S は nat のコンストラクタなので Gallina の項です。よってそのことをパーサーに明示的に指定してやる必要があります。そのために constr:(Gallina の項) という構文を使用します。

Ltac length ls :=
  match ls with
    | nil => O
    | _ :: ?ls’ => constr:(S (length ls’))
end.

これで Coq に length の定義を読み込ませることに成功します。実際に実行して結果を確認しましょう。結果の確認は以下のようにすると簡単です。

Goal False.
  let n := length (1 :: 2 :: 3 :: nil) in
  pose n.

実行すると以下のような出力が表示されます。

n := S (length (2 :: 3 :: nil)) : nat
==================
False

n := 3 : nat という結果を期待していたので、期待はずれですね。ここでの問題は constr:() 内で呼び出されている length が、今 Ltac で定義した length ではなく Gallina の list に対して定義されている length を参照している点です。

Gallina の項を Ltac 呼び出しの結果として受け取る

Gallina の項を返す Ltac を呼び出した結果を受け取って利用したい場合には let 構文を使用して一度変数に代入してやる必要があります。よって実装は以下のようになります。

Ltac length ls :=
  match ls with
    | nil => O
    | _ :: ?ls' =>
      let ls'' := length ls' in
      constr:(S ls'')
  end.

上と同様に実行すると以下の結果が表示されます。

n := 3 : nat
===================
False

望む結果が得られました。

気持ち悪い点

実装としては上の定義で良いのですが一点気持ち悪い点があります。
気づいた方もいらっしゃるかもしれませんが、S はそんな tactic は定義されていないとエラーになるのに、同様に Gallina の項で nat のコンスタラクタである O はそのまま記述しても意図した通りにパースできてしまう点です。詳しく仕様を調べていないのでなんとも言えませんが、S を同様に O の方も constr:O としておいた方がよい定義と言えるのではないかと思います。

map関数(Ltac引数)を実装する

次に引数の関数として Ltac の関数を取る map関数を実装します。

Ltac map T f :=
  let rec map' ls :=
    match ls with
      | nil => constr:(@nil T)
      | ?x :: ?ls' =>
        let x' := f x in
        let ls'' := map' ls' in
        constr:(x' :: ls'')
    end in
  map'.

let rec 構文を使用することでローカルな再帰関数を定義することができます。
constr:(@nil T) を constr:nil とすることができないのは、Ltac からはこの nil が何の型のリストか知ることができないからです。
Ltac には type of という関数が用意されていて Gallina の項の型を Ltac から知ることができます。引数 f が Gallina の項なら type of f とすることによって引数 f の返り値の型を知ることができますが、今引数 f は Ltac の関数なので type of を使用することはできません。よって明示的に map関数への引数として引数 f の返り値の型を渡しています。
この map関数を使用するには以下のように呼び出します。

Goal False.
  let ls := map (nat * nat)%type ltac:(fun n => constr:(n, n)) (1 :: 2 :: 3 :: nil) in
  pose ls

ここで ltac:() という構文が使用されています。これは constr:() と反対で、Gallina としてパースが行われている文脈で、Ltac の項としてパースするように指示する構文です。
Coq の proof editting mode では apply H. といった形の tactic の呼び出しを何度も見ると思います。この時 apply は Ltac で定義された tactic であるのに対して H は Gallina の項です。
つまり簡潔に proof を記述できるようにするために、二つのパースモードが自動的に切り替わっています。先頭のみを Ltac で定義された tactic として解釈し、続く項は Gallina の項として解釈されます。
このパースモードの挙動は map関数を定義する際にも有効であることが確認できます。つまり上の map関数の定義で f x としているところでは、f は Ltac の項で x は Gallina の項です。その下の map' ls' のところも同様です。
今定義した map関数では２つ目の項は Ltac の関数としてパースして欲しいので、ltac:() 構文を使用しています。
結果を確認してみましょう。

ls := (1, 1) :: (2, 2) :: (3, 3) :: nil : list (nat * nat)
===========================
False

これで Ltac の関数を引数として受け取る map関数を定義することができました。

map関数(Gallina引数)を実装する

最後に引数として Gallina の関数を取る map関数を実装します。これは Adam Chlipala の書籍にも載っていない例です。

Ltac map f :=
  match type of f with
    | ?T1 -> ?T2 =>
      let rec map' ls :=
        match ls with
          | nil => constr:(@nil T2)
          | ?x :: ?ls' =>
            let x' := eval compute in (f x) in
            let ls'' := map' ls' in
            constr:(x' :: ls'')  
        end in
      map'
  end.

上で説明した type of 関数を使用しています。type of 関数の返り値である引数 f の型をパターンマッチで分解することで、引数 f の返り値の型を取得することができます。ここでは ?T2 にバインドしています。
もう一点 eval ~ in という tactic が新しく出てきています。compute の箇所は、simpl や unfold など他にも指定できるものがいくつかあります。
もし eval を呼び出さずに f x の結果をそのまま constr:(f x) として使用したらどのようになるのでしょうか？そのように変更したと仮定して実行してみます。

Goal False.
  let ls := map (fun n : nat => (n, n)) (1 :: 2 :: 3 :: nil) in
  pose ls

今回は引数は Gallina の項なので ltac:() は必要ありません。また結果の型は (fun n : nat => (n, n)) の nat の部分を指定することで自動的に推論されます。全く型を指定しないと型の推論に失敗してエラーになります。この辺りは Ltac と Gallina の間で型情報をやり取りするタイミングなどの問題もあり複雑そうです。
結果は以下のようになります。

ls := (fun n : nat => (n, n)) 1 :: (fun n : nat => (n, n)) 2 :: (fun n : nat => (n, n)) 3 :: nil : list (nat * nat)
=======================
False 

β変換つまり関数適用が一切行われずにそのまま出力されてしまっています。ここでは評価を強制するために eval を使用しています。eval を使用した定義では以下のように出力されます。

ls := (1, 1) :: (2, 2) :: (3, 3) :: nil : list (nat * nat)
===========================
False

eval によって項の評価が行われるようになりました。

最後に

このように単純な例を実装することを通してでも、Ltac のセマンティクスなどについていくつか学べるところがあって面白いのではないかと思います。
Coq が他の定理証明支援系と比較して圧倒的に優れているのは Ltac の存在、つまり証明を自動化するプログラムを記述する能力にあるのではないかと個人的に考えています。
Ltac を征するものは Coq を征するといっても過言ではない？と思いつつ、これからも Ltac ハックに励んでいきたいと思います。

参考書籍

Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant

Steve Awodey の Category Theory を読む

はじめに

前回の記事では、圏論を学習する上では数学の基礎から学習する必要があると述べました。
　一方で、そんなに時間をかけていられない、かけられないといった理由から数学の素養が十分に身についていない状態で Category Theory (Oxford Logic Guides) を読み始めたいという人もいるでしょう。そのような人向けにこの本の副読本のような内容の記事を書いていこうと思います。
　 この本は十分にわかりやすい本なので解説の部分で内容を追加するようなことはしません。書籍の中で証明はされているけれども十分に明らかとは言えない箇所や、残りは読者に任せるとして省略されている箇所を中心に証明を追加していこうと思います。特に Chapter 1 では数学書を読む場合に自分で手を動かして補いながら読まないといけない箇所がどういう箇所なのか初学者にもわかるように書いていこうと思います。
　この記事が、これから独学で圏論を勉強しようとしている人や、勉強会でこの本を読もうとしている人の役に立てば嬉しいです。Texの入力に時間がかかるので更新はあまり早くできません。生暖かく見守ってください。目次は記事を書き次第アップデートしていきます。すべて書き終わりました。
　私が読んでいるのは英語の第２版ですがいくつか誤植があるので下に書いておきます。著者には報告済みなので第３版が出れば修正されるでしょう。

目次

• Chapter 1: Categories
• Chapter 2: Abstract structures
• Chapter 3: Duality
• Chapter 4: Groups and categories
• Chapter 5: Limits and colimits
• Chapter 6: Exponentials
• Chapter 7: Naturality
• Chapter 8: Categories of diagrams
• Chapter 9: Adjoints
• Chapter 10: Monads and algebras

errata list

page 27 line -5

to

page 63 line 1

to

page 63 line -3

to

page 67 line -3

to

page 68 line 3

(i.e., the images の閉じ括弧が無い

page 71 line 5

to or

page 99 line 3

example 5.9 to example 5.7

page 104 line -12

to

page 116 Exercise 8

圏 は厳密には圏にならないと思います。なぜなら pullback は up to isomorphism でのみ決まり、arrow の合成は結合則を満たさないからです。
後の章で出てくる skeltal category であるという条件を付け加えれば圏になります。

page 124 line -10

2番目のdiagramの右下の角 to

page 147 line -1

"and " に対して開き括弧が無い

page 156 line 2

と の間に空白を追加

page 162 line -1

to

page 163 line 2

to

page 167 line -13

to
to
to

書籍の p.18 などを見てみると、monoid や group の積は左から右の順に書いています。一方で、arrow の結合は右から左の順に書いています。
monoid や group を一点集合上の圏とした場合に、結合の順序が逆になります。

これは次の p.168 の 7.8 Monoidal categories 内の の定義における の箇所でも問題になります。
の使用法次第なのですが、p.169 において に対して と書いていることをみると、 は monoid や group の積と同様に左から右の順で使用することを想定しているように思われます。arrow の結合は一貫して右から左の順に書いているので、ここでは が正しい定義です。

page 169 line -3

to

page 183 line -5

to

page 188 line -2

to

page 189 line -7

to

page 192 line -2

"For, given objects in , if " to "For, given objects in , if "

page 197 line 5, line -5, line -3

cocone を記述する際には P.166 で定義した constant valued functor を使用したほうが一貫性があります。
to
to
to

page 198 line 6

to

page 198 line 17

to

page 220 line 12

もし dual image function をテキストのように定義すると が の開集合の時、 は必ずしも の開集合になりません。
よって は の right adjoint にはなり得ません。
では にあるように以下の定義に変えたらどうなるでしょうか？
\[f_{\ast}(U) = \bigcup \left\{ V \in \mathcal{O}(B) \,\middle|\, f^{-1}(V) \subseteq U \right\}\]
依然問題があります。この定義では確かに が の開集合の時、 は の開集合になります。
さらに は の right adjoint となります。
しかし今度は の right adjoint になりません。

page 221 line 10

to

page 224 Figure 9.1

to

page 225 line 3

\[\frac{\phi(x) \leq \psi(x,y)}{\phi(x) \leq \forall y.\psi(x,y)}\] to \[\frac{\phi(x) \vdash \psi(x,y)}{\phi(x) \vdash \forall y.\psi(x,y)}\]

page 229 line -5

to

page 230 line 9

単なる定義の置き換えなので、 を で置き換え可能です。
to

page 232 line 2

以下のように置き換えたほうが、本書の他の箇所との一貫性が高まります。
\[\frac{\vartheta_{j} \colon B_{j} \to A}{(\vartheta_{j}) \colon \sum_{j} B_{j} \to A}\]
to
\[\frac{(\vartheta_{j}) \colon \sum_{j} B_{j} \to A}{\vartheta_{j} \colon B_{j} \to A}\]

page 235 line 14, line 15

to

page 236 line 2

以下のように置き換えたほうが、本書の他の箇所との一貫性が高まります。
\[
\frac{Y \to \textstyle{\prod_{F}}(p)}{F^{*}Y \to p}
\]
to
\[
\frac{F^{*}Y \to p}{Y \to \textstyle{\prod_{F}}(p)}
\]

page 237 line 2

to

page 239 line 17

The definition of the solution set condition is incorrect.
To apply Lemma 9.30 in the proof of theorem 9.29, both and must be sets.
You can see the correct definition of the solution set condition on nLab.

page 240 line 2

to

page 242 line 12

"For complete posets , ," to
"For cocomplete posets , ,"

page 251 line -7

(a) to (c)

page 254 line -11

to

page 256 line -3

"the following square in " to
"the following square in "

page 257 line -4

to

page 258 line 1

" " to
" "

page 262 line -1

to

page 263 line -7

"every monoid arises from some adjunction." to
"every monad arises from some adjunction."

page 276 line 13

to

page 276 line -11

to

page 283 line -14

to

page 288 line 17

to

page 291 line 6

" over " to
" over "

page 292 line 9

"6. Here we consider " to
"7. Here we consider "

page 292 line -4

to

page 295 line 12

" and be given." to " and be given."

参考書籍

Category Theory (Oxford Logic Guides)

圏論 原著第2版

圏論に最短で入門する

はじめに

私が圏論という分野を知るきっかけは、おそらくこの文章を読んでいるほとんどの人と同様に Haskell の勉強をしたことがきっかけでした。

Haskell のモナドなどを利用する上では圏論を理解する必要は全くないのですが、型システムや処理系に関して詳しく知りたくて論文を読むと圏論の言葉が普通に使われていて、理解できずに断念していました。

そこで、当時数人が集まってやっていた圏論勉強会に参加して圏論の勉強を始めました。当時読んでいた書籍は Conceptual Mathematics: A First Introduction to Categories でした。この本は圏論の初学者向けに書かれた本で、数学的な知識をほとんど仮定せずに理解できるように書かれている非常によい本です。一方で全く数学の素養がない状態で読むと、証明もちゃんと追えているのかあやふやでなんとなく分かった気にさせられる本でもあります。私がまさにそのような状態でした。

しかし、ずっと圏論をちゃんと理解できるようになりたいと思っていたので、大学の数学科に進んだ学部1,2年生が学ぶような数学から勉強を始めました。圏論は比較的最近、1940年代に登場した理論で、数学の中でも非常に抽象的な理論なので数学を勉強しはじめてもすぐには出てきません。私は独学で勉強していたので数学の世界で右往左往することになったのですが、とりあえず現状で私が考える、圏論に至るための最短の道を紹介します。この順で勉強すれば、圏論の書籍を読む頃には、圏論が提供する抽象化を「あ〜あのことを言っているのか」と思いながら読めるようになると思います。

計算機科学の世界で生きてきたのにうっかり圏論と出会ってしまって、「今更また一から数学の勉強をしないといけないのか〜」と絶望に打ちひしがれている、昔の私のような人の一助になれば幸いです。

対象読者

どの位いるのかわかりませんが、昔の私と同様に以下のように考えている人を対象とします。

• 数学の素養がない状態で圏論を勉強してみたけれども抽象的すぎていまいち分かった気がしない
• 考えるための道具として圏論を使えるようになりたい
• 抽象的な圏論の考え方が、数学のどのような背景から生じてきたのかという歴史的な事実を含めて、数学者が圏論を理解しているような仕方で理解したい
• だけど回り道をしたくない

数学以前

数学にもともと興味があって数学科に進学した学生でも、大学以降で学ぶ数学についていけなくて挫折してしまう人は多いようです。私の考えでは、

• 大学受験までの計算主体の数学から、大学以降の証明主体の数学への移行を明確に意識させること
• 移行のためのトレーニングを積ませること

を学生が認識できる形で教育機会として大学が提供できていないことが原因なのではないかと考えています。

具体的には以下の能力、

• 証明するべきことを正しく論理式として表現する能力
• 許された演繹規則のみを用いて、正しい証明を構成する能力

の二つが身についていないと、今からあげる書籍を100回読んでも理解できるようにはならないと思います。

時々、はじめにはわからなかった証明も何度も読んでいればわかるようになってくる、といったことを言う人もいますが嘘です。数学の証明はそのような形で理解する性質のものではありません。そのようなことを言う人が語る数学はいい加減なので信用しないようにしましょう。

一般に数学書では、定義や証明は自然言語を用いて記述されています。そこで数学書を読む際には、

• 定義が出てきたら論理式として表現する
• 証明が出てきたら、証明するべきことを論理式として表現する
• 自然言語で記述されている証明に相当する論理式の操作が、許された操作のみを用いて行えるかを確認する

といったことを行いながら読み進めましょう。

上にあげた二つの能力を身につけることを意図したよい書籍を残念ながら私は知りません。入門書として野矢茂樹の 論理学 などから読み始めるといいでしょう。あなたがもし計算機科学の素養を持っているなら一番よい方法は Coq を使ってみることです。

数学の基礎

数学科に進学する学部生は解析と線形代数から勉強を始めるのが一般的なようです。圏論に最短で至るという目的ではとりあえずこの二つは飛ばして構いません。数学科の学部2年生後半から3年生に学ぶ内容から始めましょう。

はじめは松坂和夫の 集合・位相入門 です。

圏論では最も基本的な圏の例として、集合と関数の圏 、位相空間と連続写像の圏 が頻繁に登場するのでこの書籍の内容は外せません。松坂和夫の本は、長きにわたり数学科の学生の定番書になっているからか、誤植も少なく証明している定理も非常によく選ばれている感じがします。また証明が適度に厳密で、この仮定からこの結論はどうやって導いたの？ とか、詳細は読者に任せるといった、初学者泣かせも非常に少ないです。

次は同じく松坂和夫の 代数系入門 です。

ある代数系とその準同型写像の圏は圏論の書籍でも頻繁に登場します。準同型写像といった用語や意味は知っていて当然という前提で圏論の書籍は書かれています。群は数学のありとあらゆるところに出てきますし、環 上の加群はホモロジー代数を学ぶ上での基本です。 一方で、歴史的には重要でガロアの人生ドラマもあり面白い話題ですが、圏論を学ぶ上ではあまり必要ないので最後の章のガロア理論は飛ばしてもいいと思います。

これ以降の勉強をする際にも、この二つの書籍は何度も参照することになると思います。しっかり理解して常に持ち歩きましょう。

ホモロジー代数

代数的トポロジーの成果から図形的な内容を削ぎ落として、純粋に代数的な内容のみを取り出した分野がホモロジー代数です。圏論は、代数的トポロジーの研究の中で生じてきた概念だと言われています。ホモロジー代数の書籍では、圏の定義が登場し実際に利用します。ホモロジー代数の勉強を通して、圏論を実際に利用する感覚を身につけることができるでしょう。

ホモロジー代数に関して、日本語で読める書籍としては幾つかありますが河田敬義の ホモロジー代数 (岩波基礎数学選書) が良い本だと思います。残念なのは絶版中であるということです。私は近くの大学の図書館で読みました。

一点述べておきたいのは、ホモロジー代数は、代数的トポロジーの内容から図形的な内容を削ぎ落とした分野なので、それ自体がとても抽象的です。圏論が抽象的で理解できないからホモロジー代数の勉強を始めたが、こちらも圏論と同じくらい抽象的でわからない、ということになるかもしれません。私は、代数的トポロジーの知識をある程度身につけた状態でホモロジー代数の勉強をしました。ですので、代数的トポロジーの知識がない状態でホモロジー代数を理解できるか、理解したと思えるのか、わかりません。

もしホモロジー代数を勉強してみて抽象的すぎてよくわからないと思ったら、1年程度遠回りになってしまいますが、代数的トポロジーを勉強することをお勧めします。トポロジーの世界では急須とドーナツは同じ形だ、といった話を聞いたことがあると思います。代数的トポロジーの書籍では、図形を用いて直感的に理解できるような説明がされています。代数的トポロジーに関して、日本語で読めるよい教科書は残念ながら無いと思います。私は Joseph Rotman の書籍をお勧めします。An Introduction to Algebraic Topology (Graduate Texts in Mathematics)

直感的な説明、証明になりがちな代数的トポロジーの分野において、この書籍は、定義、証明が共に非常に厳密に記述されています。扱っている題材も十分で、初めから順に読めば、ホモロジー代数の背景にある幾何学的な内容を理解することができます。誤植が多いのが難点ですが、自分で証明を検証することができる能力があれば修正しながら読み通せるでしょう。

Allen Hatcher の Algebraic Topology は Amazon の書評では Rotman よりも高評価が多かったので購入しました。初めの章を読んでみて、定義、証明が非常にいい加減で読めたものじゃないと思い読むのをやめてしまいました。しかし、Rotman を読んでいて証明がわかりにくいところあってこちらの本を参照してみると、非常に簡潔に証明が与えられているということが何度かありました。どうやら、初めの章は導入で次の章から本格的に証明などをきちんとやっているようです。

圏論

圏論に単に到達するという意味では、ホモロジー代数の段階で圏論が出てくるので、目的はすでに達成しています。しかし、そこでは、ホモロジー代数で学んだ内容を圏の言葉を使って置き換えるといった使われ方がされており、ホモロジー代数以外の分野への圏論の応用や圏論自体の研究の成果を知るという観点からは不十分な内容になっています。そこで、圏論自体について書かれた書籍を1冊読むことをお勧めします。

圏論の書籍としては、初めに挙げた Conceptual Mathematics: A First Introduction to Categories があるのですが、ここまでに挙げた書籍を読んだ後では多少物足りなさを感じるでしょう。そこで私は Steve Awodey の Category Theory (Oxford Logic Guides) をお勧めします。この本も、Conceptual Mathmatics 同様、数学の素養のない人も読めるようにと謳われているのですが、数学の素養のない人には難しい内容になっています。逆に、数学の素養を持った人には、この本程度に数学の例を出してくれた方が理解しやすいと思います。この本の内容を理解すれば、かの有名な

モナドは単なる自己関手の圏におけるモノイド対象だよ。何か問題でも？

という言葉の意味も、理解できるようになっているでしょう。

ここで挙げた書籍も含めて以下の記事で圏論の入門書籍・入門資料をまとめました。ぜひ参考にしてみてください。
www.orecoli.com

もっと手取り早く圏論の勉強を始めたい人へ

上で挙げた Steve Awodey の Category Theory (Oxford Logic Guides) が圏論の入門書としてはおすすめです。ですが、数学の素養がある程度あることを前提としているために、証明は練習問題として読者に任せるとか、証明は明らか、として省略されている箇所が多数あります。
そこでより数学の素養を持たない人向けに、このブログの以下の記事で Awodey 本の詳細な証明をしています。書籍とこの記事の内容を両方参考にしながら読み進めることで、より Awodey 本が self-contained になり自習しやすくなると思います。ぜひ参考にしてみてください。
www.orecoli.com

おわりに

私が考える圏論にいたる最短の道を紹介しました。最短とはいえ、証明をしっかり自分で追いかけて練習問題も解き復習もしながら読むと、2年以上の時間がかかるでしょう。本当に価値のあるものは簡単には手に入らないと思いながら頑張ってください。初めに対象読者と設定した読者の方には一定程度の参考になるものと期待しています。

圏論は今や、数学のありとあらゆる分野に出てくるので、私が紹介した道が唯一ではないし最短でもないかもしれません。勉強を始めると興味を持つ分野などが出てくると思うので、その分野の方に脇道に逸れてみるというのもいいと思います。数学はそれ自体が、人生を捧げる価値のある非常に魅力的な学問だと思います。

大学数学の個別指導を始めました。詳しくは 大学数学の個別指導を始めます - 俺の Colimit を越えてゆけ をご覧ください。

紹介した書籍

論理学

集合・位相入門

代数系入門

ホモロジー代数 (岩波基礎数学選書)

Conceptual Mathematics: A First Introduction to Categories

An Introduction to Algebraic Topology (Graduate Texts in Mathematics)

Algebraic Topology

Category Theory (Oxford Logic Guides)

圏論 原著第2版

R加群の direct limit(順極限、直極限、帰納極限)に関する基本的な命題の証明

はじめに

私はホモロジー代数を以下の書籍で学びました。
絶賛絶版中で入手は困難ですが、現状でも日本語でホモロジー代数を勉強しようと思うと、この本一択になるのではないかと思います。
証明は自分で追える程度に十分に形式的に書かれていて、誤植などもほとんどなかったように記憶しています。

ホモロジー代数 (岩波基礎数学選書)

この本の第1章で direct limit ( と表す) という概念が出てきます。
そこで direct limit に関して成り立つ基本的な事実として、

• 任意の の元 に対して、或る十分大きな と が存在して、 が成り立つ

• 任意の の元 に対して、 となることと、十分に大きいある が存在して、 となることは同値である

ということが、証明無しに書かれています。

実は、この二つの命題を証明せよという問題が Atiyah MacDonald の『可換代数入門』の第2章の練習問題15にも出てきます。

Atiyah‐MacDonald 可換代数入門

そこでネットでこの練習問題に対する解答が落ちていないか検索するといくつか出てきますが、
一番まともな証明を載せているのは以下の PDF だと思います。

http://webhosting.math.tufts.edu/jdcarlson/intro_comm_alg(Palatino).pdf

しかし、この証明でも十分に形式的で、理解しやすいとは言えません(stackexchange にもっとわかりやすい証明があった気がする)。
そこで、私が証明を思い出すための備忘録として、この程度まで形式的に書いておけば大丈夫だろうという証明を書いておこうと思います。

証明のポイントは

• R加群とR加群の準同型の圏においては zero object(null object) が存在すること
• 上の事実と直和の UMP(Universal Mapping Property) を用いて、適当な準同型写像を定義すること

です。

の定義に関して

河田の『ホモロジー代数』ではR加群の直族 が以下のように定義されています。

有向順序集合 を添数集合とするR加群の族 および に対して
R準同型 が与えられ、かつ ならば
が成り立っているとき、 をR加群の直族という。

しかし、この定義は誤りで、以下のように修正する必要があります。

有向順序集合 を添数集合とするR加群の族 および に対して
R準同型 が与えられ、 かつ ならば
が成り立っているとき、 をR加群の直族という。

このように修正したうえで、直和R加群 と の部分集合
を考え、Sによって生成される の部分R加群を とする。
このとき direct limit を で定義する。また を標準的な準同型とする。

以上の準備をもとに、命題を証明します。

証明

命題1

に対して は全射であるから、 が成り立つ。
また、 がR加群の直和の定義より、有限個の を除いて であることと、 が有向順序であることより、 が成り立つ。
ここで、任意の に対して を以下のように定義する。

ここで とは のことで、これは が zero object であることから、必ずただ一つ存在する。
すると、直和の UMP より が存在して、任意の に対して、 が成り立つ。
とすれば、

が成り立つ。

命題2

if case

ならば、

が成り立つ。

only if case

ならば、 であるから、
と表すことができる。
が有向順序であることと、 が有限集合であることより、 が成り立つ。
ここで、任意の に対して を以下のように定義する。

すると、直和の UMP より が存在して、任意の に対して、 が成り立つ。この を用いれば、

まとめ

河田の『ホモロジー代数』の内容の修正と、direct limit 基本的な命題について証明をしました。自身で証明を再度行える程度に形式的な証明になっていたでしょうか？
不明な個所があればコメントで質問して下さい。

おわりに

数学はその性質上、書籍を読み進める中で、一部でもわからない箇所があると、それ以降の内容がちゃんと理解した気になれなかったりします。
人によるのかもしれませんが、少なくとも私はそうなので、初めてこの命題に出くわしたときはちゃんと証明できるまで先に進むことができませんでした。
この記事がどれほどの人の役に立つのかかわかりませんが、日本語で検索可能な文章として存在することに意味があると信じています。(私が読んでいないホモロジー代数の書籍に、十分に形式的な証明があって、私が知らないだけなのかもしれないが…)