2016-04-30

Steve Awodey の Category Theory を読む : Chapter 5

数学数学-圏論

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

5.2 Pullbacks
- Proposition 5.5
- Exercise 3
5.3 Properties of pullbacks
5.4 Limits
- Proposition 5.14
5.6 Colimits
- Direct limits of groups
参考書籍

5.2 Pullbacks

Proposition 5.5

only if case しか証明されていないので、if case の証明を補っておきます。

$Lemma$
$(E, p_{1}, p_{2}) \text{ is a pullback of } f \text{ and } g \Rightarrow (E, \left< p_{1}, p_{2} \right>) \text{ is an equalizer of } f \circ \pi_{1} \text{ and } g \circ \pi_{2}.$

$Proof.$
任意の $z \colon Z \to A \times B$ に対して、 $f \circ \pi_{1} \circ z = g \circ \pi_{2} \circ z$ が成り立つとする。 $(E, p_{1}, p_{2})$ が pullback であることより、 $\exists !\,u \colon Z \to E$ が存在して $p_{1} \circ u = \pi_{1} \circ z$ かつ $p_{2} \circ u = \pi_{2} \circ z$ を満たす。
このとき、 $i = 1,2$ に対して、 $\pi_{i} \circ \left< p_{1}, p_{2} \right> \circ u = p_{i} \circ u = \pi_{i} \circ z$ であるから、 $A \times B$ の UMP より $\left< p_{1}, p_{2} \right> \circ u = z$ が成り立つ。
次に、任意の $u' \colon Z \to E$ に対して、 $\left< p_{1}, p_{2} \right> \circ u' = z$ が成り立つすると、 $i = 1,2$ に対して $p_{i} \circ u' = \pi_{i} \circ \left< p_{1}, p_{2} \right> \circ u' = \pi_{i} \circ z = p_{i} \circ u$ が成り立つ。よって pullback の UMP より $u' = u$ が成り立つ。

$\square$

Exercise 3

$Lemma$
$m \text{ is monic} \Rightarrow m' \text{ is monic}.$

$Proof.$
f:id:hitotakuchan:20160502130742p:plain
任意の $z_{1}, z_{2} \colon Z \to M'$ に対して、 $m' \circ z_{1} = m' \circ z_{2}$ が成り立つとする。このとき、 $m \circ f' \circ z_{1} = f \circ m' \circ z_{1} = f \circ m' \circ z_{2} = m \circ f' \circ z_{2}$ が成り立つが、 $m$ が monic であることより $f' \circ z_{1} = f' \circ z_{2}$ が成り立つ。
$M'$ が pullback であることより、 $\exists !\,z \colon Z \to M'$ が存在して、 $m' \circ z = m' \circ z_{1} = m' \circ z_{2}$ かつ $f' \circ z = f' \circ z_{1} = f' \circ z_{2}$ を満たすが、 $z_{1},z_{2}$ も diagram を可換にするので $z_{1} = z = z_{2}$ が成り立つ。よって $m'$ は monic である。

$\square$

5.3 Properties of pullbacks

Two pullbacks lemma

$Lemma$
$\text{If the two squares are pullbacks, so is the outer rectangle}.$

