読者です 読者をやめる 読者になる 読者になる

Steve Awodey の Category Theory を読む : Chapter 1

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

はじめに

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

1.2 Functions of sets

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

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

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

関数の定義が既知であるとして述べられていないので確認しておきます。
集合  A から集合  B への関数とは、集合  A と 集合  B の直積集合  A \times B の部分集合  R で以下の性質を満たすようなものです。
\[ \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) \]
このことから任意の  a : A に対して対応する  B の要素がただ一つ決まるのでそれを  R(a) と書くことができます。 よって  f \colon A \to B が関数であるなら以下の論理式が成り立ちます。
\[ \forall a,a' \in A,\ a = a' \Rightarrow f(a) = f(a') \]
ある対応が与えられてそれが関数になるかどうかを確認しなければならない場合は、上の論理式を満たしていることを確認すればいいということです。

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

 Lemma
\[ \forall a,a' \in A,\ a = a' \Rightarrow (g \circ f)(a) = (g \circ f)(a') \] Proof.
関数の合成  \circ の定義よりこれは  \forall (a\,a' : A),\ a = a' \Rightarrow g(f(a)) = g(f(a')) と同値である。 f が関数であることより  \forall (a\,a' : A),\ a = a' \Rightarrow f(a) = f(a') が成り立つ。 a = a' という仮定より、 f(a) = f(a') が成り立つ。つぎに  g が関数であることにより、  \forall (b\,b' : B),\ b = b' \Rightarrow g(b) = g(b') が成り立つが、今  b,b' f(a),f(a') で置き換えると、 f(a) = f(a') であることから  g(f(a)) = g(f(a')) が成り立つ。よって、 g \circ f は関数である。

 \square

本文中で関数の等しさについて言及されています。関数は直積集合の部分集合であると定義したので、関数が等しいとはこの部分集合が集合として等しいことであると定義します。つまり関数  f, g \colon A \to B が与えられた時にこの二つの関数が等しいとは  \forall (a : A),\ f(a) = g(a) が成り立つことであると定義します。これを理解していれば関数の合成演算  \circ が associativity を満たすこと、つまり  (h \circ g) \circ f = h \circ (g \circ f) が成り立つことを証明するためには  \forall (a : A),\ ( (h \circ g) \circ f)(a) = (h \circ (g \circ f) )(a) が成り立つことを証明すればよいということがわかります。

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

1.4 Examples of categories

 Sets_{\text{inj}}

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

 Lemma
\[ \forall f \colon A \to B, g \colon B \to C,\ f, g \text{ is injective} \Rightarrow g \circ f \text{ is inejctive.} \] Proof.
任意の  a, a' \in A に関して  (g \circ f)(a) = (g \circ f)(a') であるとすると、 \circ の定義より  g(f(a)) = g(f(a')) が成り立つ。この時  g が injective であることより  f(a) = f(a') が成り立つ。また  f が injective であることより  a = a' が成り立つ。よって  g \circ f は injective である。

 \square

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

 Lemma
\[ \forall A \in Obj(Set_{\text{inj}}),\ 1_{A}\text{ is injective.} \] Proof.
任意の  a, a' \in A に関して  1_{A}(a) = 1_{A}(a') なら、 1_{A} の定義より  a = a' が成り立つ。よって  1_{A} は injective である。

 \square

任意の関数  f \colon A \to B と任意の  b \in B に関して  f^{-1}(b) \subseteq A が高々2つの要素を持つような関数のみに限定した場合、圏になるでしょうか?答えは、圏になりません。関数の合成が定義できないからです。確認してみてください。

 Top

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

 Lemma
\[ \forall f \colon (A, \mathcal{O}(A)) \to (B, \mathcal{O}(B)), g \colon (B, \mathcal{O}(B)) \to (C, \mathcal{O}(C)),\ f, g\text{ is continuous} \Rightarrow g \circ f \text{ is continuous.} \] Proof.
連続写像の定義より、任意の開集合  O \in \mathcal{O}(C) に関して、 (g \circ f)^{-1}(O) \in \mathcal{O}(A) となることを示せばよい。つまり  f^{-1}(g^{-1}(O)) \in \mathcal{O}(A) を示す。
 g が連続写像であることにより  g^{-1}(O) \in \mathcal{O}(B) である。また  f が連続写像であることにより  f^{-1}(g^{-1}(O)) \in \mathcal{O}(A) が成り立つ。よって  g \circ f は連続写像である。

 \square

 Lemma
\[ \forall (A, \mathcal{O}(A)), \ 1_{(A, \mathcal{O}(A))} \text{ is continuous.} \] Proof.
任意の開集合  O \in \mathcal{O}(A) に関して  1^{-1}(O) = O \in \mathcal{O}(A) であるから  1_{(A, \mathcal{O}(A))} は連続写像である。

 \square

 Rel

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

  •  1 Rel における arrow であること
  •  R \subseteq A \times B かつ S \subseteq B \times C である時に  S \circ R が arrow であること
  •  \circ が associativity を満たすこと
  •  1 \circ が unit low をみたすこと

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

 Lemma
\[ \forall R \subseteq A \times B, S \subseteq B \times C, T \subseteq C \times D,\ T \circ (S \circ R) = (T \circ S) \circ R \] Proof.
証明するべきことは  T \circ (S \circ R) (T \circ S) \circ R A \times D の部分集合として等しいということである。集合  A,  B が同じ集合であるということは  A \subseteq B \land B \subseteq A が成り立つこととして定義される。よってここでは  \forall (a, d) \in A \times D,\, (a,d) \in T \circ (S \circ R) \Rightarrow (a,d) \in (T \circ S) \circ R かつ  \forall (a, d) \in A \times D,\, (a,d) \in (T \circ S) \circ R \Rightarrow (a,d) \in T \circ (S \circ R) を示せばよい。2つを別々に示すのは面倒なので、 \iff という記号を用いて一度に示す。
\[
\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*}
\]
が成り立つ。よって T \circ (S \circ R) = (T \circ S) \circ R である。

 \square

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

 Lemma
\[ \forall R \subseteq A \times B,\ R \circ 1_{A} = R \] Proof.
 (a, b) \in R \circ 1_{A} なら  \exists a',\ (a,a') \in 1_{A} \land (a', b) \in R がなりたつ。 (a,a') \in 1_{A} より  a = a' が成り立つので、 (a,b) \in R である。逆に、 (a,b) \in R とすると、 (a,a) \in 1_{A} より  (a,b) \in R \circ 1_{A} が成り立つ。よって  R \circ 1_{A} = R である。 1_{B} \circ R = R の場合も同様である。

 \square

 \bf{3}

 \ast \to \bigstar f \bigstar \to \bullet g \ast \to \bullet h とする。圏の定義より  g \circ f \colon \ast \to \bullet が存在する。一方で、 \ast から  \bullet への arrow はただ1つのみ存在するので、 h = g \circ f が成り立つ。

Definition 1.2

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

  • (a)  F_{1}(f \colon A \to B) = F_{1}(f) \colon F_{0}(A) \to F_{0}(B)
  • (b)  F_{1}(1_{A}) = 1_{F_{0}(A)}
  • (c)  F_{1}(g \circ_{C} f) = F_{1}(g) \circ_{D} F_{1}(f)

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

poset category

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

 \mathcal{P}(X) が poset であること

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

  • reflexivity:  \forall U \in \mathcal{P}(X),\ U \subseteq U
  • transitivity:  \forall U, V, O \in \mathcal{P}(X),\ U \subseteq V \land V \subseteq O \Rightarrow U \subseteq O
  • antisymmetry:  \forall U,V \in \mathcal{P}(X),\ U \subseteq V \land V \subseteq U \Rightarrow U = V

 Lemma
\[ \forall U \in \mathcal{P}(X),\ U \subseteq U \] Proof.
証明するべきことは  \forall x \in X,\ x \in U \Rightarrow x \in U と同値であってこれは明らかである。

 \square

 Lemma
\[ \forall U, V, O \in \mathcal{P}(X),\ U \subseteq V \land V \subseteq O \Rightarrow U \subseteq O \] Proof.
証明するべきことは  \forall x \in X,\ x \in U \Rightarrow x \in O と同値である。使用できる仮定は  \forall x \in X, x \in U \Rightarrow x \in V \forall x \in X, x \in V \Rightarrow x \in O である。一つ目の仮定と  x \in U であることより  x \in V が成り立ち、これと二つ目の仮定より  x \in O が得られる。よって  \forall x \in X,\ x \in U \Rightarrow x \in O が成り立つ。

 \square

Functor は monotone function

 Lemma
\[ \forall F \colon P \to Q,\ F \text{ is a Functor} \Rightarrow F \text{ is a monotone function from } P \text{ to } Q \] Proof.
 F が monotone function であることを示すには、 \forall a, a' \in P に関して  a \leq a' \Rightarrow F(a) \leq F(a') を示す必要がある。 P を poset category としてみると poset category は thin category なので、 f \colon a \to a' なる arrow がただ1つ存在する。 F が Functor であることより  F(f) \colon F(a) \to F(a') が存在する。よって、 F(a) \leq F(a') が成り立つ。

 \square

monotone function は Functor

 Lemma
\[ \forall F \colon P \to Q,\ F \text{ is a monotone function from } P \text{ to } Q \Rightarrow F \text{ is a Functor.}\] Proof.
 F を Functor としてみようとすると、 F_{0} F P から  Q への function であるということから、 F 自身を  F_{0} と考えればいいことがわかる。そこで  F_{1} を定義する必要がある。 F が monotone function であることにより、 \forall a, a' \in P に対してただ1つ存在する  f \colon a \to a' に対してただ1つの arrow  F_{0}(a) \to F_{0}(a') が決まる。この arrow を  F_{1}(f) として定義する。この定義より  F が Functor の条件 (a) を満たすことは明らかである。また poset category は thin category なので任意の object 間には高々1 つの arrow しかないという事実から (b),(c) も成り立つ。よって  F は Functor となる。

 \square

an example from topology

specialization は preorder

reflexivity:  \forall x \in X,\ x \leq x は明らかなので、transitivity を満たすことを示す。

 Lemma
\[ \forall x, y, z \in X,\ x \leq y \land y \leq z \Rightarrow x \leq z \] Proof.
示すことは  \forall U \in \mathcal{O}(X),\ x \in U \Rightarrow z \in U である。 x \leq y より  x \in U \Rightarrow y \in U が成り立つ。また  y \leq z より  y \in U \Rightarrow z \in U が成り立つ。よって  z \in U であるから specialization は transitive である。

 \square

 X T_{1} 空間の場合

位相空間  X T_{1} 空間であるとは以下の論理式が成り立つことです。
\[ \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) \]
この時 specialization は trivial になってしまいます。つまり specialization によって  X を圏としてみた場合に、 X は離散圏になるということです。

 Lemma
\[ \forall x, y \in X,\ x \leq y \Rightarrow x = y \] Proof.
背理法により示す。 x \neq y とすると、 X T_{1} 空間であることより、 \exists U, V \in \mathcal{O}(X),\ (x \in U \land y \notin U) \land (x \notin V \land y \in V) が存在する。一方、 x \leq y より  x \in U \Rightarrow y \in U が成り立つが、これは  y \notin U であることと矛盾する。よって  x = y である。

 \square

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

 X T_{0} 空間の場合

位相空間  X T_{0} 空間であるとは以下の論理式が成り立つことです。
\[ \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) \]
この時 specialization が antisymmetric であることを示します。

 Lemma
\[ \forall x, y \in X,\ x \leq y \land y \leq x \Rightarrow x = y \] Proof.
背理法により示す。 x \neq y とする。 X T_{0} 空間であることより、 \exists U \in \mathcal{O}(X),\ (x \in U \land y \notin U) \lor (x \notin U \land y \in U) が存在する。 x \in U \land y \notin U とすると、 x \leq y より  x \in U \Rightarrow y \in U が成り立つが、これは  y \notin U と矛盾する。 x \notin U \land y \in U とすると、 y \leq x より  y \in U \Rightarrow x \in U が成り立つが、これは  x \notin U と矛盾する。よって  x = y である。

 \square

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

discrete category は poset

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

 Lemma
\[ \forall x \in X,\ x \leq x \] Proof.
 \forall x \in X に対して  1_{x} \colon x \to x が存在するので、定義より明らか。

 \square

 Lemma
\[ \forall x, y, z \in X,\ x \leq y \land y \leq z \Rightarrow x \leq z \] Proof.
 x \leq y より  \exists f \colon x \to y であるが上で確認したように  f = 1 \land x = y である。同様に、 x = y y \leq z より  x \leq z が成り立つことから、 x = z が成り立つ。よって示すべきことは、 x \leq x であるが、これは  1_{x} \colon x \to x が存在することから明らか。

 \square

 Lemma
\[ \forall x, y \in X,\ x \leq y \land y \leq x \Rightarrow x = y \] Proof.
上で確認したように、 x \leq y から  x = y が成り立つ。

 \square

1.5 Isomorphisms

inverses are unique

任意の圏  \bf{C} において任意の  f \colon A \to B が inverse を持つなら、それはただ一つに決まることを示します。何を示せばよいかすぐに論理式として表現できますか?
このことから、 f \colon A \to B が inverse を持つなら、そのただ一つに決まる inverse を  f^{-1} として表すことができます。

 Lemma
\[ \forall g, g' \colon B \to A,\ g \circ f = 1_{A} \land f \circ g = 1_{B} \land g' \circ f = 1_{A} \land f \circ g' = 1_{B} \Rightarrow g = g' \] Proof.
 g = g \circ 1_{B} = g \circ (f \circ g') = (g \circ f) \circ g' = 1_{A} \circ g' = g'

 \square

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

 Aut(X) において  \circ が closed であること

 \forall f, g \in Aut(X),\ g \circ f \in Aut(X) を示さないといけません。つまり  \forall f, g \colon X \to X,\ f, g \text{ is isomorphism} \Rightarrow g \circ f \text{ is isomorphism} を示せということです。関数  f が isomorphic であるとは、 f が injective かつ surjective であることです。関数  f が inejctive であるというのは  Sets_{\text{inj}} の所で見ました。関数  f \colon A \to B が surjective であるとは、
\[ \forall b \in B,\ \exists a \in A,\ f(a) = b \]
が成り立つこととして定義されます。

 Lemma
\[ \forall f, g \colon X \to X,\ f, g \text{ is isomorphism} \Rightarrow g \circ f \text{ is isomorphism.} \] Proof.
 g \circ f が inejctive であること。
 \forall x, x' \in X,\ (g \circ f)(x) = (g \circ f)(x') \Rightarrow x = x' を示せばよい。仮定と  \circ の定義より、 g(f(x)) = g(f(x')) が成り立つ。 g が injective であることより、 f(x) = f(x') が成り立つ。また  f が inejctive であることより  x = x' が成り立つ。よって  g \circ f は injective である。
 g \circ f が surjective であること。
 \forall x' \in X,\ \exists x \in X,\ (g \circ f)(x) = x' を示せばよい。 g が surjective であることより、 \exists y \in X,\ g(y) = x' が存在する。また  f が surjective であることより、 \exists x \in X,\ f(x) = y が存在する。この  x を用いれば、 (g \circ f)(x) = g(f(x)) = g(y) = x' が成り立つ。よって  g \circ f は surjective である。

以上より  g \circ f は isomorphism である。

 \square

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

 Lemma
\[ \forall h \colon G \to H,\ h \text{ is a monoid homomorphism} \Rightarrow \forall g \in G,\ h(g^{-1}) = h(g)^{-1} \] Proof.
 h(g) \cdot_{H} h(g^{-1}) = h(g \cdot_{G} g^{-1}) = h(u_{G}) = u_{H} であるが、 h(g) の inverse  h(g)^{-1} は unique に決まるので、 h(g^{-1}) = h(g)^{-1} が成り立つ。

 \square

この補題により、ある関数  h \colon G \to H が group homomorphism であることを示す場合は、 \forall g,g' \in G,\ h(g \cdot_{G} g') = h(g) \cdot_{H} h(g') h(u_{G}) = u_{H} を示せば十分だということがわかります。
 \forall g \in G に関して inverse が unique に決まるということを証明せずに用いましたが、証明は一般の圏における inverse の uniqueness の証明と同様に証明できるので確認してください。

Cayley の定理

証明は書籍にある通りなのですが、色々と証明が省略されているのでここでは詳しく見ておきましょう。
証明では  G と同型の置換群として  Aut(G) の subgroup  \bar{G} を定義しています。よって証明するべきことを論理式として表現すると以下のようになります。
\[ \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} \]
書籍にあるように定義された  \bar{G} Aut(G) の subgroup であること、 i, j が group homomorphism であることを確認する必要があります。

 Lemma
\[ \bar{G} = \left\{ \bar{g}\, \middle| \, g \in G \right\} \text{ is a subgroup of } Aut(G) \] Proof.
 \bar{g} \in \bar{G} が automorphism であること。
 \bar{g}^{-1} として  \bar{g^{-1}} \in \bar{G} を取ると、任意の  h \in G に対して  (\bar{g^{-1}} \circ \bar{g})(h) = \bar{g^{-1}}(\bar{g}(h)) = g^{-1} \cdot g \cdot h = h = 1_{G}(h) (\bar{g} \circ \bar{g^{-1}})(h) = \bar{g}(\bar{g^{-1}}(h)) = g \cdot g^{-1} \cdot h = h = 1_{G}(h) が成り立つので、 \bar{g} は automorphism である。
 \bar{G} Aut(G) の subgroup であること。
 \forall \bar{g}, \bar{g'} \in \bar{G},\ \bar{g'} \circ \bar{g} \in \bar{G} であることと、 \forall \bar{g} \in \bar{G},\ \bar{g}^{-1} \in \bar{G} を示せばよい。
任意の  h \in G に対して  (\bar{g'} \circ \bar{g})(h) = \bar{g'}(\bar{g}(h)) = g' \cdot g \cdot h = \overline{g' \cdot g}(h) \overline{g' \cdot g} \in \bar{G} であるから、 \bar{g'} \circ \bar{g} \in \bar{G} である。また  \bar{g}^{-1} は上に示したことより  \bar{g^{-1}} であるので、 \bar{g}^{-1} \in \bar{G} が成り立つ。

 \square

 Lemma
\[ i \colon G \to \bar{G} \text{ is a group homomorphism.} \] Proof.
任意の  g, g' \in G に対して、 i(g' \cdot g) = \overline{g' \cdot g} = \bar{g'} \circ \bar{g} = i(g') \circ i(g) が成り立つ。また、 i(u_{G}) = \bar{u_{G}} = 1_{G} = u_{\bar{G}} が成り立つ。よって  i は group homomorphism である。

 \square

 Lemma
\[ j \colon \bar{G} \to G \text{ is a group homomorphism.} \] Proof.
任意の  \bar{g}, \bar{g'} \in \bar{G} に対して、 j(\bar{g'} \circ \bar{g}) = j(\overline{g' \cdot g}) = \overline{g' \cdot g}(u_{G}) = g' \cdot u_{G} \cdot g \cdot u_{G} = j(\bar{g'}) \cdot j(\bar{g}) が成り立つ。また、 j(u_{\bar{G}}) = j(\bar{u_{G}}) = u_{G} が成り立つ。よって  j は group homomorphism である。

 \square

 i, j に関して、 i \circ j = 1_{\bar{G}} j \circ i = 1_{G} が成り立つことは容易に証明できます。以上より、 G \cong \bar{G} が成り立ちます。

Cayley の定理(圏)

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

 Lemma
\[ {\bf{\bar{C}}} \text{ is a category.} \] Proof.
任意の  \bar{g_{1}} \colon \bar{D} \to \bar{H}, \bar{g_{2}} \colon \bar{H} \to \bar{I} に対して、 \circ_{\bf{\bar{C}}} \bar{g_{2}} \circ_{\bf{\bar{C}}} \bar{g_{1}} = \overline{g_{2} \circ_{\bf{C}} g_{1}} で定義する。また  1_{\bar{D}} \bar{1_{D}} とする。
 \circ_{\bf{\bar{C}}} が associative であること。
任意の   \bar{g_{1}} \colon \bar{D} \to \bar{H}, \bar{g_{2}} \colon \bar{H} \to \bar{I}, \bar{g_{3}} \colon \bar{I} \to \bar{J} に対して、 (\bar{g_{3}} \circ_{\bf{\bar{C}}} \bar{g_{2}}) \circ_{\bf{\bar{C}}} \bar{g_{1}} = \overline{g_{3} \circ_{\bf{C}} g_{2}} \circ_{\bf{\bar{C}}} g_{1} = \overline{(g_{3} \circ_{\bf{C}} g_{2}) \circ_{\bf{C}} g_{1}} = \overline{g_{3} \circ_{\bf{C}} (g_{2} \circ_{\bf{C}} g_{1})} = \bar{g_{3}} \circ_{\bf{\bar{C}}} \overline{g_{2} \circ_{\bf{C}} g_{1}} = \bar{g_{3}} \circ_{\bf{\bar{C}}} (\bar{g_{2}} \circ_{\bf{\bar{C}}} \bar{g_{1}}) が成り立つ。
unit low を満たすこと。
任意の  \bar{g} \colon \bar{D} \to \bar{H} に対して、 \bar{g} \circ_{\bf{\bar{C}}} 1_{\bar{D}} = \overline{g \circ_{\bf{C}} 1_{D}} = \bar{g} が成り立つ。 1_{\bar{H}} \circ_{\bf{\bar{C}}} \bar{g} = \bar{g} も同様である。

 \square

次に functor  F \colon \bf{C} \to \bf{\bar{C}} G \colon \bf{\bar{C}} \to \bf{C} を、 F_{0}(D) = \bar{D}, F_{1}(g) = \bar{g}, G_{0}(\bar{D}) = D, G_{1}(\bar{g}) = g で定義します。この時、 F, G が確かに functor になっていることを確認する必要があります。

 Lemma
\[ F \text{ is a functor.} \] Proof.
定義より  F が functor の条件 (a) を満たすことは明らかである。また  F_{1}(1_{D}) = \bar{1_{D}} = 1_{\bar{D}} であるから条件 (b) を満たす。
任意の  g_{1} \colon D \to H, g_{2} \colon H \to I に対して、 F(g_{2} \circ_{\bf{C}} g_{1}) = \overline{g_{2} \circ_{\bf{C}} g_{1}} = \bar{g_{2}} \circ_{\bf{\bar{C}}} \bar{g_{1}} = F(g_{2}) \circ_{\bf{\bar{C}}} F(g_{1}) が成り立つ。よって  F は functor の条件 (c) を満たす。

 \square

 Lemma
\[ G \text{ is a functor.} \] Proof.
定義より  G が functor の条件 (a) を満たすことは明らかである。また  G_{1}(1_{\bar{D}}) = G_{1}(\bar{1_{D}}) = 1_{D} であるから条件 (b) を満たす。
任意の  \bar{g_{1}} \colon \bar{D} \to \bar{H}, \bar{g_{2}} \colon \bar{H} \to \bar{I} に対して、 G(\bar{g_{2}} \circ_{\bf{\bar{C}}} \bar{g_{1}}) = G(\overline{g_{2} \circ_{\bf{C}} g_{1}}) = g_{2} \circ_{\bf{C}} g_{1} = G(\bar{g_{2}}) \circ_{\bf{C}} G(\bar{g_{1}}) が成り立つ。よって  G は functor の条件 (c) を満たす。

 \square

 G \circ_{Cat} F = 1_{\bf{C}} F \circ_{Cat} G = 1_{\bf{\bar{C}}} が成り立つことは明らかです。以上より、 \bf{C} \cong \bf{\bar{C}} が成り立ちます。

1.6 Constructions on categories

product

projection functor  \pi_{1} \colon \bf{C} \times \bf{D} \to \bf{C} が実際に functor であることを確認しましょう。

 Lemma
\[ \pi_{1} \text{ is a functor.} \] Proof.
任意の  f \colon C \to C' \in {\bf{C}}, g \colon D \to D' \in \bf{D} に対して、 \pi_{1_{1}}( (f,g) \colon (C,D) \to (C', D')) = f \colon C \to C' = f \colon \pi_{1_{0}}( (C,D)) \to \pi_{1_{0}}( (C', D')) であるから、 \pi_{1} は functor の条件 (a) を満たす。
次に  \pi_{1_{1}}(1_{(C,D)}) = \pi_{1_{1}}( (1_{C}, 1_{D})) = 1_{C} = 1_{\pi_{1_{0}}( (C,D))} であるから、 \pi_{1} は functor の条件 (b) を満たす。
最後に、 \pi_{1_{1}}( (f', g') \circ_{(\bf{C}, \bf{D})} (f, g)) = \pi_{1_{1}}( (f' \circ_{\bf{C}} f, g' \circ_{\bf{D}} g)) = f' \circ_{\bf{C}} f = \pi_{1_{1}}( (f',g')) \circ_{\bf{C}} \pi_{1_{1}}( (f, g)) が成り立つので、 \pi_{1} は functor の条件 (c) を満たす。

 \square

dual category

書籍に書いてある定義に基づいて、dual category  \bf{C}^{op} が圏になることを確認しましょう。

 Lemma
\[ {\bf{C}^{op}} \text{ is a category.} \] Proof.
 \circ_{\bf{C}^{op}} が associative であること。
任意の  f \colon C \to D, g \colon D \to H, h \colon H \to I に対して、
 f^{\ast} \circ_{\bf{C}^{op}} (g^{\ast} \circ_{\bf{C}^{op}} h^{\ast}) = f^{\ast} \circ_{\bf{C}^{op}} (h \circ_{\bf{C}} g)^{\ast} = ( (h \circ_{\bf{C}} g) \circ_{\bf{C}} f)^{\ast} = (h \circ_{\bf{C}} (g \circ_{\bf{C}} f))^{\ast} = (g \circ_{\bf{C}} f)^{\ast} \circ_{\bf{C}^{op}} h^{\ast} = (f^{\ast} \circ_{\bf{C}^{op}} g^{\ast}) \circ_{\bf{C}^{op}} h^{\ast}
が成り立つ。よって  \circ_{\bf{C}^{op}} は associative である。
 \circ_{\bf{C}^{op}} 1_{C^{\ast}} が unit low を満たすこと。
 1_{C^{\ast}} \circ_{\bf{C}^{op}} f^{\ast} = 1_{C}^{\ast} \circ_{\bf{C}^{op}} f^{\ast} = (f \circ_{\bf{C}} 1_{C})^{\ast}  = f^{\ast} = (1_{D} \circ_{\bf{C}} f)^{\ast} = f^{\ast} \circ_{\bf{C}^{op}} 1_{D}^{\ast} = f^{\ast} \circ_{\bf{C}^{op}} 1_{D^{\ast}}
が成り立つので、 \circ_{\bf{C}^{op}} 1_{C^{\ast}} は unit low を満たす。

 \square

arrow category

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

 Lemma
\[ \circ_{\bf{C}^{\to}} \text{ is well-defined.} \] Proof.
任意の  (g1,g2) \colon (f \colon A \to B) \to (f' \colon A' \to B'), (h1, h2) \colon (f' \colon A' \to B') \to (f'' \colon A'' \to B'') に対して、 (h1,h2) \circ_{\bf{C}^{\to}} (g1,g2) \colon f \to f’' となることを示せばよい。つまり、 (h2 \circ_{\bf{C}} g2) \circ_{\bf{C}} f = f'' \circ_{\bf{C}} (h1 \circ_{\bf{C}} g1) が成り立つことを示す。
 (h2 \circ_{\bf{C}} g2) \circ_{\bf{C}} f = h2 \circ_{\bf{C}} (g2 \circ_{\bf{C}} f) = h2 \circ_{\bf{C}} (f' \circ_{\bf{C}} g1) = (h2 \circ_{\bf{C}} f') \circ_{\bf{C}} g1 = (f'' \circ_{\bf{C}} h1) \circ_{\bf{C}} g1 = f'' \circ_{\bf{C}} (h1 \circ_{\bf{C}} g1)
よって  \circ_{\bf{C}^{\to}} は well-defined である。

 \square

 \bf{dom} \bf{cod} が functor になることも確認してください。

slice category

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

 Lemma
\[ \circ_{{\bf{C}}/C} \text{ is well-defined.} \] Proof.
任意の  f \colon X \to C, f' \colon X' \to C, f'' \colon X'' \to C と任意の  a \colon f \to f', a' \colon f' \to f'' に対して、 a' \circ_{{\bf{C}}/C} a = a' \circ_{\bf{C}} a で定義する。この時  f'' \circ_{\bf{C}} (a' \circ_{\bf{C}} a) = (f'' \circ_{\bf{C}} a') \circ_{\bf{C}} a = f' \circ_{\bf{C}} a = f が成り立つので、 \circ_{{\bf{C}}/C} は well-defined である。

 \square

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

書籍に base object  C を忘れる functor  U \colon {\bf{C}}/C \to \bf{C} が存在すると書かれています。具体的に  U U_{0}(f \colon X \to C) = X U_{1}(a \colon f \to f') = a で定義されます。実際に  U が functor になることを確認しましょう。

 Lemma
\[ U \text{ is a functor.} \] Proof.
任意の  f \colon X \to C, f' \colon X' \to C, f'' \colon X'' \to C と任意の  a \colon f \to f', a' \colon f' \to f'' に対して、 U_{1}(a \colon f \to f') = a \colon X \to X' = a \colon U_{0}(f) \to U_{0}(f') であるから、 U は functor の条件 (a) を満たす。
 U_{1}(1_{f}) = 1_{X} = 1_{U_{0}(f)} であるから、 U は functor の条件 (b) を満たす。
 U_{1}(a' \circ_{{\bf{C}}/C} a) = a' \circ_{\bf{C}} a = U_{1}(a') \circ_{\bf{C}} U_{1}(a) が成り立つので、 U は functor の条件 (c) を満たす。

 \square

次に任意の  g \colon C \to D \in \bf{C} に対して composition functor  g_{\ast} \colon {\bf{C}}/C \to {\bf{C}}/D g_{\ast_{0}}(f) = g \circ_{C} f g_{\ast_{1}}(a \colon f \to f') = a \colon X \to X' で定義した時に  g_{\ast} が functor になることを確認します。

 Lemma
\[ g_{\ast} \text{ is a functor.} \] Proof.
任意の  f \colon X \to C, f' \colon X' \to C, f'' \colon X'' \to C と任意の  a \colon f \to f', a' \colon f' \to f'' に対して、 (g \circ_{\bf{C}} f') \circ_{\bf{C}} a = g \circ_{\bf{C}} (f' \circ_{\bf{C}} a) = g \circ_{\bf{C}} f が成り立つので、 g_{\ast_{1}}(a \colon f \to f') = a \colon X \to X' = a \colon g_{\ast_{0}}(f) \to g_{\ast_{0}}(f') が成り立つ。よって  g_{\ast} は functor の条件 (a) を満たす。
 g_{\ast_{1}}(1_{f}) = 1_{X} = 1_{g_{\ast_{0}}(f)} であるから、 g_{\ast} は functor の条件 (b) を満たす。
 g_{\ast_{1}}(a' \circ_{{\bf{C}}/C} a) = a' \circ_{\bf{C}} a = g_{\ast_{1}}(a') \circ_{{\bf{C}}/D} g_{\ast_{1}}(a) が成り立つので、 g_{\ast} は functor の条件 (c) を満たす。

 \square

 {\bf{C}}/(-) \colon \bf{C} \to \bf{Cat} が functor であることを証明するために一つ準備をしておきます。

 Lemma
\[ \forall g \colon C \to D, h \colon D \to H,\ (h \circ_{\bf{C}} g)_{\ast} = h_{\ast} \circ_{\bf{Cat}} g_{\ast} \] Proof.
任意の  f \colon X \to C, f' \colon X' \to C と任意の  a \colon f \to f' に対して、 (h \circ_{\bf{C}} g)_{\ast_{0}}(f) = (h \circ_{\bf{C}} g) \circ_{\bf{C}} f = h \circ_{\bf{C}} (g \circ_{\bf{C}} f) = h_{\ast_{0}}(g_{\ast_{0}}(f)) = (h_{\ast} \circ_{\bf{Cat}} g_{\ast})_{0}(f) (h \circ_{\bf{C}} g)_{\ast_{1}}(a) = a = (h_{\ast} \circ_{\bf{Cat}} g_{\ast})_{1}(a) が成り立つので、 (h \circ_{\bf{C}} g)_{\ast} = h_{\ast} \circ_{\bf{Cat}} g_{\ast} である。

 \square

 Lemma
\[ {\bf{C}}/(-) \text{ is a functor.} \] Proof.
任意の  C, D, H \in {\bf{C}}_{0} と任意の  g \colon C \to D, h \colon D \to H に対して、 {\bf{C}}/(g \colon C \to D) = g_{\ast} \colon {\bf{C}}/C \to {\bf{C}}/D = g_{\ast} \colon {\bf{C}}/(C) \to {\bf{C}}/(D) が成り立つので、 {\bf{C}}/(-) は functor の条件 (a) を満たす。
 {\bf{C}}/(1_{C}) = 1_{C_{\ast}} = 1_{{\bf{C}}/(C)} が成り立つので、 {\bf{C}}/(-) は functor の条件 (b) を満たす。
 {\bf{C}}/(h \circ_{\bf{C}} g) = (h \circ_{\bf{C}} g)_{\ast} = h_{\ast} \circ_{\bf{Cat}} g_{\ast} = {\bf{C}}/(h) \circ_{\bf{Cat}} {\bf{C}}/(g) が上の  Lemma より成り立つので、 {\bf{C}}/(-) は functor の条件 (c) を満たす。

 \square

example 1.8

任意の  (A,a) に対して、 1_{(A,a)} = 1_{A} と定義し、任意の  f \colon (A,a) \to (B,b), g \colon (B,b) \to (C,c) に対して、 \circ_{\bf{Sets_{\ast}}} g \circ_{\bf{Sets_{\ast}}} f = g \circ_{\bf{Sets}} f と定義します。 \circ_{\bf{Sets_{\ast}}} が well-defined であることを確認すれば、  \circ_{\bf{Sets}} 1_{A} が associativity と unit low を満たすことから、 \bf{Sets_{\ast}} が圏になることが証明できます。

 Lemma
\[ \circ_{\bf{Sets_{\ast}}} \text{ is well-defined.} \] Proof.
任意の  f \colon (A,a) \to (B,b), g \colon (B,b) \to (C,c) に対して、 g \circ_{\bf{Sets_{\ast}}} f が確かに (A,a) から  (C,c) への arrow になることを確認すればよいが、
 (g \circ_{\bf{Sets}} f)(a) = g(f(a)) = g(b) = c が成り立つので、 \circ_{\bf{Sets_{\ast}}} は well-defined である。

 \square

次に  {\bf{Sets_{\ast}}} \cong 1/\bf{Sets} を証明します。そのために functor  F \colon {\bf{Sets_{\ast}}} \to 1/\bf{Sets} G \colon 1/{\bf{Sets}} \to {\bf{Sets_{\ast}}} を定義して、 G \circ_{\bf{Cat}} F = 1_{\bf{Set_{\ast}}} かつ  F \circ_{\bf{Cat}} G = 1_{1/\bf{Sets}} を証明します。
 F \colon {\bf{Sets_{\ast}}} \to 1/\bf{Sets} F_{0}( (A,a)) = a \colon 1 \to A F_{1}(f) = f で定義する。

 Lemma
\[ F \text{ is a functor.} \] Proof.
任意の  (A,a), (B, b), (C, c) \in {\bf{Sets_{\ast}}}_{0} f \colon (A, a) \to (B, b), g \colon (B, b) \to (C, c) に対して、 F_{1}(f) f f(a) = b を満たすことより、 f \circ_{\bf{Sets}} a = b が成り立つので、 F_{1}(f \colon (A,a) \to (B,b)) = f \colon a \to b = f \colon F_{0}( (A,a)) \to F_{0}( (B,b)) が成り立つ。よって、 F は functor の条件 (a) を満たす。
 F_{1}(1_{(A,a)}) = 1_{A} = 1_{a} = 1_{F_{0}( (A,a))} が成り立つので、 F は functor の条件 (b) を満たす。
 F_{1}(g \circ_{\bf{Sets_{\ast}}} f) = g \circ_{\bf{Sets}} f = g \circ_{1/\bf{Sets}} f = F_{1}(g) \circ_{1/\bf{Sets}} F_{1}(f) が成り立つので、 F は functor の条件 (c) を満たす。

 \square

次に、 G \colon 1/\bf{Sets} \to {\bf{Sets_{\ast}}} G_{0}(a \colon 1 \to A) = (A,a) G_{1}(f) = f で定義する。

 Lemma
\[ G \text{ is a functor.} \] Proof.
任意の  a,b,c \in {1/\bf{Set}}_{0} f \colon a \to b, g \colon b \to c に対して、 G_{1}(f) f f \circ_{\bf{Sets}} a = b を満たすことより、 (f \circ_{\bf{Sets}} a)(\ast) = f(a(\ast)) = f(a) = b = b(\ast) が成り立つので、 G_{1}(f \colon a \to b) = f \colon (A,a) \to (B,b) = f \colon G_{0}(a) \to G_{0}(b) が成り立つ。よって  G は functor の条件 (a) を満たす。
 G_{1}(1_{a}) = 1_{A} = 1_{(A,a)} = 1_{G_{0}(a)} が成り立つので、 G は functor の条件 (b) を満たす。
 G_{1}(g \circ_{1/\bf{Sets}} f) = g \circ_{\bf{Sets}} f = g \circ_{\bf{Sets_{\ast}}} f = G_{1}(g) \circ_{\bf{Sets_{\ast}}} G_{1}(f) が成り立つので、  G は functor の条件 (c) を満たす。

 \square

ここでは集合  A の要素としての  a と、 a(\ast) = a を満たす関数を同じ  a という記号で表しています。このように表すことが妥当なのは、集合  A の要素と、 1 から  A への関数の集合との間に1対1対応が存在するからです。
 G \circ_{\bf{Cat}} F = 1_{\bf{Set_{\ast}}} F \circ_{\bf{Cat}} G = 1_{1/\bf{Sets}} が成り立つことは明らかなので、  {\bf{Sets_{\ast}}} \cong 1/\bf{Sets} が成り立ちます。

1.7 Free categories

Proposition 1.9

証明するべきことを論理式で表現すると次のようになります。
\[ \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 \]
ここでは unique に存在するということを  \exists ! で表しました。この場合は以下の2つを証明しなければいけません。

  •  |\bar{f}| \circ i = f を満たす  \bar{f} が存在すること (existence)
  • そのような  \bar{f} がただ1つに決まること (uniqueness)

ただ1つに決まることを決まることを示すには、任意の  g \colon A^{\ast} \to N |g| \circ i = f を満たすとすると  g = \bar{f} が成り立つことを証明します。
書籍の証明を見ると、前半では existence を証明し、後半では uniqueness を証明していることがわかります。時々、existence のみを証明し、uniqueness を証明していない"証明"を見かけるのですが、両方必ず証明しなければいけないので気をつけて下さい。

Proposition 1.10

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

UMP of  {\bf{C}}(G)

 \bar{h} \bar{h}_{0}(v) = h_{0}(v) \bar{h}_{1}(e_{n} \dots e_{1}) = h_{1}(e_{n}) \circ_{\bf{D}} \cdots \circ_{\bf{D}} h_{1}(e_{1}) \bar{h}_{1}(1_{v}) = 1_{h_{0}(v)} で定義する。

 Lemma
\[ \bar{h} \text{ is a functor.} \] Proof.
任意の  e_{n} \dots e_{1} \colon v_{0} \to v_{n} に対して、 \bar{h}_{1}(e_{n} \dots e_{1}) = h_{1}(e_{n}) \circ_{\bf{D}} \cdots \circ_{\bf{D}} h_{1}(e_{1}) \colon h_{0}(v_{0}) \to h_{0}(v_{n}) = h_{1}(e_{n}) \circ_{\bf{D}} \cdots \circ_{\bf{D}} h_{1}(e_{1}) \colon \bar{h}_{0}(v_{0}) \to \bar{h}_{0}(v_{n}) が成り立つので、 \bar{h} は functor の条件 (a) を満たす。
定義より  \bar{h}_{1}(1_{v}) = 1_{h_{0}(v)} = 1_{\bar{h}_{0}(v)} が成り立つので、 \bar{h} は 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*}
\]
が成り立つので、 \bar{h} は functor の条件 (c) を満たす。

 \square

 Lemma
\[ |\bar{h}| \circ_{\bf{Graph}} i = h \] Proof.
任意の  v \in G_{0} に対して、 (|\bar{h}| \circ_{\bf{Graph}} i)_{0}(v) = (|\bar{h}|_{0} \circ i_{0})(v) = h_{0}(v) が成り立つ。
また任意の  e \in G_{1} に対して、 (|\bar{h}| \circ_{\bf{Graph}} i)_{1}(e) = (|\bar{h}|_{1} \circ i_{1})(e) = h_{1}(e) が成り立つ。
よって、 |\bar{h}| \circ_{\bf{Graph}} i = h が成り立つ。

 \square

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

 Lemma
\[ \forall g \colon {\bf{C}}(G) \to D,\ g \circ_{\bf{Graph}} i = h \Rightarrow g = \bar{h} \] Proof.
任意の  v \in {\bf{C}}(G)_{0} に対して、 g_{0}(v) = (|g|_{0} \circ i_{0})(v) = (|g| \circ_{\bf{Graph}} i)_{0}(v) = h_{0}(v) = \bar{h}_{0}(v) が成り立つ。
また、任意の  e_{n} \dots e_{1} \colon v_{0} \to v_{n} に対して、
\[
\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*}
\]
が成り立つので、 g = \bar{h} である。

 \square

おわりに

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

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

参考書籍

Category Theory (Oxford Logic Guides)

Category Theory (Oxford Logic Guides)

圏論 原著第2版

圏論 原著第2版