$Proof.$
f:id:hitotakuchan:20160503121002p:plain
任意の $x \colon Z \to A$ と $y \colon Z \to D$ に対して、 $g \circ f \circ x = h \circ y$ が成り立つとする。すると right square が pullback であることより、 $\exists !\, z' \colon Z \to E$ が存在して $g' \circ z' = y$ かつ $h' \circ z' = f \circ x$ を満たす。さらに left square が pullback であることより $\exists !\, z \colon Z \to F$ が存在して $h'' \circ z = x$ かつ $f' \circ z = z'$ を満たす。
次に、任意の $z'' \colon Z \to F$ に対して $h'' \circ z'' = x$ かつ $g' \circ f' \circ z'' = y$ が成り立つとする。 $f' \circ z''$ は $g' \circ (f' \circ z'') = y$ と $h' \circ (f' \circ z'') = f \circ h'' \circ z'' = f \circ x$ が成り立つから、right square の UMP より $f' \circ z'' = z'$ が成り立つ。すると left square の UMP より $z = z''$ が成り立つ。

$\square$

$Lemma$
$\text{If the right square and the outer rectangle are pullbacks, so is the left square}.$

$Proof.$
f:id:hitotakuchan:20160503121025p:plain
任意の $x \colon Z \to A$ と $y \colon Z \to E$ に対して、 $f \circ x = h' \circ y$ とする。 $g \circ f \circ x = g \circ h' \circ y = h \circ g' \circ y$ が成り立ち、outer rectangle が pullback であることより $\exists !\, z \colon Z \to F$ が存在して $h'' \circ z = x$ かつ $g' \circ f' \circ z = g' \circ y$ を満たす。
$h' \circ f' \circ z = f \circ h'' \circ z = f \circ x = h' \circ y$ が成り立つことと、right square が pullback であることより $f' \circ z = y$ が成り立つ。
次に、任意の $z' \colon Z \to F$ に対して $h'' \circ z' = x$ かつ $f' \circ z' = y$ が成り立つとする。すると $g' \circ f' \circ z' = g' \circ y$ が成り立つので、outer rectangle の UMP より $z = z'$ が成り立つ。

$\square$

Proposition 5.10

証明自体は難しくないので詳細は省略します。一般に pullback は up to isomorphism でしか決まりません。よって、この functor $h^{\ast}$ の存在を言うためには選択公理を仮定するか、後で出てくる skeletal という概念を用いて圏 $\bf{C}$ は skeletal であるという条件を付け加えないといけないと思います。

Example 5.13

$Lemma$
${\coprod_{j \in J} A_{\alpha(j)}} \text{ is a pullback}.$

$Proof.$
f:id:hitotakuchan:20160503141325p:plain
$\alpha'(j, a) = (\alpha(j), a)$ で定義する。 $a \in A_{\alpha(j)}$ であるから $\alpha'$ は well-defined である。
任意の $f \colon Z \to J$ と $g \colon Z \to {\coprod_{i \in I} A_{i}}$ に対して、 $\alpha \circ f = p \circ g$ が成り立つとする。このとき、任意の $z \in Z$ に対して $g(z) = (i, a)$ とするとき、 $h \colon Z \to {\coprod_{j \in J} A_{\alpha(j)}}$ を $h(z) = (f(z), a)$ で定義する。これは $\alpha(f(z)) = (\alpha \circ f)(z) = (p \circ g)(z) = i$ が成り立つので $a \in A_{\alpha(f(z))}$ となり well-defined である。また、 $(q \circ h)(z) = f(z)$ かつ $(\alpha' \circ h)(z) = (\alpha(f(z)), a) = (i, a) = g(z)$ が成り立つので、 $h$ は diagram を可換にする。
次に、任意の $h' \colon Z \to {\coprod_{j \in J} A_{\alpha(j)}}$ が $q \circ h' = f$ かつ $\alpha' \circ h' = g$ を満たすとする。任意の $z \in Z$ に対して $h'(z) = (j, b)$ とすると、 $q \circ h' = f$ より $j = f(z)$ が成り立つ。また $g(z) = (i, a)$ とすると、 $(i,a) = g(z) = (\alpha' \circ h')(z) = (\alpha(f(z)), b) = (p(g(z)), b) = (i, b)$ より $a = b$ が成り立つ。よって $h = h'$ が成り立つ。

$\square$

5.4 Limits

Proposition 5.14

上の two-pullback lemma の場合もそうでしたが、証明が easy diagram chase とだけ書かれていて省略されている場合、私の経験上全然 easy じゃないことが多いので補足しておきます。

$Lemma$
$(E,e,h) \text{ is a pullback then } (E,e) \text{ is an equalizer of } f,g.$

$Proof.$
f:id:hitotakuchan:20160506130719p:plain
初めに $\Delta$ が monic であることを示す。
任意の $x,y \colon Z \to B$ に対して、 $\Delta \circ x = \Delta \circ y$ が成り立つとする。すると $x = 1_{B} \circ x = \pi_{1} \circ \Delta \circ x = \pi_{1} \circ \Delta \circ y = 1_{B} \circ y = y$ が成り立つ。よって $\Delta$ は monic である。
次に、 $f \circ e = \pi_{1} \circ \left< f,g \right> \circ e = \pi_{1} \circ \Delta \circ h = h$ と $g \circ e = \pi_{2} \circ \left< f,g \right> \circ e = \pi_{2} \circ \Delta \circ h = h$ が成り立つので、 $f \circ e = g \circ e$ が成り立つ。
最後に、任意の $x \colon Z \to A$ に対して、 $f \circ x = g \circ x$ が成り立つとする。このとき $\pi_{1} \circ \Delta \circ f \circ x = f \circ x = \pi_{1} \circ \left< f,g \right> \circ x$ かつ $\pi_{2} \circ \Delta \circ f \circ x = f \circ x = g \circ x = \pi_{2} \circ \left< f,g \right> \circ x$ が成り立つから $B \times B$ の UMP より $\Delta \circ f \circ x = \left< f,g \right> \circ x$ が成り立つ。すると $Z$ が pullback であることより、 $\exists !\, z \colon Z \to E$ が存在して $e \circ z = x$ かつ $h \circ z = f \circ x$ を満たす。
Exercise 3 より $\Delta$ が monic なら $e$ は monic となるので $e \circ z = x$ を満たす $z$ はただ一つに決まる。よって $(E,e)$ は $f$ と $g$ の equalizer である。

$\square$

5.6 Colimits

Direct limits of groups

$G_{\inf}$ が $\omega$ -colimits であることの証明は簡単ではないです。ここでは詳細は証明は省略しますが、以下の記事で R 加群の場合の direct limit に関する基本的な性質の証明を行っているので、詳しく証明を確認したい人は参照してください。

www.orecoli.com

参考書籍

Category Theory (Oxford Logic Guides)

作者:Awodey, Steve
発売日: 2008/01/10
メディア: ペーパーバック

圏論原著第2版

作者:スティーブアウディ
発売日: 2015/09/19
メディア: 単行本

2016-04-07

Steve Awodey の Category Theory を読む : Chapter 4

数学数学-圏論

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

4.1 Groups in a category
- Corollary 4.6
4.2 The category of groups
4.3 Groups as categories
4.4 Finitely presented categories
- smallest congruence
参考書籍

4.1 Groups in a category

Corollary 4.6

任意の $(G,\circ,i,u)$ が abelian group であるとすると、 $\circ$ 、 $i$ 、 $u$ が group homomorphism であれば $(G, \circ, i, u)$ が group object であるための条件を満たすことは $(G, \circ, i, u)$ が abelian group であることから明らかです。
$\bf{Group}$ において $1$ は zero object なので $u \colon G \to 1 \to G$ はただ一つ存在する group homomorphism になります。そこで $\circ$ と $i$ が group homomorphism であることを証明します。

$Lemma$
$\circ \text{ is a group homomorphism}.$

$Proof.$
任意の $(g_{1}, g_{2}), (h_{1},h_{2}) \in G \times G$ に対して、 $(G,\circ,i,u)$ が abelian group であることより、

\begin{align*}
\circ((g_{1},g_{2}) \circ (h_{1}, h_{2}) ) &= \circ (g_{1} \circ h_{1}, g_{2} \circ h_{2}) \\
&= g_{1} \circ h_{1} \circ g_{2} \circ h_{2} \\
&= g_{1} \circ g_{2} \circ h_{1} \circ h_{2} \\
&= (\circ(g_{1}, g_{2}) ) \circ (\circ(h_{1}, h_{2}) )
\end{align*}

が成り立つので $\circ$ は group homomorphism である。

$\square$

$Lemma$
$i \text{ is a group homomorphism}.$

$Proof.$
任意の $g_{1}, g_{2} \in G$ に対して、 $(G,\circ,i,u)$ が abelian group であることより、 $i(g_{1} \circ g_{2}) = i(g_{2}) \circ i(g_{1}) = i(g_{1}) \circ i(g_{2})$ が成り立つので $i$ は group homomorphism である。

$\square$

4.2 The category of groups

$\sim$ is an equivalence relation

group $N$ が group $G$ の subgroup であるとは任意の $g_{1},g_{2} \in N$ に対して、 $g_{1} \cdot g_{2}^{-1} \in N$ が成り立つこととして定義されます。この定義から $N$ が $G$ の単位元を自身の単位元として含むことが証明できます。
さらに $N$ が $G$ の normal subgroup であるとは、任意の $g \in G$ と任意の $h \in N$ に対して、 $g \cdot h \cdot g^{-1} \in N$ が成り立つこととして定義されます。

$Lemma$
$\sim \text{ is an equivalence relation}.$

$Proof.$

reflexive

任意の $h \in N$ に対して、 $h \cdot h^{-1} = u \in N$ であるから、 $h \sim h$ が成り立つ。

symmetric

任意の $x,y \in N$ に対して $x \sim y$ とすると、 $x \cdot y^{-1} \in N$ が成り立つ。 $N$ は group であるから、 $(x \cdot y^{-1})^{-1} = y \cdot x^{-1} \in N$ が成り立つので $y \sim x$ が成り立つ。

transitive

任意の $x, y, z \in N$ に対して $x \sim y$ かつ $y \sim z$ とする。 $x \cdot y^{-1} \in N$ と $y \cdot z^{-1} \in N$ より $x \cdot y^{-1} \cdot y \cdot z^{-1} = x \cdot z^{-1} \in N$ が成り立つ。よって $x \sim z$ が成り立つ。

$\square$

Corollary 4.11

$N = \text{ker}(h)$ であるとき、 $\overline{h}$ が injective になることは書籍で証明されているので、ここでは $h$ が injective であるための必要十分条件が $\text{ker}(h) = \left\{ u \right\}$ であることを証明します。準備として以下を証明しておきます。

$Lemma$
$h \text{ is injective} \iff \pi \text{ is injective}.$

$Proof.$

only if case

任意の $x,y \in G$ に対して、 $[x] = [y]$ であるとする。このとき、 $h(x) = \overline{h}([x]) = \overline{h}([y]) = h(y)$ が成り立つが、 $h$ が injective であることより $x = y$ が成り立つ。よって $\pi$ は injective である。

if case

任意の $x,y \in G$ に対して、 $h(x) = h(y)$ であるとする。 $h = \overline{h} \circ \pi$ であるから $\overline{h}([x]) = \overline{h}([y])$ が成り立つが、 $\overline{h}$ が injective であるから $[x] = [y]$ が成り立つ。さらに $\pi$ が injective であるから $x = y$ が成り立つ。よって $h$ は injective である。

$\square$

この準備の元に次の補題を証明します。

$Lemma$
$\pi \text{ is injective} \iff \text{ker}(h) = \left\{ u \right\}$

$Proof.$

only if case

背理法により証明する。 $\text{ker}(h) \neq \left\{ u \right\}$ であるとすると、 $\exists x \in \text{ker}(h),\, x \neq u$ が存在する。すると $x \cdot u \in \text{ker}(h)$ より $[x] = [u]$ が成り立つ。仮定より $\pi$ が injective であるから $x = u$ が成り立つが、これは $x \neq u$ と矛盾する。よって $\text{ker}(h) = \left\{ u \right\}$ である。

if case

任意の $x,y \in G$ に対して、 $[x] = [y]$ であるとすると、 $x \cdot y^{-1} \in \text{ker}(h) = \left\{ u \right\}$ が成り立つ。よって $x = y$ となるので、 $\pi$ は injective である。

$\square$

Cokernels are special coequalizers

Cokernel に関しては Exercise 5 を通して見ておきましょう。Exercise 5 では abelian group を考えているので、二項演算子を $+$ 、単位元を $0$ で表します。
任意の $f \colon A \to B$ に対して、 $\pi \colon B \to B / \text{im}(f)$ を $\pi(b) = [b]$ で定義される natural homomorphism であるとします。

f:id:hitotakuchan:20160411185847p:plain

$Exercise\ 5\ (a)$
$Proof.$
任意の $a \in A$ に対して、 $\pi \circ f (a) = [f(a)]$ で $f(a) - 0_{B} \in \text{im}(f)$ であるから $[f(a)] = [0_{B}]$ が成り立つ。 $B/\text{im}(f)$ の単位元は $[0_{B}]$ であるから $\pi \circ f = 0_{B/\text{im}(f)}$ が成り立つ。
また任意の $g \colon B \to G$ に対して、 $g \circ f = 0_{G}$ が成り立つとする。 $\overline{g} \colon B/\text{im}(f) \to G$ を $\overline{g}([b]) = g(b)$ で定義する。このとき、 $[b] = [b']$ とすると $b - b' \in \text{im}(f)$ より $\exists a \in A,\, b - b' = f(a)$ が存在する。すると $g(b) - g(b') = g(b - b') = g(f(a)) = 0_{G}$ が成り立つ。よって $\overline{g}$ は well-defined である。
$g = \overline{g} \circ \pi$ が成り立つことは定義より明らか。また $\pi$ が epic であるから、 $\overline{g}$ はただ一つに決まる。

$\square$

(a) で証明した UMP より、 $(\pi, B/\text{im}(f) )$ は $f \colon A \to B$ と $0 \colon A \to 0 \to B$ の coequalizer であることがわかります。
次に cokernel を使用すると任意の coequalizer が構成できることを証明します。

f:id:hitotakuchan:20160411190220p:plain

$Exercise\ 5\ (b)$
$Proof.$
任意の $f,f' \colon A \to B$ に対して、 $f - f'$ を $(f - f')(a) = f(a) - f'(a)$ で定義すると、 $B$ が abelian group であることより

\begin{align*}
(f-f')(a + b) &= f(a + b) - f'(a + b) \\
&= f(a) + f(b) - f'(a) - f'(b) \\
&= f(a) - f'(a) + f(b) - f'(b) \\
&= (f-f')(a) + (f-f')(b)
\end{align*}

が成り立つので group homomorphism になる。 $f - f'$ の cokernel を $\pi \colon B \to B/\text{im}(f-f')$ とすると、 $\pi$ が $f$ 、 $f'$ の coequalizer となることを示す。
まず、 $\pi \circ (f - f') = 0$ より $\pi \circ f = \pi \circ f'$ が成り立つ。
次に、任意の $g \colon B \to G$ に対して、 $g \circ f = g \circ f'$ が成り立つとする。このとき $g \circ (f - f') = (g \circ f) - (g \circ f') = 0_{G} = g \circ 0_{B}$ が成り立つ。すると (a) で示した UMP より $\exists ! \,\overline{g} \colon B/\text{im}(f) \to G$ が存在して、 $g = \overline{g} \circ \pi$ が成り立つ。よって $(\pi, B/\text{im}(f-f') )$ は $f$ と $f'$ の coequalizer である。

$\square$

(c) に関しては以下の可換図式より $\text{Ker}(\text{cok}(f) ) \cong A/\text{Ker}(f)$ であることを確認してください。可換図式では $f$ の cokernel となる対象を $\text{Cok}(f)$ 、cokernel への homomorphism を $\text{cok}(f)$ 等として表しています。

f:id:hitotakuchan:20160411191918p:plain

4.3 Groups as categories

composition of the congruence category is well-defined

$\circ_{{\bf{C}}^{\sim}}$ を $\left< f',g' \right> \circ_{{\bf{C}}^{\sim}} \left< f,g \right> = \left< f' \circ f, g' \circ g \right>$ で定義するとき、 $\circ_{{\bf{C}}^{\sim}}$ が well-defined であることを証明します。

$Lemma$
$\circ_{{\bf{C}}^{\sim}} \text{ is well-defined}.$

$Proof.$
任意の $f \sim g \colon A \to B$ と $f' \sim g' \colon B \to C$ に対して、congruence の条件より $f' \circ f = f' \circ f \circ 1_{A} \sim f' \circ g \circ 1_{A} = f' \circ g$ が成り立つ。一方で $f' \circ g = 1_{C} \circ f' \circ g \sim 1_{C} \circ g' \circ g = g' \circ g$ が成り立つ。 $\sim$ が equivalence relation であることより、 $f' \circ f \sim g' \circ g$ が成り立つ。

$\square$

$\sim_{F}$ is a congruence

$\sim_{F}$ が equivalence relation であることは定義よりほぼ自明なので省略します。 $\sim_{F}$ が congruence の条件を満たすことを証明します。

$Lemma$
$\sim_{F} \text{ is a congruence}.$

$Proof.$
任意の $f,g \in {\bf{C}}_{1}$ に対して、 $f \sim_{F} g$ とすると定義より $\text{dom}(f) = \text{dom}(g)$ かつ $\text{cod}(f) = \text{cod}(g)$ が成り立つ。
また任意の $a \colon A \to \text{dom}(f)$ と $b \colon \text{cod}(f) \to B$ に対して、 $\text{dom}(b \circ f \circ a) = \text{dom}(a) = \text{dom}(b \circ g \circ a)$ かつ $\text{cod}(b \circ f \circ a) = \text{cod}(b) = \text{cod}(b \circ g \circ a)$ が成り立つ。また $F$ が functor であることより、 $F(b \circ f \circ a) = F(b) \circ F(f) \circ F(a) = F(b) \circ F(g) \circ F(a) = F(b \circ g \circ a)$ が成り立つので、 $b \circ f \circ a \sim_{F} b \circ g \circ a$ が成り立つ。よって $\sim_{F}$ は congruence である。

$\square$

Theorem 4.13

Theorem 4.13 の証明は難しくないのですが省略されているのでここで証明しておきます。

$Theorem$
$(\forall f,g \in {\bf{C}}_{1},\, f \sim g \Rightarrow f \sim_{F} g) \iff \exists !\, \tilde{F} \colon {\bf{C}}/\sim \, \to {\bf{D}},\, F = \tilde{F} \circ \pi$

$Proof.$

only if case

$\tilde{F}$ を $\tilde{F}_{0}(C) = F(C)$ 、 $\tilde{F}_{1}([f]) = F(f)$ で定義する。このとき、任意の $f,g \in {\bf{C}}_{1}$ に対して $[f] = [g]$ であるとすると、 $f \sim g$ であるから、仮定より $f \sim_{F} g$ が成り立つ。よって定義より $F(f) = F(g)$ が成り立つので、 $\tilde{F}_{1}$ は well-defined である。
次に $\tilde{F}$ が functor であることを示す。
$\tilde{F}_{1}([f] \colon A \to B) = F(f) \colon F(A) \to F(B) = F(f) \colon \tilde{F}_{0}(A) \to \tilde{F}_{0}(B)$ であるから、 $\tilde{F}$ は functor の条件 (a) を満たす。
また、 $\tilde{F}_{1}([id] \colon A \to A) = F(id) = id_{F(A)} = id_{\tilde{F}_{0}(A)}$ が成り立つので、 $\tilde{F}$ は functor の条件 (b) を満たす。
最後に $\tilde{F}_{1}([f'] \circ [f]) = \tilde{F}_{1}([f' \circ f]) = F(f' \circ f) = F(f') \circ F(f) = \tilde{F}_{1}([f']) \circ \tilde{F}_{1}([f])$ が成り立つので、 $\tilde{F}$ は functor の条件 (c) を満たす。
よって $\tilde{F}$ は functor である。
この $\tilde{F}$ が $F = \tilde{F} \circ \pi$ を満たすことは定義より明らかである。また $\pi$ が epic であることより、 $\tilde{F}$ はただ一つに決まる。

if case

$f \sim g$ であるとすると、congruence の条件より $\text{dom}(f) = \text{dom}(g)$ かつ $\text{cod}(f) = \text{cod}(g)$ が成り立つ。さらに $[f] = [g]$ であるから、 $F(f) = (\tilde{F} \circ \pi)(f) = \tilde{F}([f]) = \tilde{F}([g]) = (\tilde{F} \circ \pi)(g) = F(g)$ が成り立つので $f \sim_{F} g$ が成り立つ。

$\square$

$Lemma$
$\tilde{F} \colon {\bf{C}}/\text{ker}(F) \to D \text{ is a faithful functor}.$

$Proof.$
任意の $[f],[g] \colon A \to B$ に対して $\tilde{F}([f]) = \tilde{F}([g]) \Rightarrow [f] = [g]$ を示せばよい。 $[f],[g] \colon A \to B$ より $\text{dom}(f) = \text{dom}(g)$ かつ $\text{cod}(f) = \text{cod}(g)$ が成り立つ。また $F(f) = (\tilde{F} \circ \pi)(f) = \tilde{F}([f]) = \tilde{F}([g]) = (\tilde{F} \circ \pi)(g) = F(g)$ が成り立つので $f \sim_{F} g$ つまり $[f] = [g]$ が成り立つ。よって $\tilde{F}$ は faithful functor である。

$\square$

4.4 Finitely presented categories

smallest congruence

書籍において $\sim_{\Sigma}$ を $g = g' \in \Sigma$ なら $g \sim g'$ を満たす congruence の中で最小の congruence として定義しています。congruence の intersection が congruence になることから、 $\sim_{\Sigma}$ が存在すると書かれていますが本当でしょうか？
これは、 $g = g' \in \Sigma$ なら $g \sim g'$ を満たす congruence が少なくとも一つは存在することを示さないと定義として意味がありません。ここでは以下の記事の内容を元に具体的に $\sim_{\Sigma}$ を構成します。
www.orecoli.com

まず二項関係 $\Sigma'$ を $\Sigma' = \left\{ (b \circ f \circ a, b \circ g \circ a) \,\middle| \, (f,g) \in \Sigma,\, \forall a,b,\, \text{cod}(a) = \text{dom}(f),\, \text{dom}(b) = \text{cod}(f) \right\}$ で定義します。上の記事を参考に $\Sigma'$ から生成される equivalence relation として $\sim_{\Sigma}$ を定義します。このとき $\sim_{\Sigma}$ が $(f,g) \in \Sigma$ なら $f \sim g$ を満たす最小の congruence であることを証明します。初めに $\sim_{\Sigma}$ が congruence であることを証明します。

$Lemma$
$\sim_{\Sigma} \text{ is a congruence}.$

$Proof.$
任意の $f,g \in {\bf{C}}_{1}$ に対して $f \sim_{\Sigma} g$ であるとする。

$n = 1$ のとき

$f = g$ であるとすると、 $\text{dom}(f) = \text{dom}(g)$ かつ $\text{cod}(f) = \text{cod}(g)$ は明らか。また任意の $a,b$ に対して $b \circ f \circ a = b \circ g \circ a$ であるから、 $\sim_{\Sigma}$ が equivalence relation であることより $b \circ f \circ a \sim_{\Sigma} b \circ g \circ a$ が成り立つ。
$(f, g) \in \Sigma'$ とすると、 $\exists (f',g') \in \Sigma$ と $\exists x,y$ が存在して $(f,g) = (y \circ f' \circ x, y \circ g' \circ x)$ と表される。このとき $\text{dom}(f) = \text{dom}(g)$ かつ $\text{cod}(f) = \text{cod}(g)$ は明らかである。また任意の $a,b$ に対して $(b \circ y \circ f' \circ x \circ a, b \circ y \circ g' \circ x \circ a) \in \Sigma'$ であるから、 $b \circ f \circ a \sim_{\Sigma} b \circ g \circ a$ が成り立つ。
$(g,f) \in \Sigma'$ の場合も $(f,g) \in \Sigma'$ の場合と同様である。

$n \gt 1$ のとき

帰納法の仮定により $\text{dom}(f) = \text{dom}(x_{n-1})$ 、 $\text{cod}(f) = \text{cod}(x_{n-1})$ かつ任意の $a,b$ に対して $b \circ f \circ a \sim_{\Sigma} b \circ x_{n-1} \circ a$ が成り立つ。一方で $x_{n-1} = g$ 、 $(x_{n-1}, g) \in \Sigma'$ 、 $(g, x_{n-1}) \in \Sigma'$ のそれぞれの場合に対して、 $n = 1$ の場合と同様の議論により、 $\text{dom}(x_{n-1}) = \text{dom}(g)$ 、 $\text{cod}(x_{n-1}) = \text{cod}(g)$ かつ任意の $a,b$ に対して $b \circ x_{n-1} \circ a \sim_{\Sigma} b \circ g \circ a$ が成り立つ。
よって $\sim_{\Sigma}$ が equivalence relation であることより $\text{dom}(f) = \text{dom}(g)$ 、 $\text{cod}(f) = \text{cod}(g)$ かつ任意の $a,b$ に対して $b \circ f \circ a \sim_{\Sigma} b \circ g \circ a$ が成り立つ。

$\square$

次に $\sim_{\Sigma}$ が $(f,g) \in \Sigma$ ならば $f \sim g$ を満たす最小の congruence であることを証明します。 $\sim_{\Sigma}$ が $(f,g) \in \Sigma$ ならば $f \sim_{\Sigma} g$ をみたすことは、 $a = 1_{\text{dom}(f)}$ 、 $b = 1_{\text{cod}(f)}$ とすれば $(f,g) \in \Sigma'$ となることから明らかです。

$Lemma$
$\sim_{\Sigma} \text{ is the smallest congruence}.$

$Proof.$
$\sim$ を $(f,g) \in \Sigma$ ならば $f \sim g$ を満たす任意の congruence であるとする。
任意の $f,g \in {\bf{C}}_{1}$ に対して $f \sim_{\Sigma} g$ であるとする。

$n = 1$ のとき

$f = g$ とすると、 $\sim$ は equivalence relation であるから $f \sim g$ が成り立つ。
$(f,g) \in \Sigma'$ とすると、 $\exists (f',g') \in \Sigma$ と $\exists x,y$ が存在して $(f,g) = (y \circ f' \circ x, y \circ g' \circ x)$ と表される。仮定より $f' \sim g'$ が成り立ち、 $\sim$ が congruence であることより $f \sim g$ が成り立つ。
$(g,f) \in \Sigma'$ の場合も $(f,g) \in \Sigma'$ の場合と同様である。

$n \gt 1$ のとき

帰納法の仮定より $f \sim x_{n-1}$ が成り立つ。一方で $x_{n-1} = g$ 、 $(x_{n-1}, g) \in \Sigma'$ 、 $(g, x_{n-1}) \in \Sigma'$ のそれぞれの場合に対して、 $n = 1$ の場合と同様の議論により、 $x_{n-1} \sim g$ が成り立つ。よって $\sim$ の transitivity により $f \sim g$ が成り立つ。

$\square$

参考書籍

Category Theory (Oxford Logic Guides)

作者:Awodey, Steve
発売日: 2008/01/10
メディア: ペーパーバック

圏論原著第2版

作者:スティーブアウディ
発売日: 2015/09/19
メディア: 単行本

2016-03-31

二項関係から生成される同値関係に関する形式的な証明

数学

はじめに
二項関係から生成される関係
同値類
同値類と同値関係の性質

はじめに

数学の勉強をしていると、関係 $\sim$ を次の等式を含むような最小の同値関係とする、という定義がよく出てきます。
しかし、この定義は関係 $\sim$ の具体的な構成を与えていないので、この同値関係に関する証明をしようとすると途端に行き詰まってしまいます(例えば、商空間を定義域とするような関数が well-defined であることを証明する場合など)。
この記事では、二項関係から生成される同値関係を構成的に定義し、それが本当に最小の同値関係になっていることを証明します。
また同値類を定義し、同値類と同値関係に関して成り立つ基本的な事柄に関して補足します。

二項関係から生成される関係

$R$ を任意の集合 $X$ 上の二項関係であるとします。このとき、新しい $X$ 上の二項関係 $R'$ を次のように定義します。

\begin{align*}
\forall x,y \in X,\, (x,y) \in R' \iff &\exists n,\, \exists x_{0}, \dots , x_{n} \in X, \\
&x = x_{0} \\
&\land y = x_{n} \\
&\land \left( \forall 0 \leq i \leq n - 1,\, x_{i} = x_{i+1} \lor (x_{i}, x_{i+1}) \in R \lor (x_{i+1}, x_{i}) \in R \right)
\end{align*}

この $R'$ が $R$ を含むような最小の同値関係であることを示します。

$Lemma$
$R \subseteq R'$

$Proof.$
任意の $x,y \in X$ に対して、 $(x,y) \in R$ とすると、 $n = 1$ 、 $x = x_{0}$ 、 $y = x_{1}$ とすると、 $(x_{0}, x_{1}) \in R$ が成り立つので、 $(x,y) \in R'$ が成り立つ。

$\square$

$Lemma$
$R' \text{ is an equivalence relation}.$

$Proof.$

reflexive

任意の $x \in X$ に対して、 $n = 1$ 、 $x = x_{0}$ 、 $x = x_{1}$ とすれば、 $x_{0} = x_{1}$ が成り立つので、 $(x,x) \in R'$ が成り立つ。

symmetric

任意の $x,y \in X$ に対して、 $(x,y) \in R'$ とすると、 $\exists n,\ \exists x_{0}, \dots , x_{n}$ が存在して、 $x = x_{0}$ 、 $y = x_{n}$ 、 $\forall 0 \leq i \leq n-1,\, x_{i} = x_{i+1} \lor (x_{i}, x_{i+1}) \in R \lor (x_{i+1},x_{i}) \in R$ を満たす。このとき、 $x_{0}, \dots , x_{n}$ の順序を逆にした列 $x_{n}, \dots, x_{0}$ を新たに $x'_{0}, \dots x'_{n}$ とすると、これは $y = x'_{0}$ 、 $x = x'_{n}$ 、 $\forall 0 \leq i \leq n-1,\, x'_{i} = x'_{i+1} \lor (x'_{i}, x'_{i+1}) \in R \lor (x'_{i+1},x'_{i}) \in R$ を満たす。よって $(y,x) \in R'$ が成り立つ。

transitive

任意の $x,y,z \in X$ に対して、 $(x,y) \in R'$ 、 $(y,z) \in R'$ とすると、 $\exists n,\, \exists x_{0}, \dots ,x_{n}$ と $\exists n',\, \exists x'_{0}, \dots, x'_{n'}$ が存在して条件を満たす。このとき、列 $x_{0}, \dots, x_{n}, x'_{0}, \dots, x'_{n'}$ を新たに列 $x''_{0}, \dots , x''_{n + n' + 1}$ とすると、これは $x = x''_{0}$ 、 $z = x''_{n+n'+1}$ 、 $\forall 0 \leq i \leq n + n',\, x''_{i} = x''_{i+1} \lor (x''_{i}, x''_{i+1}) \in R \lor (x''_{i+1}, x''_{i}) \in R$ を満たす。よって $(x,z) \in R'$ が成り立つ。

$\square$

以上より、 $R'$ が $R$ を含む同値関係であることがわかりました。次に $R'$ が $R$ を含むような同値関係の中で最小であることを示します。

$Lemma$
$R' \text{ is the least equivalence relation containing } R.$

$Proof.$
任意の $R''$ を $R$ を含む同値関係であるとする。任意の $x,y \in X$ に対して、 $(x,y) \in R'$ とすると $\exists n,\, \exists x_{0}, \dots, x_{n}$ が存在して条件を満たす。このとき、 $n$ に関する帰納法により証明する。

$n = 1$ のとき

$x_{0} = x_{1}$ のときは $R''$ が同値関係であることより $(x,y) \in R''$ である。 $(x_{0},x_{1}) \in R \lor (x_{1}, x_{0}) \in R$ のときは、 $R''$ が $R$ を含むことより $(x,y) \in R''$ が成り立つ。

$n \gt 1$ のとき

帰納法の仮定より $(x_{0}, x_{n-1}) \in R''$ が成り立つ。 $n = 1$ のときと同様の議論により、 $(x_{n-1}, x_{n}) \in R''$ が成り立つ。よって $R''$ の transitivity により、 $(x,y) \in R''$ が成り立つ。

$\square$

同値類

集合 $X$ 上の任意の同値関係 $\sim$ が与えられているときに、任意の $x \in X$ に対して次にように定義される集合を $x$ の同値類と呼びます。
\begin{equation}
[x] = \left\{ y \in X \ \middle| \ x \sim y \right\}
\end{equation}
このとき、次の事柄が成り立ちます。

$Lemma$
$\forall x,x',y \in X,\, y \in [x$ \land y \in [x'] \Rightarrow [x] = [x'] ]

$Proof.$
$y \in [x]$ 、 $y \in [x']$ より $x \sim y$ 、 $x' \sim y$ が成り立つ。すると $\sim$ が同値関係であることから、 $x \sim x'$ が成り立つ。
すると任意の $z \in X$ に対して、 $z \in [x] \iff x \sim z \iff x' \sim z \iff z \in [x']$ が成り立つ。よって $[x] = [x']$ である。

$\square$

これは集合 $X$ が互いに素な同値類に分解されることを示しています。

同値類と同値関係の性質

最後に基本的な事柄を確認して終わりにします。これによって、同値関係にない要素は違う同値類に属することがわかります。

$Lemma$
$\forall x,y \in X,\, [x$ = [y] \iff x \sim y ]

$Proof.$

only if case

$y \in [y]$ であるから仮定より $y \in [x]$ が成り立つ。すると定義より $x \sim y$ が成り立つ。

if case

任意の $z \in X$ に対して、仮定と $\sim$ が同値関係であることより、 $z \in [x] \iff x \sim z \iff y \sim z \iff z \in [y]$ が成り立つ。よって $[x] = [y]$ である。

$\square$

2016-03-29

Steve Awodey の Category Theory を読む : Chapter 3

数学数学-圏論

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

3.2 Coproducts
3.4 Coequalizers
- Example 3.20
参考書籍

3.2 Coproducts

Example 3.5

$Lemma$
$M(A) + M(B) \cong M(A + B)$

$Proof.$
$i_{M(A)} \colon M(A) \to M(A + B)$ を $M(A)$ の UMP より $\left| i_{M(A)} \right| \circ \eta_{A} = \eta_{A+B} \circ i_{A}$ を満たすただ一つの arrow とする。同様に $i_{M(B)} \colon M(B) \to M(A+B)$ を定める。このとき、 $(M(A+B),i_{M(A)},i_{M(B)})$ が $M(A)$ 、 $M(B)$ の coproduct となることを示す。
任意の $N \in \bf{Mon}_{0}$ と任意の $f \colon M(A) \to N, g \colon M(B) \to N$ に対して、 $\left| f \right| \circ \eta_{A} \colon A \to \left| N \right|$ と $\left| g \right| \circ \eta_{B} \colon B \to \left| N \right|$ を考えると、 $A + B$ の UMP より $\exists !\, [\left| f \right| \circ \eta_{A}, \left| g \right| \circ \eta_{B}] \colon A + B \to \left| N \right|$ が存在する。すると $M(A+B)$ の UMP より $\exists !\, [f,g] \colon M(A+B) \to N$ が存在して、 $\left| [f,g] \right| \circ \eta_{A+B} = [\left| f \right| \circ \eta_{A}, \left| g \right| \circ \eta_{B}]$ を満たす。この $[ f,g ]$ に対して、

\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*}

が成り立つので、 $M(A)$ の UMP より $[f,g] \circ i_{M(A)} = f$ が成り立つ。同様に $[f,g] \circ i_{M(B)} = g$ が成り立つので、 $[f,g]$ は diagram を可換にする。
次に、任意の $h \colon M(A+B) \to N$ が 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*}

が成り立つ。同様に $\left| h \right| \circ \eta_{A+B} \circ i_{B} = \left| g \right| \circ \eta_{B}$ が成り立つので、 $A+B$ の UMP より、 $\left| h \right| \circ \eta_{A+B} = [\left| f \right| \circ \eta_{A}, \left| g \right| \circ \eta_{B}]$ である。よって $M(A+B)$ の UMP より $[f,g] = h$ が成り立つので、 $M(A+B)$ は $M(A)$ 、 $M(B)$ の coproduct である。

$\square$

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

Example 3.6

一般に $(X, \mathcal{O}(X) )$ 、 $(Y, \mathcal{O}(Y) )$ が位相空間のとき、 $X + Y$ の位相は $\mathcal{O}(X + Y) = \left\{ O_{X} + O_{Y} \,\middle| \, O_{X} \in \mathcal{O}(X),\, O_{Y} \in \mathcal{O}(Y) \right\}$ で定義されます。

$Lemma$
$(X + Y, \mathcal{O}(X + Y) ) \text{ is a coproduct of } (X, \mathcal{O}(X) ) \text{ and } (Y, \mathcal{O}(Y) ).$

$Proof.$
任意の $(Z, \mathcal{O}(X) )$ と任意の $f \colon X \to Z, g \colon Y \to Z$ に対して、 $[ f,g] \colon X + Y \to Z$ を Example 3.4 と同様に定義すると、可換性と唯一性は Example 3.4 で証明済みなので $[ f,g]$ が continuous であることを示せばよい。
任意の $O \in \mathcal{O}(Z)$ に対して、 ${[f,g ]}^{-1}(O) = f^{-1}(O) + g^{-1}(O)$ であるが、 $f$ 、 $g$ が continuous であることより、 $f^{-1}(O) \in \mathcal{O}(X)$ 、 $g^{-1}(O) \in \mathcal{O}(Y)$ が成り立つ。 $\mathcal{O}(X + Y)$ の定義より ${[f,g ]}^{-1}(O) \in \mathcal{O}(X + Y)$ となるから、 $[ f,g ]$ は continuous である。

$\square$

Example 3.9

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

$i_{A}$ 、 $i_{B}$ が homomorphism となることは明らかなので省略します。 $i_{A}(u_{A}) = [u_{A}]$ と $i_{B}(u_{B}) = [u_{B}]$ が $A + B$ において一致して、かつ $A + B$ の単位元になる必要があるので、4つの等式の上の二つを含む equivalence relation で割る必要があるということを確認してください。
ここでは、書籍にあるように $[f,g]([x \dots y]) = [f,g]'((x \dots y) )$ で定義される $[f,g]$ が well-defined であることを証明します。

$Lemma$
\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}

$Proof.$
4つの等式を表現する $M(\left| A \right| + \left| B \right|)$ 上の二項関係を $R$ とする。
先に参照した記事の内容より、 $[v] = [w] \iff v \sim w$ が成り立つ。よって $\exists n,\, \exists x_{0}, \dots ,x_{n}$ が存在して、 $x_{0} = v$ 、 $x_{n} = w$ かつ $\forall 0 \leq i \leq n-1,\, x_{i} = x_{i+1} \lor (x_{i},x_{i+1}) \in R \lor (x_{i+1},x_{i}) \in R$ が成り立つ。 $n$ に関する帰納法により示す。

$n = 1$ のとき

$v = w$ の場合は明らか。 $(v,w) \in R$ のとき、 $s, s'$ を $\left| A \right| + \left| B \right|$ 上の任意の word とすると、 $v = su_{A}s',\, w = ss'$ の場合を考える。このとき、

\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*}

が成り立つので、 $[f,g]([v]) = [f,g]([w])$ が成り立つ。 $v = su_{B}s',\, w = ss'$ の場合も同様である。
$v = saa's',\, w = s(a \cdot_{A} a')s'$ のとき、

\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*}

が成り立つので、 $[f,g]([v]) = [f,g]([w])$ が成り立つ。 $v = sbb's',\, w = s(b \cdot_{B} b')s'$ の場合も同様である。
$(w,v) \in R$ の場合も同様に成り立つ。

$n \gt 1$ のとき

帰納法の仮定より、 $[f,g]([x_{0}]) = [f,g]([x_{n-1}])$ が成り立つ。また $n = 1$ の場合と同様の議論により、 $[f,g]([x_{n-1}]) = [f,g]([x_{n}])$ が成り立つ。よって $[f,g]([v]) = [f,g]([w])$ が成り立つ。

$\square$

$[f,g]$ が homomorphism であることは $[f,g]'$ が homomorphism であることから明らかです。
また $\pi \colon M(\left| A \right| + \left| B \right|) \to M(\left| A \right| + \left| B \right|)\, / \sim$ を自然な homomorphism とすると、 $[f,g] \circ \pi = [f,g]'$ が成り立ちます。任意の $h \colon M(\left| A \right| + \left| B \right|)\, / \sim \to M$ が $h \circ \pi = [f,g]'$ を満たすなら $h = [f,g]$ が成り立つことも簡単に確かめられます。
最後に $[f,g]$ が $[f,g] \circ i_{A} = f$ 、 $[f,g] \circ i_{B} = g$ を満たすただ一つの arrow であることを証明します。

$Lemma$
\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}

$Proof.$
$h \circ \pi = [f,g]'$ を示せばよい。それには $M(\left| A \right| + \left| B \right|)$ の UMP より、 $\left| h \circ \pi \right| \circ \eta_{\left| A \right| + \left| B \right|} = \left[ \left| f \right|, \left| g \right| \right]$ を示せばよい。それには $\left| A \right| + \left| B \right|$ の UMP より、 $\left| h \circ \pi \right| \circ \eta_{\left| A \right| + \left| B \right|} \circ i_{\left| A \right|} = \left| f \right|$ かつ $\left| h \circ \pi \right| \circ \eta_{\left| A \right| + \left| B \right|} \circ i_{\left| B \right|} = \left| g\right|$ を示せばよい。
任意の $a \in A$ に対して、

\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*}

が成り立つ。同様に、 $\left| h \circ \pi \right| \circ \eta_{\left| A \right| + \left| B \right|} \circ i_{\left| B \right|} = \left| g\right|$ が成り立つので $h = [f,g]$ が成り立つ。

$\square$

Example 3.10

$Lemma$
$A + B \text{ is a coproduct of } A \text{ and } B.$

$Proof.$
任意の $X$ と任意の $f \colon A \to X, g \colon B \to X$ に対して、 $[f,g] \colon A + B \to X$ を $[f,g](a,b) = f(a) + g(b)$ で定義する。すると $([f,g] \circ i_{A})(a) = [f,g](a,0) = f(a)$ が成り立つ。同様に $[f,g] \circ i_{B} = g$ が成り立つので、 $[f,g]$ は diagram を可換にする。
一方、任意の $h \colon A + B \to X$ が diagram を可換にするとすると、任意の $(a,b) \in A + B$ に対して、 $h(a,b) = h((a,0) + (0,b) ) = (h \circ i_{A})(a) + (h \circ i_{B})(b) = f(a) + g(b) = [f,g](a,b)$ が成り立つ。よって $A + B$ は $A$ 、 $B$ の coproduct である。

$\square$

Proposition 3.11

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

3.4 Coequalizers

Example 3.20

集合圏 $Sets$ において任意の $f,g \colon A \rightrightarrows B$ に対して coequalizer を具体的に構成します。
$R$ を $R = \left\{ (f(a), g(a)) \, \middle| \, a \in A \right\}$ で定義される $B$ 上の二項関係とし、 $R'$ を $R$ から生成される equivalence relation とします。このとき、 $\pi \colon B \to B / R'$ を任意の $b \in B$ に対して $\pi(b) = [b]$ で定義します。

$Lemma$
$\pi \circ f = \pi \circ g$

$Proof.$
任意の $a \in A$ に対して、 $(\pi \circ f)(a) = [f(a)]$ 、 $(\pi \circ g)(a) = [g(a)]$ であるから、 $[f(a)] = [g(a)]$ つまり $(f(a),g(a)) \in R'$ を示せばよい。これは $R'$ の定義より、 $n = 1$ 、 $x_{0} = f(a)$ 、 $x_{1} = g(a)$ とすれば、 $(f(a), g(a)) \in R$ であるから $(f(a),g(a)) \in R'$ が成り立つ。

$\square$

次に任意の $h \colon B \to C$ が $h \circ f = h \circ g$ を満たすとき、 $\overline{h} \colon B / R' \to C$ を $\overline{h}([b]) = h(b)$ で定義します。このとき、 $\overline{h}$ が well-defined であることを証明します。
f:id:hitotakuchan:20160406180220p:plain:w400

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

$Proof.$
$[b] = [b']$ であるから $(b,b') \in R'$ である。よって $\exists n,\, \exists x_{0}, \dots ,x_{n}$ が存在して、 $x_{0} = b$ 、 $x_{n} = b'$ かつ $\forall 0 \leq i \leq n-1,\, x_{i} = x_{i+1} \lor (x_{i},x_{i+1}) \in R \lor (x_{i+1},x_{i}) \in R$ が成り立つ。 $n$ に関する帰納法により示す。

$n = 1$ のとき

$b = b'$ なら $\overline{h}([b]) = \overline{h}([b'])$ は明らかである。
$(b,b') \in R$ なら $\exists a \in A$ が存在して、 $b = f(a)$ かつ $b' = g(a)$ であるから、 $\overline{h}([b]) = h(b) = h(f(a)) = h(g(a)) = h(b') = \overline{h}([b'])$ が成り立つ。
$(b',b) \in R$ なら $\exists a \in A$ が存在して、 $b = g(a)$ かつ $b' = f(a)$ であるから、 $\overline{h}([b]) = h(b) = h(g(a)) = h(f(a)) = h(b') = \overline{h}([b'])$ が成り立つ。

$n \gt 1$ のとき

帰納法の仮定より $\overline{h}([b]) = \overline{h}([x_{n-1}])$ が成り立つ。 $(x_{n-1}, b')$ に対して、 $n = 1$ の場合と同様の議論により $\overline{h}([x_{n-1}]) = \overline{h}([b'])$ が成り立つ。よって $\overline{h}([b]) = \overline{h}([b'])$ が成り立つ。

$\square$

$\overline{h} \circ \pi = h$ が成り立つことは定義より明らかです。また $\pi$ が epic であるから、 $\overline{h}$ はただ一つに決まります。よって $(B/R', \pi)$ は $f,g$ の coequalizer になります。

参考書籍

Category Theory (Oxford Logic Guides)

作者:Awodey, Steve
発売日: 2008/01/10
メディア: ペーパーバック

圏論原著第2版

作者:スティーブアウディ
発売日: 2015/09/19
メディア: 単行本

2016-03-22

Steve Awodey の Category Theory を読む : Chapter 2

数学数学-圏論

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

2.1 Epis and monos
2.3 Generalized elements
- ultrafilter に関する lemma
- Example 2.12
2.5 Examples of products
- 3
2.6 Categories with products
- is a functor
- product of -indexed family of object
参考書籍

2.1 Epis and monos

Example 2.4

poset category $P$ において、任意の $p,q \in P_{0}$ 間の arrow は $p \leq q$ ならばただ一つ存在すると定義されました。

$Lemma$
$\forall f \colon p \to q,\ f \text{ is both monic and epic.}$

$Proof.$

$f$ が monic であること。

任意の $g,h \colon r \to p$ に対して、 $f \circ g = f \circ h \Rightarrow g = h$ を示せば良いが、 $r$ から $p$ への arrow は定義よりただ一つに決まるので、 $g = h$ が成り立つ。よって $f$ は monic である。

$f$ が epic であること。

任意の $g, h \colon q \to s$ に対して、 $g \circ f = h \circ f \Rightarrow g = h$ を示せば良いが、 $q$ から $s$ への arrow は定義よりただ一つに決まるので、 $g = h$ が成り立つ。よって $f$ は epic である。

$\square$

a function is epic iff surjective in $Sets$

$Lemma$
$\forall A,B \in Sets_{0},\ \forall f \colon A \to B,\ f \text{ is epic} \Rightarrow f \text{ is surjective.}$

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

$\square$

$Lemma$
$\forall A,B \in Sets_{0},\ \forall f \colon A \to B,\ f \text{ is surjective} \Rightarrow f \text{ is epic.}$

$Proof.$
任意の $C \in Sets_{0}$ と任意の $g,h \colon B \to C$ に対して、 $g \circ f = h \circ f \Rightarrow g = h$ を示せばよい。そのためには、任意の $b \in B$ に対して、 $g(b) = h(b)$ を示せばよい。 $f$ が surjective であることより、 $\exists a,\ f(a) = b$ が成り立つので、 $g(b) = g(f(a)) = (g \circ f)(a) = (h \circ f)(a) = h(f(a)) = h(b)$ が成り立つ。よって $f$ は epic である。

$\square$

any epi into a projective object splits

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

$Lemma$
$\forall e \colon E \to P,\ e \text{ is epic} \Rightarrow e \text{ splits.}$

$Proof.$
$1_{P}$ と $e$ に対して、 $P$ が projective であることより、 $\exists \bar{1_{P}} \colon P \to E$ が存在して $e \circ \bar{1_{P}} = 1_{P}$ が成り立つ。よって $e$ は split epi である。

$\square$

any retract of a projective object is projective

$Lemma$
$\forall X' \in {\bf{C}}_{0},\ X' \text{is a restract of } P \Rightarrow X' \text{ is projective.}$

$Proof.$
任意の epic $e \colon E \to X$ と任意の $f \colon X' \to X$ に対して、 $\exists \bar{f} \colon X' \to E,\ e \circ \bar{f} = f$ を示す。 $X'$ が $P$ の rectact であることより、 $\exists s \colon X' \to P,\ r \colon P \to X',\ r \circ s = 1_{X'}$ が成り立つ。一方、 $P$ が projective であることより $(f \circ r) \colon P \to X$ と $e$ に対して、 $\exists \overline{f \circ r}$ が存在して、 $e \circ \overline{f \circ r} = f \circ r$ が成り立つ。 $\bar{f}$ を $\bar{f} = \overline{f \circ r} \circ s$ で定義すると、 $e \circ \overline{f \circ r} \circ s = f \circ r \circ s = f \circ 1_{X'} = f$ が成り立つ。よって $X'$ は projective である。

$\square$

2.3 Generalized elements

ultrafilter $F$ に関する lemma

$Lemma$
$F \text{ is an ultrafilter} \iff \forall b \in B,\ (b \in F \land \lnot b \notin F) \lor (b \notin F \land \lnot b \in F)$

$Proof.$

only if case

任意の $b$ に対して、 $b \in F$ とする。 $\lnot b \in F$ とすると、 $F$ が filter であることより、 $0 = b \land \lnot b \in F$ が成り立つ。よって $F = B$ となるが、これは $F$ が ultrafilter であることと矛盾する。
次に $b \notin F$ とする。このとき、 $\lnot b \in F$ であることを背理示す。
$\lnot b \notin F$ であるとする。集合 $F \cup \{b\}$ を考え、この集合から filter $F'$ を構成する。このとき $F \subsetneq F'$ が成り立つ。 $\lnot b \in F'$ であるとすると、 $\exists a \in F,\ a \land b \leq \lnot b$ が成り立つ。つまり、 $a \land b = 0$ が成り立つ。よって $a \leq \lnot b$ が成り立つが、 $F$ が filter であることより $\lnot b \in F$ が成り立ち、これは $\lnot b \notin F$ と矛盾する。よって $\lnot b \notin F'$ が成り立ち、 $F \subsetneq F' \subsetneq B$ が成り立つ。これは $F$ が maximal であることと矛盾する。よって $\lnot b \in F$ が成り立つ。

if case

$F$ が仮定を満たすような filter であるとき、 $\forall F',\ F' \text{ is a filter} \land F \subsetneq F' \Rightarrow F' = B$ を示す。
$F \subsetneq F'$ より、 $\exists b' \in F',\ b' \notin F$ が存在する。すると $F$ の仮定より、 $\lnot b' \in F$ が成り立つ。 $F \subsetneq F'$ より $\lnot b' \in F'$ であるから、 $b' \in F' \land \lnot b' \in F'$ が成り立つ。 $F'$ が filter であることより、 $0 = b' \land \lnot b' \in F'$ である。よって $F' = B$ となるので、 $F$ は maximal filter である。

$\square$

Example 2.12

$Lemma$
$\forall f,g \colon C \to D,\ f = g \iff \forall x \colon X \to C,\ f \circ x = g \circ x$

$Proof.$

only if case

$f = g$ より $f \circ x = g \circ x$ は明らかに成り立つ。

if case

仮定が成り立つとすると、 $x$ として $1_{C}$ を取ると $f = f \circ 1_{C} = g \circ 1_{C} = g$ が成り立つ。

$\square$

2.5 Examples of products

3

$\bf{Cat}$ において、任意の圏 $\bf{C}, \bf{D}$ の product $\bf{C} \times \bf{D}$ が存在することを示します。証明することがたくさんあるので一つずつ確認していきましょう。

$\bf{C} \times \bf{D}$ が圏であること

$Lemma$
${\bf{C}} \times {\bf{D}} \text{ is a category.}$

$Proof.$
$({\bf{C}} \times {\bf{D}})_{0} = \left\{ (c,d)\ \middle| \ c \in {\bf{C}}_{0},\,d \in {\bf{D}}_{0} \right\}$ 、 $\text{Hom}_{\bf{C} \times \bf{D}}((c,d),(c',d') ) = \left\{ (f,g)\ \middle| \ f \in \text{Hom}_{\bf{C}}(c,c'),\, g \in \text{Hom}_{\bf{D}}(d,d') \right\}$ 、 $(f', g') \circ_{\bf{C} \times \bf{D}} (f,g) = (f' \circ_{\bf{C}} f, g' \circ_{\bf{D}} g)$ 、 $1_{(c,d)} = (1_{c}, 1_{d})$ で ${\bf{C}} \times {\bf{D}}$ を定義する。
すると圏 $\bf{C}, \bf{D}$ の性質より、 $\circ_{\bf{C} \times \bf{D}}$ と $1_{(c,d)}$ が associativity と unit low を満たすことは明らかである。よって $\bf{C} \times \bf{D}$ は圏となる。

$\square$

$\pi_{1}, \pi_{2}$ が functor であること

$Lemma$
$\pi_{1} \colon {\bf{C} \times \bf{D}} \to {\bf{C}}, \pi_{2} \colon {\bf{C} \times \bf{D}} \to {\bf{D}} \text{ are functors.}$

$Proof.$
$\pi_{1}$ を任意の $(c,d) \in ({\bf{C} \times \bf{D}}_{0})$ と任意の $(f,g) \colon (c,d) \to (c',d')$ に対して、 $\pi_{1_{0}}((c,d) ) = c$ 、 $\pi_{1_{1}}((f,g) ) = f$ で定義する。
すると、 $\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) を満たす。
任意の $(f',g') \colon (c',d') \to (c'',d'')$ に対して、 $\pi_{1_{1}}((f',g') \circ_{\bf{C} \times \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) を満たす。よって $\pi_{1}$ は functor である。
$\pi_{2}$ に関しても同様である。

$\square$

$\bf{C} \times \bf{D}$ が product であること

$Lemma$
${\bf{C} \times \bf{D}} \text{ is a product of } {\bf{C}} \text{ and } {\bf{D}}.$

$Proof.$
任意の $\bf{X}$ と、任意の $F \colon {\bf{X}} \to {\bf{C}},G \colon {\bf{X}} \to {\bf{D}}$ に対して、 $\left< F,G \right> \colon {\bf{X}} \to {\bf{C} \times \bf{D}}$ を $\left< F,G \right>_{0}(x) = (F_{0}(x), G_{0}(x) )$ 、 $\left< F,G \right>_{1}(f) = (F_{1}(f), G_{1}(f) )$ で定義する。
すると、

\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*}

が成り立つので、 $\left< F,G \right>$ は functor の条件 (a) を満たす。
$\left< F,G \right>_{1}(1_{x}) = (F_{1}(1_{x}), G_{1}(1_{x}) ) = (1_{F_{0}(x)}, 1_{G_{0}(x)}) = 1_{\left< F,G \right>_{0}(x)}$ が成り立つので、 $\left< F,G \right>$ は functor の条件 (b) を満たす。
任意の $f \colon x \to x', f' \colon x' \to x''$ に対して、

\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*}

が成り立つので、 $\left< F,G \right>$ は functor の条件 (c) を満たす。よって $\left< F,G \right>$ は functor である。
このとき、 $\pi_{1_{0}} \circ \left< F,G \right>_{0} = F_{0},\ \pi_{1_{1}} \circ \left< F,G \right>_{1} = F_{1}$ と $\pi_{2_{0}} \circ \left< F,G \right>_{0} = G_{0},\ \pi_{2_{1}} \circ \left< F,G \right>_{1} = G_{1}$ が成り立つので、diagram は可換となる。
また、任意の $H \colon X \to {\bf{C} \times \bf{D}}$ に対して、 $H$ が diagram を可換とするなら、 $H_{0}(x) = (F_{0}(x), G_{0}(x) )$ 、 $H_{1}(f) = (F_{1}(f), G_{1}(f) )$ が成り立つ。よって、 $H = \left< F,G \right>$ となり diagram を可換とする functor はただ一つに決まる。
以上より、 $\bf{C} \times \bf{D}$ は $\bf{C}$ と $\bf{D}$ の product である。

$\square$

product of posets constructed in $\bf{Cat}$

$\bf{Pos}$ の要素である poset それ自体を圏としてみた場合、poset 間の写像が functor であることと、monotone function であることは同一視できるのでした。よってここで確認するべきことは、先の product の定義が poset になるかどうかということです。
任意の poset $P$ 、 $Q$ に対して、 $P \times Q$ は $(P \times Q)_{0} = \left\{ (p,q)\ \middle| \ p \in P,\, q \in Q \right\}$ 、 $\text{Hom}_{P \times Q}((p,q), (p',q') ) = \left\{ (f,g)\ \middle| \ f \in \text{Hom}_{P}(p,p'),\, q \in \text{Hom}_{Q}(q,q') \right\}$ で定義される。一方、Hom の定義は $(p,p') \leq (q,q') \iff p \leq p' \land q \leq q'$ と同値です。
このように $P \times Q$ に順序を入れた時に、 $P \times Q$ が poset となることは $P$ 、 $Q$ がそれぞれ poset であることより明らかです。
よって、 $\bf{Cat}$ において構成した product が $\bf{Pos}$ において product になることが確認できました。
$\bf{Mon}$ の場合も同様です。

2.6 Categories with products

$\times \colon \bf{C} \times \bf{C} \to \bf{C}$ is a functor

$Lemma$
$\times \colon {\bf{C}} \times {\bf{C}} \to {\bf{C}} \text{ is a functor.}$

$Proof.$
任意の product $(A \times A', p_{1}, p_{2}),\,(B \times B', q_{1}, q_{2})$ と任意の $f \colon A \to B, f' \colon A' \to B'$ に対して、 $\times \colon \bf{C} \times \bf{C} \to \bf{C}$ を $\times_{0}((A,A') ) = A \times A'$ 、 $\times_{1}((f, f') ) = f \times f'$ で定義する。
$\times_{1}((f,f') \colon (A,A') \to (B,B') ) = f \times f' \colon A \times A' \to B \times B' = f \times f' \colon \times_{0}((A,A') ) \to \times_{0}((B,B') )$ が成り立つので、 $\times$ は functor の条件 (a) を満たす。
次に、 $\times_{1}((1_{A},1_{A'}) ) = 1_{A} \times 1_{A'}$ であるが、これは定義より $p_{1} \circ (1_{A} \times 1_{A'}) = 1_{A} \circ p_{1}$ 、 $p_{2} \circ (1_{A} \times 1_{A'}) = 1_{A'} \circ p_{2}$ を満たす。一方で $1_{A \times A'}$ も $p_{1} \circ 1_{A \times A'} = 1_{A} \circ p_{1}$ 、 $p_{2} \circ 1_{A \times A'} = 1_{A'} \circ p_{2}$ を満たす。よって、 $A \times A'$ の UMP より、 $1_{A} \times 1_{A'} = 1_{A \times A'}$ が成り立つので、 $\times$ は functor の条件 (b) を満たす。
最後に、任意の product $(C \times C', r_{1}, r_{2})$ と $g \colon B \to C, g' \colon B' \to C'$ に対して、 $\times_{1}((g,g') \circ (f,f') ) = \times_{1}((g \circ f, g' \circ f') ) = (g \circ f) \times (g' \circ f')$ である。これは、定義より $r_{1} \circ ((g \circ f) \times (g' \circ f') ) = g \circ f \circ p_{1}$ 、 $r_{2} \circ ((g \circ f) \times (g' \circ f') ) = g' \circ f' \circ p_{2}$ を満たす。
一方で、 $(g \times g') \circ (f \times f')$ に対して、

\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*}

が成り立ち、同様に $r_{2} \circ ((g \times g') \circ (f \times f') ) = g' \circ f' \circ p_{2}$ が成り立つ。よって $C \times C'$ の UMP より $(g \circ f) \times (g' \circ f') = (g \times g') \circ (f \times f') = \times_{1}((g,g') ) \circ \times_{1}((f,f') )$ が成り立つ。よって $\times$ は functor の条件 (c) を満たす。

$\square$

product of $I$ -indexed family of object $(X_{i})_{i \in I}$

$\prod_{i \in I} X_{i}$ と $(\pi_{i} \colon \prod_{i \in I} X_{i} \to X_{i})_{i \in I}$ の組み $(\prod_{i \in I} X _{i}, (\pi_{i})_{i \in I})$ が $(X_{i})_{i \in I}$ の product であるとは、任意の $Y$ と任意の $(f_{i} \colon Y \to X_{i})_{i \in I}$ に対して、ただ一つの $f \colon Y \to \prod_{i \in I} X_{i}$ が存在して、任意の $i \in I$ に対して、 $\pi_{i} \circ f = f_{i}$ が成り立つこととして定義されます。

参考書籍

Category Theory (Oxford Logic Guides)

作者:Awodey, Steve
発売日: 2008/01/10
メディア: ペーパーバック

圏論原著第2版

作者:スティーブアウディ
発売日: 2015/09/19
メディア: 単行本

2016-03-07

Steve Awodey の Category Theory を読む : Chapter 1

数学数学-圏論

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

はじめに
1.2 Functions of sets
1.4 Examples of categories
1.5 Isomorphisms
1.6 Constructions on categories
1.7 Free categories
おわりに
参考書籍

はじめに

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

本文では $f \colon A \to B$ , $g \colon B \to C$ の二つの関数の合成 $g \circ f \colon A \to C$ を以下のように定義してます。
\begin{equation}
(g \circ f)(a) = g(f(a)) \qquad a \in A
\end{equation}
この時実際に $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))$ への連続写像であるとは、
\begin{equation}
\forall O \in \mathcal{O}(B),\ f^{-1}(O) \in \mathcal{O}(A)
\end{equation}
が成り立つということです。
位相空間の関数の合成と $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$ の要素間の関係です。
\begin{equation}
\forall a,b \in P,\ a \to b \text{ if and only if } a \leq b
\end{equation}
圏 $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}$ 空間であるとは以下の論理式が成り立つことです。
\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 によって $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}$ 空間であるとは以下の論理式が成り立つことです。
\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 であることを示します。

$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 を以下のように定義します。
\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 は $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 であるとは、
\begin{equation}
\forall b \in B,\ \exists a \in A,\ f(a) = b
\end{equation}
が成り立つこととして定義されます。

$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}$ を定義しています。よって証明するべきことを論理式として表現すると以下のようになります。
\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}
書籍にあるように定義された $\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

証明するべきことを論理式で表現すると次のようになります。
\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 に存在するということを $\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)

作者:Awodey, Steve
発売日: 2008/01/10
メディア: ペーパーバック

圏論原著第2版

作者:スティーブアウディ
発売日: 2015/09/19
メディア: 単行本

2016-03-04

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

Coq

はじめに
length関数を実装する
map関数(Ltac引数)を実装する
map関数(Gallina引数)を実装する
最後に
参考書籍

はじめに

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

作者: Adam Chlipala
出版社/メーカー: The MIT Press
発売日: 2013/12/06
メディア: ハードカバー
この商品を含むブログを見る

5.2 Pullbacks

Proposition 5.5

Exercise 3

5.3 Properties of pullbacks

Two pullbacks lemma

Proposition 5.10

Example 5.13

5.4 Limits

Proposition 5.14

5.6 Colimits

Direct limits of groups

参考書籍

4.1 Groups in a category

Corollary 4.6

4.2 The category of groups

is an equivalence relation

Corollary 4.11

Cokernels are special coequalizers

4.3 Groups as categories

composition of the congruence category is well-defined

is a congruence

Theorem 4.13

4.4 Finitely presented categories

smallest congruence

参考書籍

はじめに

二項関係から生成される関係

同値類

同値類と同値関係の性質

3.2 Coproducts

Example 3.5

Example 3.6

Example 3.9

Example 3.10

Proposition 3.11

3.4 Coequalizers

Example 3.20

参考書籍

2.1 Epis and monos

Example 2.4

a function is epic iff surjective in

any epi into a projective object splits

any retract of a projective object is projective

2.3 Generalized elements

ultrafilter に関する lemma

Example 2.12

2.5 Examples of products

3

が圏であること

が functor であること

が product であること

product of posets constructed in

2.6 Categories with products

is a functor

product of -indexed family of object

参考書籍

はじめに

1.2 Functions of sets

1.4 Examples of categories

圏

Definition 1.2

poset category

が poset であること

Functor は monotone function

monotone function は Functor

an example from topology

specialization は preorder

が 空間の場合

が 空間の場合

discrete category は poset

1.5 Isomorphisms

inverses are unique

において が closed であること

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

Cayley の定理

Cayley の定理(圏)

1.6 Constructions on categories

product

dual category

arrow category

$\sim$ is an equivalence relation

$\sim_{F}$ is a congruence

a function is epic iff surjective in $Sets$

ultrafilter $F$ に関する lemma

$\bf{C} \times \bf{D}$ が圏であること

$\pi_{1}, \pi_{2}$ が functor であること

$\bf{C} \times \bf{D}$ が product であること

product of posets constructed in $\bf{Cat}$

$\times \colon \bf{C} \times \bf{C} \to \bf{C}$ is a functor

product of $I$ -indexed family of object $(X_{i})_{i \in I}$

圏 $\bf{3}$

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

$X$ が $T_{1}$ 空間の場合

$X$ が $T_{0}$ 空間の場合

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

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