エレファント・ビジュアライザー調査記録

ビジュアルプログラミングで数式の変形を表すことを考えていくブロクです。

エレファントな群とリー代数(2)

モノイドの左逆元・右逆元

 (M, \cdot, e) をモノイド( e単位元)とします。

  • (L)  x \in M に対して、 x_L \cdot x = e であるような  x_L x の左逆元と呼びます。
  • (R)  x \in M に対して、  x \cdot x_R = e であるような  x_R x の右逆元と呼びます。

 x \in M が左逆元  x_L と右逆元  x_R を持つならば、 x_L = x_R となります。
[証明]
(L)より  (x_L \cdot x) \cdot x_R = e \cdot x_R = x_R
(R)より  x_L \cdot (x \cdot x_R) = x_L \cdot e = x_L
よって結合法則より  x_R = e \cdot x_R = (x_L \cdot x) \cdot x_R = x_L \cdot (x \cdot x_R) = x_L \cdot e = x_L
[証明終わり]

これも「マグマの左単位元・右単位元」と同様に変形していくことができます。 M \{x, x_L, x_R, e\} で生成された自由マグマとします。書き換え規則は \begin{cases}
\rho_{1} & = & ( & x, y, z & \mapsto & (x \cdot y) \cdot z & \to & x \cdot (y \cdot z) & ) \\
\rho_{2} & = & ( & x, y, z & \mapsto & x \cdot (y \cdot z) & \to & (x \cdot y) \cdot z & ) \\
\rho_{3} & = & ( & x & \mapsto & e \cdot x & \to & x & ) \\
\rho_{4} & = & ( & x & \mapsto & x & \to & e \cdot x & ) \\
\rho_{5} & = & ( & x & \mapsto & x \cdot e & \to & x & ) \\
\rho_{6} & = & ( & x & \mapsto & x & \to & x \cdot e & ) \\
\rho_{7} & = & ( & & \mapsto & x_L \cdot x & \to & e & ) \\
\rho_{8} & = & ( & & \mapsto & e & \to & x_L \cdot x & ) \\
\rho_{9} & = & ( & & \mapsto & x \cdot x_R & \to & e & ) \\
\rho_{10} & = & ( & & \mapsto & e & \to & x \cdot x_R & ) \\
\end{cases} となります。2段階まで変形を行った結果は \begin{cases}
x_L & \xrightarrow{\rho_{4}} & e \cdot x_L & \xrightarrow{\rho_{3}} & x_L \\
x_L & \xrightarrow{\rho_{4}} & e \cdot x_L & \xrightarrow{\rho_{4}} & e \cdot (e \cdot x_L) \\
x_L & \xrightarrow{\rho_{4}} & e \cdot x_L & \xrightarrow{\rho_{4}} & (e \cdot e) \cdot x_L \\
x_L & \xrightarrow{\rho_{4}} & e \cdot x_L & \xrightarrow{\rho_{4}} & e \cdot (e \cdot x_L) \\
x_L & \xrightarrow{\rho_{6}} & x_L \cdot e & \xrightarrow{\rho_{4}} & e \cdot (x_L \cdot e) \\
x_L & \xrightarrow{\rho_{6}} & x_L \cdot e & \xrightarrow{\rho_{4}} & (e \cdot x_L) \cdot e \\
x_L & \xrightarrow{\rho_{6}} & x_L \cdot e & \xrightarrow{\rho_{4}} & x_L \cdot (e \cdot e) \\
x_L & \xrightarrow{\rho_{6}} & x_L \cdot e & \xrightarrow{\rho_{5}} & x_L \\
x_L & \xrightarrow{\rho_{4}} & e \cdot x_L & \xrightarrow{\rho_{6}} & (e \cdot x_L) \cdot e \\
x_L & \xrightarrow{\rho_{4}} & e \cdot x_L & \xrightarrow{\rho_{6}} & (e \cdot e) \cdot x_L \\
x_L & \xrightarrow{\rho_{4}} & e \cdot x_L & \xrightarrow{\rho_{6}} & e \cdot (x_L \cdot e) \\
x_L & \xrightarrow{\rho_{6}} & x_L \cdot e & \xrightarrow{\rho_{6}} & (x_L \cdot e) \cdot e \\
x_L & \xrightarrow{\rho_{6}} & x_L \cdot e & \xrightarrow{\rho_{6}} & (x_L \cdot e) \cdot e \\
x_L & \xrightarrow{\rho_{6}} & x_L \cdot e & \xrightarrow{\rho_{6}} & x_L \cdot (e \cdot e) \\
x_L & \xrightarrow{\rho_{4}} & e \cdot x_L & \xrightarrow{\rho_{8}} & (x_L \cdot x) \cdot x_L \\
x_L & \xrightarrow{\rho_{6}} & x_L \cdot e & \xrightarrow{\rho_{8}} & x_L \cdot (x_L \cdot x) \\
x_L & \xrightarrow{\rho_{4}} & e \cdot x_L & \xrightarrow{\rho_{10}} & (x \cdot x_R) \cdot x_L \\
x_L & \xrightarrow{\rho_{6}} & x_L \cdot e & \xrightarrow{\rho_{10}} & x_L \cdot (x \cdot x_R) \\
\end{cases} となります。多すぎるので、5段階まで変形を行った結果を一つだけ書くと \begin{matrix}
x_L & \xrightarrow{\rho_{6}} & x_L \cdot e & \xrightarrow{\rho_{10}} & x_L \cdot (x \cdot x_R) & \xrightarrow{\rho_{2}} & (x_L \cdot x) \cdot x_R & \xrightarrow{\rho_{7}} & e \cdot x_R & \xrightarrow{\rho_{3}} & x_R \\
\end{matrix} となって、上記の証明の結果が得られます。このとき \begin{cases}
X_1 = \{x_1\}, & σ_1 : X_1 \to M[X_1], & σ_1(x_1) = x_L ; \\
X_2 = \{ \} ; \\
X_3 = \{x_3, y_3, z_3\}, & σ_3 : X_3 \to M[X_1][X_3], & σ_3(x_3) = x_L, σ_3(y_3) = x, σ_3(z_3) = x_R ; \\
X_4 = \{ \} ; \\
X_5 = \{x_5\}, & σ_5 : X_5 \to M[X_1][X_3][X_5], & σ_5(x_5) = x_R ; \\
\end{cases} となっています。これらをまとめると \begin{cases}
X = \{x_1, x_3, y_3, z_3, x_5\}, \\
σ : X \to M[X], \\
σ(x_1) = x_L, \\
σ(x_3) = x_L, \\
σ(y_3) = x, \\
σ(z_3) = x_R, \\
σ(x_5) = x_R \\
\end{cases} となります。 x_L と書き換え規則を組み合わせて写像にしたものを  f(x_1, x_3, y_3, z_3, x_5) とすると、 f(x_L, x_L, x, x_R, x_R) = x_R となります。

エレファントな群とリー代数(1)

ここでは「項書き換え」のような方法で群、モノイド、半環やリー代数に関する証明を行ってみます。「項書き換え」については[1][2]の本を持っていたのですが見当たらないので、ウェブに同様の記事があったのでそれを参考にします。本来の「項書き換え」では数式を一方向に変換して標準形にするというもののようですが、ここでは変形できるすべてのものに変形するという方法でやっていきます。

マグマの左単位元・右単位元

 (M, \cdot) をマグマとします。

  • (L) 任意の  x \in M に対して  e_L \cdot x = x であるとき、 e_L M の左単位元と呼びます。
  • (R) 任意の  x \in M に対して  x \cdot e_R = x であるとき、 e_R M の右単位元と呼びます。

 M が左単位元  e_L と右単位元  e_R を持つならば、 e_L = e_R となります。
[証明]
(1) (L)より  e_L \cdot e_R = e_R
(2) (R)より  e_L \cdot e_R = e_L
(1)、(2)より  e_R = e_L \cdot e_R = e_L
[証明終わり]

この証明を「項書き換え」のような形に書き直します。

自由マグマによる「多項式」の定義

 (M, \cdot) をマグマ、 X を集合とします。集合としての直和  M + X で生成された自由マグマを  (F(M + X), *) とします。 F(M + X) に演算  \circledast を \begin{cases}
\alpha \circledast \beta = \alpha \cdot \beta & (\alpha, \beta \in M \ のとき) \\
\alpha \circledast \beta = \alpha * \beta & (それ以外のとき) \\
\end{cases} と定義します。 (F(M + X), *) が自由マグマであることから  M + X 上では恒等写像であるようなマグマの準同型
 f: (F(M + X), *) \to (F(M + X), \circledast) が一意的に存在します。 f による  F(M + X) の像を  M[X] とおきます。

 (F(M + X), *) の台集合  F(M + X) の部分集合  A に対して \begin{cases}
A^{(*)(1)} = A \\
A^{(*)(n+1)} = A^{(*)(n)} * A^{(*)(n)} \\
\end{cases} と帰納的に  A^{(*)(n)} を定義します。

 (F(M + X), *) が自由マグマであることから  \displaystyle F(M + X) = \bigcup_{n \in \mathbb{N}} (M \cup X)^{(*)(n)} が成り立ちます。

 M[X] の演算を  \star と書くことにします。 (M[X], \star) の台集合  M[X] の部分集合  B に対して \begin{cases}
B^{(\star)(1)} = B \\
B^{(\star)(n+1)} = B^{(\star)(n)} \star B^{(\star)(n)} \\
\end{cases} と帰納的に  B^{(\star)(n)} を定義します。

 f: F(M + X) \to M[X] を上で述べた全射のマグマの準同型とすると、\begin{eqnarray*}
f(F(M + X)) & = & f(\bigcup_{n \in \mathbb{N}} (M \cup X)^{(*)(n)}) \\
& = & \bigcup_{n \in \mathbb{N}} f( (M \cup X)^{(*)(n)}) \\
& = & \bigcup_{n \in \mathbb{N}} f(M \cup X)^{(\star)(n)} \\
& = & \bigcup_{n \in \mathbb{N}} (f(M) \cup f(X))^{(\star)(n)} \\
\end{eqnarray*} となります。 f M への制限、 f X への制限は単射となるので、 M \subseteq M[X] X \subseteq M[X] とみなすことができて、 \displaystyle M[X] = \bigcup_{n \in \mathbb{N}} (M \cup X)^{(\star)(n)} となります。

 (M', \odot) をマグマ、 g: M + X \to M'単射 g M への制限がマグマの準同型であるとします。 \alpha \in M[X] に対して  \displaystyle n_\alpha = \min \{ n \in \mathbb{N} \mid \alpha \in \bigcup_{k \le n} (M \cup X)^{(\star)(k)} \} が存在します。 \alpha \in M \cup X または  \alpha = \beta \star \gamma となる  \displaystyle \beta, \gamma \in \bigcup_{k \le n_\alpha-1} (M \cup X)^{(\star)(k)} が存在します。\begin{cases}
g^*(\alpha) = g(\alpha) & (\alpha \in M \cup X \ のとき) \\
g^*(\alpha) = g^*(\beta) \odot g^*(\gamma) & (それ以外のとき) \\
\end{cases} と帰納的に定義することにより、マグマの準同型  g^*: M[X] \to M' を定義することができます。

  •  M[X] はマグマ
  • 単射  i: M + X \to M[X] が存在し
  •  i M への制限はマグマの準同型で、
  •  M' がマグマ、単射  g: M + X \to M' が存在し、 g M への制限がマグマの準同型ならば、マグマの準同型  g^*: M[X] \to M' が存在します。

多項式」への代入

 \sigma: X \to M[X] とすると、上の議論により、 \sigma を拡張した  M を保存するマグマの準同型  \sigma^*: M[X] \to M[X] が一意的に存在します。

 \alpha \in M[X] に対して  \alpha[\sigma] = \sigma^*(\alpha) と定義します。 X = \{x_1, x_2, \cdots, x_n\} のとき  \alpha[\sigma] \alpha[\sigma(x_1), \sigma(x_2), \cdots, \sigma(x_n)] と書くことにします。これを  \alpha X \sigma を代入する、または  x_1, x_2, \cdots, x_n \sigma(x_1), \sigma(x_2), \cdots, \sigma(x_n) を代入するということにします。 \sigma を代入写像と呼ぶことにします。

 (X \mapsto \alpha): M[X]^X \to M[X] \sigma: X \to M[X] \alpha[\sigma] に写す写像とします。 X = \{x_1, x_2, \cdots, x_n\} のとき  (x_1, x_2, \cdots, x_n \mapsto \alpha): M[X]^n \to M[X] \langle \sigma(x_1), \sigma(x_2), \cdots, \sigma(x_n) \rangle \in M[X]^n \alpha[\sigma(x_1), \sigma(x_2), \cdots, \sigma(x_n)] に写す写像とします。これは  \langle a_1,a_2, \cdots, a_n \rangle \in M[X]^n \alpha[a_1, a_2, \cdots, a_n] に写す写像となります。これらを  \alpha の「ラムダ式化」と呼ぶことにします。

部分項の位置

 \alpha \in M[X] \setminus (M \cup X) に対して、 \alpha = \alpha_L \cdot \alpha_R となる  \alpha_L, \alpha_R が一意的に存在します(演算を  \cdot と書きます)。 \alpha \alpha_L に写す写像 L: M[X] \setminus (M \cup X) \to M[X] \alpha \alpha_R に写す写像 R: M[X] \setminus (M \cup X) \to M[X] と定義することができます。 \alpha \in M \cup X のときは  M[X] に含まれない元  \bot (失敗を表す)を追加した  M[X] + \{\bot\} を考え、 L(\alpha) = R(\alpha) = \bot と定義することによってこれらを拡張して、 L, R: M[X] \to M[X] + \{\bot\} とします。さらに  L(\bot) = R(\bot) = \bot と定義することによって拡張して、 L, R: M[X] + \{\bot\} \to M[X] + \{\bot\} とします。

 L(\alpha) \alpha L R(\alpha) \alpha R と書くことにすると \begin{cases}
α L = α_L & (α \in M[X] \setminus (M \cup X)) \\
α L = ⊥ & (α \in (M \cup X) \\
⊥ L = ⊥
\end{cases} \begin{cases}
α R = α_L & (α \in M[X] \setminus (M \cup X)) \\
α R = ⊥ & (α \in (M \cup X) \\
⊥ R = ⊥
\end{cases} となります。

 \delta_i L または  R としたとき、すべての自然数  n に対する  \alpha \delta_1 \delta_2 \cdots \delta_n 全体の集合  T_\alpha を考えます。

 \displaystyle M[X] = \bigcup_{n \in \mathbb{N}} (M \cup X)^{(\cdot)(n)} であることから  \displaystyle n_\alpha = \min \{ n \in \mathbb{N} \mid \alpha \in \bigcup_{k \le n} (M \cup X)^{(\cdot)(k)} \} が存在するので、すべての  0 \le n \le n_\alpha に対する  \alpha \delta_1 \delta_2 \cdots \delta_n 全体の集合を  T'_\alpha とすると  T_\alpha = T'_\alpha \cup \{\bot\} となります。

 T_\alpha \setminus \{\bot\} の元を  \alpha の部分項と呼ぶことにします。 \alpha の部分項を  \alpha \delta_1 \delta_2 \cdots \delta_n と表したときの最も小さい  n に対応する  \delta_1 \delta_2 \cdots \delta_n 全体の集合を  I_\alpha とします。 \delta_1 \delta_2 \cdots \delta_n \alpha の部分項  \alpha \delta_1 \delta_2 \cdots \delta_n の位置と呼ぶことにします。

 \alpha \in M[X] の位置  \delta_1 \delta_2 \cdots \delta_n \in  I_\alpha \beta \in M[X] で置き換えた  \alpha(\delta_1 \delta_2 \cdots \delta_n \gets \beta) を \begin{cases}
β & (n = 0) \\
L(α)(δ_2 \cdots δ_n \gets β) \cdot R(α) & (n>0, δ_1 = L) \\
L(α) \cdot R(α)(δ_2 \cdots δ_n \gets β) & (n>0, δ_1 = R) \\
\end{cases} と帰納的に定義します。 n = 0 のときの位置を  0 と書くことにします。

書き換え規則

 \alpha, \beta \in M[X] とします。 \alpha, \beta の順序のついた組  \langle \alpha, \beta \rangle の「ラムダ式化」  (x_1, x_2, \cdots, x_n \mapsto \langle \alpha, \beta \rangle): M[X]^n \to M[X]^2 を上の議論と同様に考えることができます。これを書き換え規則と呼び、 (x_1, x_2, \cdots, x_n \mapsto \alpha \to \beta) と書くことにします。

 \alpha \in M[X] に対して、代入写像  \sigma: Y \to M[X][Y] が存在して、ある  \alpha の部分項の位置  p \in I_\alpha に対して  p(\alpha) = \beta[\sigma] となるとき、 \alpha は書き換え規則  \rho = (Y \mapsto \beta \to \gamma) によって書き換え可能ということにします。 \alpha の部分項の位置  p \gamma[\sigma] で置き換えた  \alpha(p \gets \gamma[\sigma]) を書き換え後の項と呼ぶことにします。これを
 \alpha \xrightarrow{\rho, \sigma, p} \alpha(p \gets \gamma[\sigma])
または
 \alpha \xrightarrow{\rho} \alpha(p \gets \gamma[\sigma])
と書くことにします。

自由マグマによる項書き換え

再びマグマの左単位元・右単位元の問題を考えます。 M \{ e_L , e_R \} で生成された自由マグマ、書き換え規則を \begin{cases}
\rho_1 & = & ( & x & \mapsto & e_L \cdot x & \to & x & ) \\
\rho_2 & = & ( & x & \mapsto & x & \to & e_L \cdot x & ) \\
\rho_3 & = & ( & x & \mapsto & x \cdot e_R & \to & x & ) \\
\rho_4 & = & ( & x & \mapsto & x & \to & x \cdot e_R & )\\
\end{cases} とします。このとき
 e_L \xrightarrow{\rho_4, \sigma_1, 0} e_L \cdot e_R \xrightarrow{\rho_1, \sigma_2, 0} e_R
が成り立ちます。ここで

  •  X = \{ x \} \sigma_1: X \to M[X], \sigma_1(x) = e_L
  •  Y = \{ y \} \sigma_2: Y \to M[X][Y], \sigma_2(y) = e_R

とします。

この変換をすべてのパターンについて  n 段階行うと、 n 段階で得られるすべての結果を得ることができます。この場合はすべてのパターンに対して2段階行うと \begin{cases}
e_L & \xrightarrow{\rho_2} & e_L \cdot e_L & \xrightarrow{\rho_1} & e_L \\
e_L & \xrightarrow{\rho_4} & e_L \cdot e_R & \xrightarrow{\rho_1} & e_R \\
e_L & \xrightarrow{\rho_2} & e_L \cdot e_L & \xrightarrow{\rho_2} & e_L \cdot (e_L \cdot e_L) \\
e_L & \xrightarrow{\rho_4} & e_L \cdot e_R & \xrightarrow{\rho_2} & e_L \cdot (e_L \cdot e_R) \\
e_L & \xrightarrow{\rho_4} & e_L \cdot e_R & \xrightarrow{\rho_3} & e_L \\
e_L & \xrightarrow{\rho_2} & e_L \cdot e_L & \xrightarrow{\rho_4} & (e_L \cdot e_L) \cdot e_R \\
e_L & \xrightarrow{\rho_4} & e_L \cdot e_R & \xrightarrow{\rho_4} & (e_L \cdot e_R) \cdot e_R \\
\end{cases} となって、上記の結果が得られます。

代数的構造による圏論(12)

随伴(3) 随伴の三角等式による定義

随伴の定義についても本に従って見ていきます。

随伴の三角等式による定義

定義 8.1 \mathcal{C} \mathcal{D} 間の関手  \mathcal{C} \xrightarrow{F} \mathcal{D} \mathcal{C} \xleftarrow{G} \mathcal{D} について、自然変換  FG \overset{\varepsilon}{\Longrightarrow} \mathrm{id}_\mathcal{D} \mathrm{id}_\mathcal{C} \overset{\eta}{\Longrightarrow} GF が存在してこれらが三角等式を満たすとき、すなわち  \require{AMScd} \begin{CD}
F @> 1_F >> F \\
@V Fη VV @| \\
FGF @>> εF > F
\end{CD} \begin{CD}
G @> ηG >> GFG \\
@| @VV Gε V \\
G @>> 1_G > G
\end{CD} を可換にするとき、四つ組  \langle F, G, \varepsilon, \eta \rangle を随伴関係と呼びます。

定義(圏の積) \mathcal{C} \mathcal{D} の積  \mathcal{C} \times \mathcal{D} とは、

  •  \mathcal{C} \times \mathcal{D} の対象は、 \mathcal{C} の対象  X \mathcal{D} の対象  Y の組  \langle X, Y \rangle
  •  \mathcal{C} \times \mathcal{D} の射は、 \mathcal{C} の射  X \xrightarrow{f} X' \mathcal{D} の射  Y \xrightarrow{g} Y' の組  \langle X, Y \rangle \xrightarrow{\langle f, g \rangle} \langle X', Y' \rangle

であるものと定義します(これは圏となります)。

定義 関手  \mathcal{C}^\mathrm{op} \times \mathcal{C} \xrightarrow{\mathrm{Hom}_\mathcal{C}(-, -)} \mathbf{Set}

  •  \mathcal{C}^\mathrm{op} \times \mathcal{D} の対象  \langle X, Y \rangle \mathrm{Hom}_\mathcal{C}(X, Y) を対応させる
  •  \mathcal{C} の射  A' \xrightarrow{a} A に対応する  \mathcal{C}^\mathrm{op} の射を  A \xrightarrow{a^\mathrm{op}} A' とすると、 \mathcal{C}^\mathrm{op} の射を  A \xrightarrow{a^\mathrm{op}} A' \mathcal{C} の射  B \xrightarrow{b} B' の組である  \mathcal{C}^\mathrm{op} \times \mathcal{C} の射  \langle A, B \rangle \xrightarrow{\langle a^\mathrm{op}, b \rangle} \langle A', B' \rangle に対応する  \mathbf{Set} の射  \mathrm{Hom}_\mathcal{C}(A, B) \xrightarrow{\mathrm{Hom}_\mathcal{C}(a^\mathrm{op}, b)} \mathrm{Hom}_\mathcal{C}(A,' B') を、
    •  A \xrightarrow{x} B A' \xrightarrow{a} A \xrightarrow{x} B \xrightarrow{b} B' に対応させるもの

と定義します(これは関手となります)。

定義 関手  \mathcal{C} \xrightarrow{F} \mathcal{D} に対応する関手  \mathcal{C}^\mathrm{op} \xrightarrow{F^\mathrm{op}} \mathcal{D}^\mathrm{op} F^\mathrm{op} として

  •  \mathcal{C}^\mathrm{op} \times \mathcal{D} \xrightarrow{F^\mathrm{op} \times \mathrm{id}_\mathcal{D}} \mathcal{D}^\mathrm{op} \times \mathcal{D} \xrightarrow{\mathrm{Hom}_\mathcal{D}(-, -)} \mathrm{Set} \mathrm{Hom}_\mathcal{D}(F(-), -)
  •  \mathcal{C}^\mathrm{op} \times \mathcal{D} \xrightarrow{\mathrm{id}_{\mathcal{C}^\mathrm{op}} \times G} \mathcal{C}^\mathrm{op} \times \mathcal{C} \xrightarrow{\mathrm{Hom}_\mathcal{C}(-, -)} \mathrm{Set} \mathrm{Hom}_\mathcal{C}(-, G(-))

と書きます。

定理 8.2 \mathcal{C} \mathcal{D} 間の関手  \mathcal{C} \xrightarrow{F} \mathcal{D} \mathcal{C} \xleftarrow{G} \mathcal{D} の定める随伴関係  \langle F, G, \varepsilon, \eta \rangle から自然同値  \mathrm{Hom}_\mathcal{D}(F(-), -) \implies \mathrm{Hom}_\mathcal{C}(-, G(-)) を構成することができます。

[証明]

  •  F(X) \xrightarrow{f} Y から  X \xrightarrow{\eta_X} GF(X) \xrightarrow{G(f)} G(Y) への対応を  \Phi_{\langle X, Y \rangle}
  •  X \xrightarrow{g} G(Y) から  F(X) \xrightarrow{F(g)} FG(Y) \xrightarrow{\varepsilon_Y} Y への対応を  \Psi_{\langle X, Y \rangle}

とおきます。

  •  \mathrm{Hom}_\mathcal{D}(F(-), -) \overset{\Phi}{\Longrightarrow} \mathrm{Hom}_\mathcal{C}(-, G(-)) (カリー化)
  •  \mathrm{Hom}_\mathcal{D}(F(-), -) \overset{\Psi}{\Longleftarrow} \mathrm{Hom}_\mathcal{C}(-, G(-)) (アンカリー化)

は以下の図式が可換図式となることから自然変換となります。

 X \xrightarrow{x} X' Y \xrightarrow{y} Y' に関する以下の図式を考えます。(図式1) \begin{CD}
\mathrm{Hom}_{\mathcal{D}}(F(X),Y) @> \Phi_{\langle X, Y \rangle} >> \mathrm{Hom}_{\mathcal{C}}(X,G(Y)) \\
@V \mathrm{Hom}_{\mathcal{D}}(F(x),y) VV @VV \mathrm{Hom}_{\mathcal{C}}(x,G(y)) V \\
\mathrm{Hom}_{\mathcal{D}}(F(X'),Y') @> \Phi_{\langle X', Y' \rangle} >> \mathrm{Hom}_{\mathcal{C}}(X',G(Y')) \\
\end{CD}

 F(X) \xrightarrow{f} Y をとると、 \eta が自然変換であることから  GF(x) \circ η_{X'} = η_{X} \circ x となるので \begin{eqnarray*}
\Phi_{\langle X', Y' \rangle} ( \mathrm{Hom}_{\mathcal{D}}(F(x),y) (f) )
& = & \Phi_{\langle X', Y' \rangle} ( y \circ f \circ F(x) ) \\
& = & G(y) \circ G(f) \circ GF(x) \circ η_{X'} \\
& = & G(y) \circ G(f) \circ η_{X} \circ x \\
& = & \mathrm{Hom}_{\mathcal{C}}(x,G(y)) ( G(f) \circ η_{X} ) \\
& = & \mathrm{Hom}_{\mathcal{C}}(x,G(y)) ( \Phi_{\langle X, Y \rangle}(f) ) \\
\end{eqnarray*} となって、(図式1)は可換図式となります。よって  \Phi は自然変換となります。

 X \xrightarrow{x} X' Y \xrightarrow{y} Y' に関する以下の図式を考えます。(図式2) \begin{CD}
\mathrm{Hom}_{\mathcal{D}}(F(X),Y) @< \Psi_{\langle X, Y \rangle} << \mathrm{Hom}_{\mathcal{C}}(X,G(Y)) \\
@V \mathrm{Hom}_{\mathcal{D}}(F(x),y) VV @VV \mathrm{Hom}_{\mathcal{C}}(x,G(y)) V \\
\mathrm{Hom}_{\mathcal{D}}(F(X'),Y') @< \Psi_{\langle X', Y' \rangle} << \mathrm{Hom}_{\mathcal{C}}(X',G(Y')) \\
\end{CD}

 X \xrightarrow{g} G(Y) をとると、 \varepsilon が自然変換であることから  ε_{Y'} \circ FG(y) = y \circ ε_{Y} となるので \begin{eqnarray*}
\Psi_{\langle X', Y' \rangle} ( \mathrm{Hom}_{\mathcal{c}}(x,G(y)) (g) )
& = & \Phi_{\langle X', Y' \rangle} ( G(y) \circ g \circ x ) \\
& = & ε_{Y'} \circ FG(y) \circ F(g) \circ F(x) \\
& = & y \circ ε_{Y} \circ F(g) \circ F(x) \\
& = & \mathrm{Hom}_{\mathcal{D}}(F(x),y) ( ε_{Y} \circ F(g) ) \\
& = & \mathrm{Hom}_{\mathcal{D}}(F(x),y) ( \Psi_{\langle X, Y \rangle}(g) ) \\
\end{eqnarray*} となって、(図式2)は可換図式となります。よって  \Psi は自然変換となります。

 (Fη)_X = F(η_X) (εF)_X = ε_{F(X)} なので三角等式を書き換えると(図式3) \begin{CD}
F(X) @> 1_{F(X)} >> F(X) \\
@V F(η_X) VV @VV 1_{F(X)} V \\
FGF(X) @>> ε_{F(X)} > F(X)
\end{CD} は可換図式となります。 F(X) \xrightarrow{f} Y をとると、 ε は自然変換なので(図式4) \begin{CD}
F(X) @> 1_{F(X)} >> F(X) \\
@V F(η_X) VV @VV 1_{F(X)} V \\
FGF(X) @>> ε_{F(X)} > F(X) \\
@V FG(f) VV @VV f V \\
F(X) @>> ε_{Y} > Y
\end{CD} は可換図式となります。よって \begin{eqnarray*}
\Psi_{\langle X, Y \rangle} ( \Phi_{\langle X, Y \rangle} (f) )
& = & \Psi_{\langle X, Y \rangle} ( G(f) \circ η_{X} ) \\
& = & ε_{Y} \circ FG(f) \circ F(η_{X}) \\
& = & f \\
\end{eqnarray*} となって、 \Psi \circ \Phi \mathrm{Hom}_{\mathcal{D}}(F(-), -) の恒等自然変換となります。

 (Gε)_Y = G(ε_Y) (ηG)_Y = η_{G(Y)} なので三角等式を書き換えると(図式5) \begin{CD}
G(Y) @> η_{G(Y)} >> GFG(Y) \\
@V 1_{G(Y)} VV @VV G(ε_Y) V \\
G(Y) @>> 1_{G(Y)} > G(Y)
\end{CD} は可換図式となります。 X \xrightarrow{g} G(Y) をとると、 η は自然変換なので(図式6) \begin{CD}
X @> η_{X} >> GF(X) \\
@V g VV @VV GF(g) V \\
G(Y) @> η_{G(Y)} >> GFG(Y) \\
@V 1_{G(Y)} VV @VV G(ε_Y) V \\
G(Y) @>> 1_{G(Y)} > G(Y)
\end{CD} は可換図式となります。よって \begin{eqnarray*}
\Phi_{\langle X, Y \rangle} ( \Psi_{\langle X, Y \rangle} (g) )
& = & \Phi_{\langle X, Y \rangle} ( ε_Y \circ F(g) ) \\
& = & G(ε_{Y}) \circ GF(g) \circ η_{X} \\
& = & g \\
\end{eqnarray*} となって、 \Phi \circ \Psi \mathrm{Hom}_{\mathcal{C}}(-, G(-)) の恒等自然変換となります。

よって  \Phi は自然同値となります。[証明終わり]

代数的構造による圏論(11)

随伴(2) 積関手と冪関手

自由マグマと自由モノイドの関係を使って、随伴(の一部)を説明することができると思ったのですが、まだできていないし、随伴の全体を説明することは難しいと思われるので、また「圏論の道案内 ~矢印でえがく数学の世界~」の「第8章 随伴 ①積と冪との間の関係」に従って説明していくことにします。

これ以降この本では可換モノイド、半環、行列などの話題が現れないようですが、これらについても調査していく予定です。

積関手

積を持つ圏  \mathcal{C} の対象  A に対して

  • 任意の対象  X に対して対象  A \times X
  • 任意の射  X \xrightarrow{f} Y に対して射  A \times X \xrightarrow{1_A \times f} A \times Y

を対応させるものは関手となります。この関手を  \mathcal{C} から  \mathcal{C} への積関手  A \times () と呼びます。

冪関手

積および冪を持つ圏  \mathcal{C} において、対象  X に対して評価射  A \times X^A \xrightarrow{\varepsilon_X} X は、任意の射  A \times Y \xrightarrow{h} X に対して 射  Y \xrightarrow{\tilde{h}} X^A で(可換図式1)  \require{AMScd} \begin{CD}
A \times Y @> h >> X \\
@V 1_A \times \tilde{h} VV @VV 1_X V \\
A \times X^A @>> \varepsilon_X > X
\end{CD} を可換にするものが一意的に存在するものとなります。 \tilde{h} h のカリー化または転置と呼び、ここでは  \mathrm{curry}(h) と書きます。

 X \xrightarrow{f} Y に対して、冪の普遍性(可換図式1)より  X^A \xrightarrow{u} Y^A で(可換図式2) \begin{CD}
A \times X^A @> \varepsilon_X >> X \\
@V 1_A \times u VV @VV f V \\
A \times Y^A @>> \varepsilon_Y > Y
\end{CD} を可換にするものが一意的に存在します。

この  u f^A と書くと、冪を持つ圏  \mathcal{C} の対象  A に対して

  • 任意の対象  X に対して対象  X^A
  • 任意の射  X \xrightarrow{f} Y に対して射  X^A \xrightarrow{f^A} Y^A

を対応させるものは関手となります。この関手を  \mathcal{C} から  \mathcal{C} への関手(冪関手)  ()^A と呼びます。

積関手と冪関手の関係 ( \varepsilon)

積関手を  F_A、冪関手を  G_A とすると、(可換図式2)は(可換図式3) \begin{CD}
F_A G_A (X) @> \varepsilon_X >> X \\
@V F_A G_A (f) VV @VV f V \\
F_A G_A (Y) @>> \varepsilon_Y > Y \\
\end{CD} となって、自然変換  F_A G_A \overset{\varepsilon}{\Longrightarrow} \mathrm{id}_\mathcal{C} を表すものとなります。

積関手と冪関手の関係 ( \eta)

対象  A X に対して冪の普遍性(可換図式1)より(可換図式4) \begin{CD}
A \times X @> 1_A \times 1_X >> A \times X \\
@V 1_A \times η_X VV @VV 1_A \times 1_X V \\
A \times (A \times X)^A @>> \varepsilon_{A \times X} > A \times X
\end{CD} を可換にする  X \xrightarrow{η_X} (A \times X)^A が一意的に存在します( η_X = \mathrm{curry}(1_A \times 1_X))。

 A \times X \xrightarrow{1_A \times f} A \times Y のカリー化  X \xrightarrow{g} (A \times Y)^A ( g = \mathrm{curry}(1_A \times f))が一意的に存在して(可換図式5) \begin{CD}
A \times X @> 1_A \times f >> A \times Y \\
@V 1_A \times g VV @VV 1_A \times 1_Y V \\
A \times (A \times Y)^A @>> \varepsilon_{A \times Y} > A \times Y
\end{CD} を可換にします。

以下の図式が可換図式となることを見ていきます。(図式6) \begin{CD}
X @> η_X >> (A \times X)^A \\
@V f VV @VV (1_A \times f)^A V \\
Y @>> η_Y > (A \times Y)^A \\
\end{CD}

(可換図式4)より以下の図式(可換図式7) \begin{CD}
A \times X @> 1_A \times f >> A \times Y \\
@V 1_A \times f VV @VV 1_A \times 1_Y V \\
A \times Y @> 1_A \times 1_Y >> A \times Y \\
@V 1_A \times η_Y VV @VV 1_A \times 1_Y V \\
A \times (A \times Y)^A @>> \varepsilon_{A \times Y} > A \times Y
\end{CD} は可換図式となります。(可換図式5)より  \eta_Y \circ f = \mathrm{curry}(1_A \times f) となります。

(可換図式4)、(可換図式2)より(可換図式8) \begin{CD}
A \times X @> 1_A \times 1_X >> A \times X \\
@V 1_A \times η_X VV @VV 1_A \times 1_X V \\
A \times (A \times X)^A @> \varepsilon_{A \times X} >> A \times X \\
@V 1_A \times (1_A \times f)^A VV @VV 1_A \times f V \\
A \times (A \times Y)^A @>> \varepsilon_{A \times Y} > A \times Y
\end{CD} は可換図式となります。(可換図式5)のより  (1_A \times f)^A \circ η_X = \mathrm{curry}(1_A \times f) となります。

よって(図式6)は可換図式となり(可換図式9) \begin{CD}
X @> η_X >> G_A F_A(X) \\
@V f VV @VV G_A F_A(f) V \\
Y @>> η_Y > G_A F_A(Y) \\
\end{CD} は可換図式となり、自然変換  \mathrm{id}_\mathcal{C} \overset{\eta}{\Longrightarrow} G_A F_A を表す可換図式となります。

三角等式

三角等式 ( F_AG_AF_A)

(可換図式4)を  F_A G_A を使って描くと(可換図式10) \begin{CD}
F_A(X) @> 1_{F_A(X)} >> F_A(X) \\
@V F_A(η_X) VV @VV 1_{F_A(X)} V \\
F_AG_AF_A(X) @>> \varepsilon_{F_A(X)} > F_A(X)
\end{CD} となります。

三角等式 ( G_AF_AG_A)

(可換図式10)で  X G_A(X) にすると(可換図式11) \begin{CD}
F_AG_A(X) @> 1_{F_AG_A(X)} >> F_AG_A(X) \\
@V F_A(η_{G_A(X)}) VV @VV 1_{F_AG_A(X)} V \\
F_AG_AF_AG_A(X) @>> \varepsilon_{F_AG_A(X)} > F_AG_A(X)
\end{CD} は可換図式となります。

(可換図式3)で  X \xrightarrow{f} Y F_A G_A (X) \xrightarrow{\varepsilon_X} X とすると(可換図式12) \begin{CD}
F_A G_A F_A G_A (X) @> \varepsilon_{F_A G_A (X)} >> F_A G_A (X) \\
@V F_A G_A (\varepsilon_X) VV @VV \varepsilon_X V \\
F_A G_A (X) @>> \varepsilon_X > X \\
\end{CD} は可換図式となります。

(可換図式11)と(可換図式12)より(可換図式13) \begin{CD}
F_AG_A(X) @> 1_{F_AG_A(X)} >> F_AG_A(X) \\
@V F_A(η_{G_A(X)}) VV @VV 1_{F_AG_A(X)} V \\
F_A G_A F_A G_A (X) @> \varepsilon_{F_A G_A (X)} >> F_A G_A (X) \\
@V F_A G_A (\varepsilon_X) VV @VV \varepsilon_X V \\
F_A G_A (X) @>> \varepsilon_X > X \\
\end{CD} は可換図式となって、 G_A (\varepsilon_X) \circ η_{G_A(X)} = \mathrm{curry}(\varepsilon_X) となります。

(可換図式3)の  X \xrightarrow{f} Y X \xrightarrow{1_{X}} X とすると(可換図式14)
\begin{CD}
F_A G_A (X) @> \varepsilon_X >> X \\
@V F_A(1_{G_A (X)}) VV @VV 1_X V \\
F_A G_A (X) @>> \varepsilon_X > X \\
\end{CD} は可換図式となって、 1_{G_A(X)} = \mathrm{curry}(\varepsilon_X) となります。

よって(可換図式15) \begin{CD}
G_A (X) @> η_{G_A(X)} >> G_A F_A G_A(X) \\
@V 1_{G_A (X)} VV @VV G_A (\varepsilon_X) V \\
G_A (X) @>> 1_{G_A (X)} > G(X) \\
\end{CD} は可換図式となります。

三角等式 (自然変換  \varepsilon, \eta)

関手  H と自然変換  t を合成した自然変換  Ht tH X 成分が

  •  (Ht)_X = H(t_X)
  •  (tH)_X = t_{H(X)}

であるものと定義します。\begin{CD}
F_A @> 1_{F_A} >> F_A \\
@V F_Aη VV @| \\
F_AG_AF_A @>> εF_A > F_A
\end{CD} \begin{CD}
G_A @> ηG_A >> G_AF_AG_A \\
@| @VV G_Aε V \\
G_A @>> 1_{G_A} > G_A
\end{CD} は自然変換の可換図式となります。

代数的構造による圏論(10)

随伴(1) 自由マグマ

まず基本になると思われる自由マグマから始めます。

マグマ

集合  M が二項演算  \cdot を持つとき  (M, \cdot) をマグマと呼びます。単に  M と表すこともあります。

部分マグマ

 (M, \cdot) をマグマとします。 X, Y \subseteq M に対して  X \cdot Y = \{ x \cdot y \mid x \in X, y \in Y \} と書くことにします。 X \subseteq M X \cdot X \subseteq X を満たすとき  X \cdot X への制限に関してマグマとなります。このような  X M の部分マグマと呼びます。 X M の部分マグマであるとき  X \le M と書くことにします。マグマ  M の部分マグマ全体の集合を  \mathfrak{S}(M) と書くことにします。

マグマの準同型

マグマ  (M. \cdot) からマグマ  (M', *) への写像  f: M \to M' が演算を保存するとき、すなわち

  •  f(x \cdot y) = f(x) * f(y)

を満たすとき、 f をマグマ  (M. \cdot) からマグマ  (M', *) へのマグマの準同型と呼びます。 f の像  f(M) M' の部分マグマとなります。 f全単射であるときマグマの同型と呼びます。マグマの同型  f: M \to M' が存在するとき  (M. \cdot) (M', *) は同型である(通常は演算を省略して  M M' は同型である)といい、 M \cong M' と書きます。

部分集合で生成された部分マグマ

 X をマグマ  M の部分集合とします。 N \subseteq M に対して、 N X を含む  M の部分マグマ( X \subseteq N \le M)であり、 X を含む  M の部分マグマの最小のもの、すなわち

  •  N' X を含む  M の部分マグマ( X \subseteq N' \le M)ならば  N \subseteq N'

であるとき、 N X で生成された  M の部分マグマと呼びます。マグマ  M X で生成された  M の部分マグマであるとき  M X で生成されたマグマと呼びます。

  • (MAG1)  N N' がどちらも  X で生成された  M の部分マグマならば  N = N' となります。

 X \subseteq M に対して  \overline{X} = \{ N \in \mathfrak{S}(M) \mid X \subseteq N \le M \} とおき、  \displaystyle X^+ = \bigcap \overline{X} とおきます。

任意の  N \in \overline{X} に対して  X \subseteq N となるので  X = \bigcap \{ X \mid N \in \overline{X} \} \subseteq \bigcap \{ N \mid N \in \overline{X} \} = X^+ が成り立ちます。また
\begin{eqnarray*}
X^+ \cdot X^+ & = & \left(\bigcap \overline{X}\right) \cdot \left(\bigcap \overline{X}\right) \\
& \subseteq & \bigcap \{ N \cdot N' \mid N, N' \in \overline{X} \} \\
& \subseteq & \bigcap \{ N \cdot N \mid N \in \overline{X} \} \\
& \subseteq & \bigcap \{ N \mid N \in \overline{X} \} = X^+ \\
\end{eqnarray*}
となります。よって  X \subseteq X^+ \le M が成り立ち、 X^+ X で生成された部分マグマとなります。

 X \subseteq M に対して、 X^{(\cdot)} = X \cup (X \cdot X) とおき、 X^{(\cdot)(n)}帰納的に
\begin{cases}
X^{(\cdot)(0)} = X \\
X^{(\cdot)(n+1)} = (X^{(\cdot)(n)})^{(\cdot)} \\
\end{cases}
と定義します。 \displaystyle X^{(\cdot)(*)} = \bigcup_{n \in \mathbb{N}} X^{(\cdot)(n)} とおくと、 X = X^{(\cdot)(0)} \subseteq X^{(\cdot)(*)} であり、
\begin{eqnarray*}
X^{(\cdot)(*)} \cdot X^{(\cdot)(*)} & = & \left( \bigcup_{n \in \mathbb{N}} X^{(\cdot)(n)} \right) \cdot \left( \bigcup_{n \in \mathbb{N}} X^{(\cdot)(n)} \right) \\
& \subseteq & \bigcup_{n \in \mathbb{N}} \bigcup_{n' \in \mathbb{N}} \left( X^{(\cdot)(n)} \cdot X^{(\cdot)(n')} \right) \\
& \subseteq & \bigcup_{n \in \mathbb{N}} \bigcup_{n' \in \mathbb{N}} X^{(\cdot)(n+n')} \\
& \subseteq & \bigcup_{n \in \mathbb{N}} X^{(\cdot)(n)} = X^{(\cdot)(*)} \\
\end{eqnarray*}
となります。よって  X \subseteq X^{(\cdot)(*)} \le M が成り立ち、 X^{(\cdot)(*)} X で生成された部分マグマとなります。

(MAG1)より  X^+ = X^{(\cdot)(*)} が成り立ちます。

自由マグマ

 M X で生成されたマグマ(または  X と集合として同値な集合で生成されたマグマ)で、任意のマグマ  M'写像  f: X \to M' に対して  f を拡張したマグマの準同型  f^*: M \to M' が一意的に存在するとき、 M X で生成された自由マグマと呼びます。 \eta: X \to M を包含写像とすると  f^* \circ \eta = f が成り立ちます。(以下は可換図式) \require{AMScd} \begin{CD}
X @> f >> M' \\
@V η VV @| \\
M @>> f^* > M'
\end{CD}

  • (MAG2)  M M' がどちらも  X で生成された自由マグマならば  M \cong M' となります。

(MAG3)  M X で生成された自由マグマ、 \eta: X \to M を包含写像 M' をマグマとします。

  • 写像  f: X \to M' に対して  f を拡張したマグマの準同型  f^*: M \to M' が一意的に存在します。 f^* = \varphi(f) とおきます。
  • マグマの準同型  g: M \to M' に対して  g X への制限写像  g|_X: X \to M' が一意的に存在します。 g|_X = \psi(g) とおきます。
  •  \psi(\varphi(f)) = f が成り立ちます。
  •  \varphi(\psi(g)) = g が成り立ちます。

集合  X に対して、 X に「  (」(開きかっこ)、「 )」(閉じかっこ)、「 *」(アスタリスク) という元をを付け加えた集合を  C_X とし、 C_X の元からなる有限個の列全体の集合を  S_X とします。すなわち、 S_X の元は、ある自然数  n が存在して  a_1 a_2 \cdots a_n という列で、各  a_i X の元であるか、開きかっこ、閉じかっこ、アスタリスクのどれかであるものとします。

 S_X に二項演算  \cdot: S_X \times S_X \to S_X \alpha \cdot \beta (\alpha * \beta) という列と定義すると  S_X はマグマとなります。 \iota: X \to S_X x \in X x という(長さ  1 の)列を対応させる写像とします。

 \eta(X) で生成された  S_X の部分マグマを  M_X とおきます。

 \displaystyle M_X = X^{(\cdot)(*)} = \bigcup_{n \in \mathbb{N}} X^{(\cdot)(n)} より  \alpha \in M_X に対してある自然数  n が存在して  \alpha \in X^{(\cdot)(n)} となります。このような最小の  n n_\alpha とおきます。

 n_\alpha > 0 のとき  \alpha = \beta \cdot \gamma となる  \beta, \gamma が存在します。 \alpha (\beta * \gamma) という列なのでこのような  \beta, \gamma は一意的に存在します。

よってマグマ  M'写像  f: X \to M' に対して  f^*: M_X \to M'
\begin{cases}
f^*(\alpha) = f(x) & (n_\alpha = 0, \alpha = \iota(x)) \\
f^*(\alpha) = f^*(\beta) \cdot f^*(\gamma) & (n_\alpha > 0, \alpha = \beta \cdot \gamma) \\
\end{cases}
と定義することができて、 n_\alpha > 0 のとき  f^*(\beta \cdot \gamma) = f^*(\beta) \cdot f^*(\gamma) が成り立つのでマグマの準同型となります。

また  n_\alpha = 0 のとき  f^*(\eta(x)) = f(x) が成り立つので  f^* \circ \eta = f が成り立ちます。

また、 g: M_X \to M' f を拡張したマグマの準同型とすると、任意の  \alpha \in M_X に対して  \alphaアスタリスクの個数に関する帰納法によって  g(\alpha) = f^*(\alpha) が成り立ちます。よって  M_X X で生成された自由マグマとなります。

集合の直積と直和との関係

集合  X, Y に対して、集合の直積  X \times Y、集合の直和  X + Y が一意的に決まるとします。

集合の直和を作る演算は可換かつ結合的とし、有限個の集合からなる集合  \mathcal{X} = \{ X_1, X_2, \cdots, X_m \} に対して  X_1 + X_2 + \cdots + X_m \bigsqcup \mathcal{X} と表します。 \mathcal{X} = \{ X_1, X_2, \cdots, X_m \} \mathcal{Y} = \{ Y_1, Y_2, \cdots, Y_n \} に対して  \mathcal{X} \cdot \mathcal{Y} = \{ X \times Y \mid X \in \mathcal{X}, Y \in \mathcal{Y} \} と定義します。

有限個の集合からなる集合  \mathcal{X} に対して、 \mathcal{X}^{(\cdot\cdot)} = \mathcal{X} \cup (\mathcal{X} \cdot \mathcal{X}) とおきます。集合  X に対して  X^{(\cdot\cdot)(n)}帰納的に
\begin{cases}
X^{(\cdot\cdot)(0)} = \{X\} \\
X^{(\cdot\cdot)(n+1)} = (X^{(\cdot\cdot)(n)})^{(\cdot\cdot)} \\
\end{cases}
と定義します。 \displaystyle X^{(\cdot\cdot)(*)} = \bigcup_{n \in \mathbb{N}} X^{(\cdot\cdot)(n)} とおくと、 X \in X^{(\cdot\cdot)(0)} \subseteq X^{(\cdot\cdot)(*)} であり、
\begin{eqnarray*}
X^{(\cdot\cdot)(*)} \cdot X^{(\cdot\cdot)(*)} & = & \left( \bigcup_{n \in \mathbb{N}} X^{(\cdot\cdot)(n)} \right) \cdot \left( \bigcup_{n \in \mathbb{N}} X^{(\cdot\cdot)(n)} \right) \\
& \subseteq & \bigcup_{n \in \mathbb{N}} \bigcup_{n' \in \mathbb{N}} \left( X^{(\cdot\cdot)(n)} \cdot X^{(\cdot\cdot)(n')} \right) \\
& \subseteq & \bigcup_{n \in \mathbb{N}} \bigcup_{n' \in \mathbb{N}} X^{(\cdot\cdot)(n+n')} \\
& \subseteq & \bigcup_{n \in \mathbb{N}} X^{(\cdot\cdot)(n)} = X^{(\cdot\cdot)(*)} \\
\end{eqnarray*}
となります。

 M^\times_X = \bigsqcup  X^{(\cdot\cdot)(*)} とおきます。 y \in Y \in X^{(\cdot\cdot)(*)} z \in Z \in X^{(\cdot\cdot)(*)} に対して  y z の組  \langle y, z \rangle \in Y \times Z \in X^{(\cdot\cdot)(*)} y \cdot z と定義すると、 (M^\times_X, \cdot) はマグマとなります。 M_X の元を  X の元で表したものを同じ形の  M^\times_X の元に対応させる写像はマグマの同型となるので、 (M^\times_X, \cdot) X で生成された自由マグマとなります。

随伴との関係

Wikipedia「随伴関手」の「自由群」の項を参考にします。ここの書き方に従って関手の記法を  FGX のように書くことがあります。

 \mathbf{Set} を集合の圏、 \mathbf{Mag} をマグマの圏とします。

関手  F : \mathbf{Mag} ← \mathbf{Set} は各集合  Y Y で生成された自由マグマを対応させるものとし、関手  G : \mathbf{Mag} → \mathbf{Set} はマグマ  X にその台集合を対応させる忘却関手とします。

集合  Y で生成された自由マグマ  FY とは、 GFY Y を含み( \eta_Y: Y \to GFY を包含写像とする)、任意のマグマ  X写像  g: Y \to GX に対してマグマの準同型  g^*: FY \to X が一意的に存在して、 G(g^*) \circ \eta_Y = g が成り立つというものでした。(可換図式1)
\begin{CD}
Y @> g >> GX \\
@V η_Y VV @| \\
GFY @>> G(g^*) > GX
\end{CD}

マグマの準同型  f: X \to X' に対して、 G(f): GX \to GX' f を集合の間の写像とみなしたものとすれば  G は関手となります。

集合の間の写像  g: Y \to Y' に対して、 F(g): FY \to FY' F(g) = (\eta_{Y'} \circ g)^* とすれば  F は関手となります。(可換図式2)
\begin{CD}
Y @> η_{Y'} \circ g >> GFY' \\
@V η_Y VV @| \\
GFY @>> G(η_{Y'} \circ g)^* > GFY'
\end{CD}
(可換図式2)より  1_Y: Y \to Y に対して
\begin{CD}
Y @> η_{Y} >> GFY \\
@V η_Y VV @| \\
GFY @>> G (1_{FY}) > GFY
\end{CD} は可換図式となり、自由マグマ  FY の普遍性( G (1_{FY}) の射の一意性)より  F (1_Y) = 1_{FY} = (\eta_{Y})^* となります。

以下に示すように  F G の左随伴となります。

余単位-単位随伴

(MAG3)より  \mathbf{Mag} の対象  X \mathbf{Set} の対象  Y に対して、 FY \xrightarrow{f} X Y に制限した  Y \xrightarrow{g} GX は一意的に存在し、 Y \xrightarrow{g} GX FY に拡張した  FY \xrightarrow{f} X は一意的に存在します。この対応
 \Phi_{Y,X}: \mathrm{Hom}_{\mathbf{Mag}}(FY,X) \to \mathrm{Hom}_{\mathbf{Set}}(Y,GX)
全単射となります。

マグマ  X に対して、 \varepsilon_{X}: FGX \to X \varepsilon_{X} = \Phi_{GX,X}^{-1}(1_{GX}) とおくと、以下の可換図式を満たします。(可換図式3)
\begin{CD}
GX @> 1_{GX} >> GX \\
@V η_{GX} VV @| \\
GFGX @>> G (\varepsilon_{X}) > GX
\end{CD}

 X \xrightarrow{f} X' とすると  \Phi_{GX,X'}^{-1}(G(f)) = ε_{X'} \circ FG(f) = f \circ ε_{X} となって(可換図式4)
\begin{CD}
FGX @> FG(f) >> FGX' \\
@V ε_{X} VV @VV ε_{X'} V \\
X @>> f > X'
\end{CD} は可換図式となり、 FG \overset{\varepsilon}{\Longrightarrow} 1_{\mathbf{Mag}} は自然変換となります。

集合  Y に対して、 Y \xrightarrow{\eta_Y} GFY \eta_{Y} = \Phi_{Y,FY}(1_{FY}) とおくと、以下の可換図式を満たします。(可換図式5)
\begin{CD}
FY @> F(η_{Y}) >> FGFY \\
@| @VV ε_{FY} V \\
FY @>> 1_{FY} > FY
\end{CD}

 Y \xrightarrow{g} Y' に対して、 \Phi_{Y,FY'}(F(g)) = η_{Y'} \circ g = GF(g) \circ η_{Y} となって(可換図式6)
\begin{CD}
Y @> g >> Y' \\
@V η_{Y} VV @VV η_{Y'} V \\
GFY @>> GF(g) > GFY'
\end{CD} は可換図式となり、 1_{\mathbf{Set}} \overset{\eta}{\Longrightarrow} GF は自然変換となります。

 FG \overset{\varepsilon}{\Longrightarrow} 1_{\mathbf{Mag}} を余単位、 1_{\mathbf{Set}} \overset{\eta}{\Longrightarrow} GF を単位と呼びます。

(可換図式5)、(可換図式3)より任意の  \mathbf{Mag} の対象  X \mathbf{Set} の対象  Y に対して \begin{eqnarray*}
1_{{FY}} &=& \varepsilon _{{FY}}\circ F(η_{Y}) \\
1_{{GX}} &=& G(\varepsilon _{X})\circ η_{{GX}}
\end{eqnarray*} が成り立ちます。よって余単位-単位恒等式 \begin{eqnarray*}
1_{F} &=& \varepsilon F\circ Fη \\
1_{G} &=& G\varepsilon \circ ηG
\end{eqnarray*} が成り立ちます。

[定義] \mathcal{C} \mathcal{D}、関手  F: \mathcal{C} \gets \mathcal{D} G: \mathcal{C} \to \mathcal{D}、 自然変換(余単位および単位)
\begin{aligned}
ε: & \ FG \to 1_{\mathcal{C}} \\
η: & \ 1_{\mathcal{D}} \to GF
\end{aligned}
が余単位-単位恒等式 \begin{eqnarray*}
1_{F} &=& \varepsilon F\circ Fη \\
1_{G} &=& G\varepsilon \circ ηG
\end{eqnarray*} を満たすとき、 F G の左随伴、 G F の右随伴と呼びます。この関係を  (\varepsilon ,\eta ):F \dashv G、または単に  F \dashv Gと書きます。

(三角等式) この等式を以下の可換図式で記述して三角等式と呼びます。(ただし三角形の図が描けないので四角形で描きますがこの等式自体を三角等式と呼ぶようなので問題はありません。) \begin{CD}
F @> 1_F >> F \\
@V Fη VV @| \\
FGF @>> εF > F
\end{CD} \begin{CD}
G @> ηG >> GFG \\
@| @VV Gε V \\
G @>> 1_G > G
\end{CD}

 F から  X への普遍射

 Y \mathbf{Set} の対象、 f : FY → X \mathbf{Mag} の射とすると、(可換図式5)、(可換図式4)より(可換図式7)
\begin{CD}
FY @> F(η_{Y}) >> FGFY @> FG(f) >> FGX \\
@| @VV ε_{FY} V @VV ε_{X} V \\
FY @>> 1_{FY} > FY @>> f > X
\end{CD}
は可換図式となります。よって  g = G(f) \circ η_{Y} とおくと  \varepsilon_{X} \circ F(g) = f となります。 g = \Phi_{Y,X}(f) となります。よって

  •  Y \mathbf{Set} の対象で  f : FY → X \mathbf{Mag} の射ならば、 \mathbf{Set} の射  g : Y → GX が一意的に存在して  \varepsilon_{X} \circ F(g) = f

が成り立ちます。よって  (GX,\varepsilon_{X}) F から  X への普遍射となります。

[定義] \mathcal{C} \mathcal{D}、関手  F: \mathcal{C} \gets \mathcal{D} が、任意の  \mathcal{C} の対象  X に対して  F から  X への普遍射が存在するとき、 F を左随伴関手と呼びます。

 \mathcal{C} の対象  X に対して  \mathcal{D} の対象  G_0X F から  X への普遍射  ε_X : FG_0X → X を決めます。関手  G: \mathcal{C} \to \mathcal{D} を、

  •  GX = G_0X
  •  \mathcal{C} の射  f : X → X' に対して  ε_{X'} \circ F(g) = f \circ  ε_X を満たす  g: GX \to GX' が一意的に存在します。この  g に対して  G(f) = g

と定義することができます。このとき  F G の左随伴であるといいます。

 Y から  G への普遍射

 X \mathbf{Mag} の対象、 g : GX \gets Y \mathbf{Set} の射とすると、(可換図式6)、(可換図式3)より(可換図式8)
\begin{CD}
Y @> g >> GX @> 1_{GX} >> GX \\
@V η_{Y} VV @VV η_{GX} V @| \\
GFY @>> GF(g) > GFGX @>> G (\varepsilon_{X}) > GX
\end{CD}
は可換図式となります。よって  f = \varepsilon_{X} \circ F(g) とおくと   G(f) \circ \eta_{Y} = g となります。 f = \Phi_{Y,X}^{-1}(g) となります。よって

  •  X \mathbf{Mag} の対象で  g : GX \gets Y \mathbf{Set} の射ならば、 \mathbf{Mag} の射  f : X \gets FY が一意的に存在して   G(f) \circ \eta_{Y} = g

が成り立ちます。よって  (FY,\eta_{Y}) Y から  G への普遍射となります。

[定義] \mathcal{C} \mathcal{D}、関手  G: \mathcal{C} \to \mathcal{D} が、任意の  \mathcal{D} の対象  Y に対して  Y から  G への普遍射が存在するとき、 G を右随伴関手と呼びます。

 \mathcal{D} の対象  Y に対して  \mathcal{C} の対象  F_0Y Y から  G への普遍射  η_Y : Y → GF_0Y を決めます。関手  F: \mathcal{C} \gets \mathcal{D} を、

  •  FY = F_0Y
  •  \mathcal{D} の射  g : Y → Y' に対して  G(f) \circ η_Y = η_{Y'} \circ g を満たす  f: FY \to FY' が一意的に存在します。この  f に対して  F(g) = f

と定義することができます。このとき、 G F の右随伴であるといいます。

Hom集合随伴

 \mathbf{Mag} の対象  X \mathbf{Set} の対象  Y \mathbf{Mag} の射  FY \xrightarrow{f} X \mathbf{Set} の射  Y \xrightarrow{g} GX \Phi_{Y,X}(f) = g を満たすとします。

(可換図式7)より任意の  \mathbf{Mag} の射  FY \xrightarrow{f} X に対して  \mathbf{Set} の射  Y \xrightarrow{g} GX が一意的に存在して以下の図式は可換図式となります。よって任意の  \mathbf{Set} の射  Y' \xrightarrow{y} Y に対して以下の図式を可換にする  Y' \to GX の射は一意的に存在します。(可換図式9)
\begin{CD}
FY' @> F(y) >> FY @> F(g) >> FGX \\
@. @| @VV ε_{X} V \\
@. FY @>> f > X
\end{CD}
よって  \Phi_{Y',X}(f \circ F(y)) = g \circ y が成り立ちます。このとき  \Phi_{Y,X} Y に関して自然であるといいます。これを \begin{equation*}
\cfrac{FY' \xrightarrow{F(y)} FY \xrightarrow{f} X}{Y' \xrightarrow[y]{} Y \xrightarrow[g]{} GX}
\end{equation*} と表します。

(可換図式8)より任意の  \mathbf{Set} の射  Y \xrightarrow{g} GX に対して  \mathbf{Mag} の射  FY \xrightarrow{f} X が一意的に存在して以下の図式は可換図式となります。よって任意の  \mathbf{Mag} の射  X \xrightarrow{x} X' に対して以下の図式を可換にする  FY \to X' の射は一意的に存在します。(可換図式10)
\begin{CD}
Y @> g >> GX \\
@VV η_{Y} V @| \\
GFY @>> G(f) > GX @>> G(x) > GX'
\end{CD}
よって  \Phi_{Y,X'}(x \circ f) = G(x) \circ g が成り立ちます。このとき  \Phi_{Y,X} X に関して自然であるといいます。これを \begin{equation*}
\cfrac{FY \xrightarrow{f} X \xrightarrow{x} X'}{Y \xrightarrow[g]{} GX \xrightarrow[G(x)]{} GX'}
\end{equation*} と表します。

[定義]  \Phi_{Y,X} Y に関して自然であり、 X に関して自然であるとき、 F G の左随伴であり  G F の右随伴であるといいます。この関係を  \Phi: F \dashv G、または単に  F\dashv G と書きます。

この対応によって  \Phi : \mathrm{Hom}_{\mathbf{Mag}}(F-,-) \to \mathrm{Hom}_{\mathbf{Set}}(-,G-) は自然同型となります。以下でこれを説明します。

 \mathbf{Mag} の対象  X に対して  \mathrm{Hom}_{\mathbf{Mag}}(F-,X)

  •  \mathbf{Set} の対象  Y \mathrm{Hom}_\mathbf{Mag}(FY, X) を対応させ、
  •  \mathbf{Set}の射  y: Y' \to Y \psi(y) = \mathrm{Hom}_\mathbf{Mag}(Fy, X): \mathrm{Hom}_\mathbf{Mag}(FY, X) \to \mathrm{Hom}_\mathbf{Mag}(FY', X) \psi(y)(f) = f \circ F(y) を対応させるもの

\begin{CD}
FY' @> \psi(y)(f) >> X \\
@V F(y) VV @| \\
FY @>> f > X
\end{CD} と定義すると、 Y'' \xrightarrow{y'} Y' \xrightarrow{y} Y に対して \begin{eqnarray*}
\psi(y \circ y')(f) & = & f \circ ( F(y \circ y') ) \\
& = & f \circ ( F(y) \circ F(y') ) \\
& = & ( f \circ F(y) ) \circ F(y') \\
& = & \psi(y') ( f \circ F(y) ) \\
& = & \psi(y') ( \psi(y) (f) ) \\
& = & (\psi(y') \circ \psi(y))(f)
\end{eqnarray*} となり、 \mathbf{Set} から  \mathbf{Set} への反変関手となります。

 \mathbf{Mag} の対象  X に対して  \mathrm{Hom}_{\mathbf{Set}}(-,GX)

  •  \mathbf{Set} の対象  Y \mathrm{Hom}_\mathbf{Set}(Y, GX) を対応させ、
  •  \mathbf{Set}の射  y: Y' \to Y \psi(y) = \mathrm{Hom}_\mathbf{Set}(y, GX): \mathrm{Hom}_\mathbf{Set}(Y, GX) \to \mathrm{Hom}_\mathbf{Set}(Y', GX) \psi(y)(g) = g \circ y を対応させるもの

\begin{CD}
Y' @> \psi(y)(g) >> GX \\
@V y VV @| \\
Y @>> g > GX
\end{CD} と定義すると、 Y'' \xrightarrow{y'} Y' \xrightarrow{y} Y に対して \begin{eqnarray*}
\psi(y \circ y')(g) & = & g \circ ( (y \circ y' ) \\
& = & ( g \circ y ) \circ y' \\
& = & \psi(y') ( g \circ y ) \\
& = & \psi(y') ( \psi(y) (g) ) \\
& = & (\psi(y') \circ \psi(y))(g)
\end{eqnarray*} となり、 \mathbf{Set} から  \mathbf{Set} への反変関手となります。

 \mathbf{Set} の対象  Y に対して  \mathrm{Hom}_{\mathbf{Mag}}(FY,-)

  •  \mathbf{Mag} の対象  X \mathrm{Hom}_\mathbf{Mag}(FY, X) を対応させ、
  •  \mathbf{Mag}の射  x: X \to X' \psi(x) = \mathrm{Hom}_\mathbf{Mag}(FY, x): \mathrm{Hom}_\mathbf{Mag}(FY, X) \to \mathrm{Hom}_\mathbf{Mag}(FY, X') \psi(x)(f) = x \circ f を対応させるもの

\begin{CD}
FY @> f >> X \\
@| @VV x V \\
FY @>> \psi(x)(f) > X'
\end{CD} と定義すると、 X \xrightarrow{x} X' \xrightarrow{x'} X'' に対して \begin{eqnarray*}
\psi(x' \circ x)(f) & = & (x' \circ x) \circ f \\
& = & x' \circ (x \circ f) \\
& = & x' \circ \psi(x)(f) \\
& = & \psi(x')( \psi(x)(f) ) \\
& = & (\psi(x') \circ \psi(x))(f) \\
\end{eqnarray*} となり、 \mathbf{Mag} から  \mathbf{Set} への共変関手となります。

 \mathbf{Set} の対象  Y に対して  \mathrm{Hom}_{\mathbf{Set}}(Y,G-)

  •  \mathbf{Mag} の対象  X \mathrm{Hom}_\mathbf{Set}(Y, GX) を対応させ、
  •  \mathbf{Mag}の射  x: X \to X' \psi(x) = \mathrm{Hom}_\mathbf{Set}(Y, Gx): \mathrm{Hom}_\mathbf{Set}(Y, GX) \to \mathrm{Hom}_\mathbf{Set}(Y, GX') \psi(x)(g) = G(x) \circ g を対応させるもの

\begin{CD}
Y @> g >> GX \\
@| @VV G(x) V \\
Y @>> \psi(x)(g) > GX'
\end{CD} と定義すると、 X \xrightarrow{x} X' \xrightarrow{x'} X'' に対して \begin{eqnarray*}
\psi(x' \circ x)(g) & = & G(x' \circ x) \circ g \\
& = & (G(x') \circ G(x)) \circ g \\
& = & G(x') \circ (G(x) \circ g) \\
& = & G(x') \circ \psi(x)(g) \\
& = & \psi(x')(\psi(x)(g)) \\
& = & (\psi(x') \circ \psi(x))(g) \\
\end{eqnarray*} となり、 \mathbf{Mag} から  \mathbf{Set} への共変関手となります。

これらの関手を組み合わせることによって  \mathrm{Hom}_{\mathbf{Mag}}(F-,-): \mathbf{Set}^\mathrm{op} \times \mathbf{Mag} \to \mathbf{Set} \mathrm{Hom}_{\mathbf{Set}}(-,G-): \mathbf{Set}^\mathrm{op} \times \mathbf{Mag} \to \mathbf{Set} は関手となります。

 \mathbf{Set} の対象  Y Y'、射  g: Y' \to Y \mathbf{Mag} の対象  X X'、射  f: X \to X' に対して(可換図式9)、(可換図式10)より  \Phi_{Y,X}: \mathrm{Hom}_{\mathbf{Mag}}(FY,X) \to \mathrm{Hom}_{\mathbf{Set}}(Y,GX) は可換図式
\begin{CD}
\mathrm{Hom}_{\mathbf{Mag}}(FY,X) @> \Phi_{Y,X} >> \mathrm{Hom}_{\mathbf{Set}}(Y,GX) \\
@V \mathrm{Hom}_{\mathbf{Mag}}(Fg,f) VV @VV \mathrm{Hom}_{\mathbf{Set}}(g,Gf) V \\
\mathrm{Hom}_{\mathbf{Mag}}(FY',X') @> \Phi_{Y',X'} >> \mathrm{Hom}_{\mathbf{Set}}(Y',GX') \\
\end{CD}
を満たすので  \Phi : \mathrm{Hom}_{\mathbf{Mag}}(F-,-) \to \mathrm{Hom}_{\mathbf{Set}}(-,G-) は自然変換となります。 \Phi_{Y,X}全単射なので  \Phi は自然同型(自然同値)となります。

[定義]  \Phi が自然同型であるとき、 F G の左随伴であり  G F の右随伴であるといいます。この関係を  \Phi: F \dashv G、または単に  F\dashv G と書きます。

代数的構造による圏論(9)

トポス(1)

この段階で数学的帰納法を使うことによって図式を使わずに説明することができるようになったと思うのですが、簡単にはいかないのでトポスについてもう少し調べてみたいと思います。

[4]、[5]、[6]、[7]の本を持っていたので少し読んでみようと思います。[4]、[5]は型理論の本でトポスに関する記述もあるようです。[7]はトポスの本のようです。[6]は圏論全般の本のようですがトポスに関する記述があります。ただ英語のトポスの本を読むのはたいへんなので、[2]、[3]の本を持っていたのでまずこれから読んで見たいと思います。

まずトポスの定義から見ていきます。

[1] 圏論の道案内 ~矢印でえがく数学の世界~

[1]のトポスの定義は以下のようになっています。

定義 7.2 (トポス) \mathcal{C} が CCC であり、部分対象分類子を持つとき、初等トポス(elementary topos)あるいは単にトポスと呼びます。ここで部分対象分類子(subobject classifier)とは  \mathcal{C} の射  1 \xrightarrow{t} \Omegaで、任意の単射  A \xrightarrow{m} B に対して射  B \xrightarrow{\chi_m} \Omega \require{AMScd} \begin{CD}
A @> !_A >> 1 \\
@V m VV @VV t V \\
B @>> \chi_m > \Omega
\end{CD} が引き戻しの図式となるようなものが一意に存在するものをいいます。このとき  \chi_m m の特性射(characteristic morphism)と呼びます。 t は真(True)とも呼ばれ、また True とも書かれます。そして  \Omega は真理値対象(truth value object)と呼ばれます。

[2] 圏論による論理学―高階論理とトポス

部分対象分類子の定義、以下の定義 1 (トポス)は[1]と同じです。

定義 1 (トポス) 圏が以下の条件 (1)~(4) を満たすときトポスと呼びます。

  • (1) 終対象が存在する。
  • (2) 任意の対象  A, B に対して積  A \times B が存在する。
  • (3) 任意の対象  A, B に対して冪  B^A が存在する。
  • (4) 部分対象分類子が存在する。

<1> 終対象、積、部分対象分類子が存在するなら、イコライザーが存在する。

[証明] A \overset{f}{\underset{g}{\rightrightarrows}} B とします。[1]で  \binom{f}{g} と書かれていた射をここでは  \langle f, g \rangle と書いています。 \Delta_B = \langle 1_B, 1_B \rangle とし  B \times B \xrightarrow{\delta_B} \Omega を図式(1) \begin{CD}
B @> !_B >> 1 \\
@V \Delta_B VV @VV t V \\
B \times B @>> \delta_B > \Omega
\end{CD} が引き戻しの図式となる射とします。 A \xrightarrow{\langle f, g \rangle} B \times B \xrightarrow{\delta_B} \Omega に対して図式(2) \begin{CD}
C @> !_C >> 1 \\
@V e VV @VV t V \\
A @>> \delta_B \circ \langle f, g \rangle > \Omega
\end{CD} が引き戻しの図式となる射  C \xrightarrow{e} A が存在します。*1

 X \xrightarrow{p} C とすると、図式(3) \begin{CD}
X @> !_X >> 1 \\
@V e \circ p VV @VV t V \\
A @>> \delta_B \circ \langle f, g \rangle > \Omega
\end{CD} は可換となります。図式(2)が引き戻しの図式であることから  e \circ p = e \circ u となる  X \xrightarrow{u} C が一意的に存在します。一意性より  e \circ p = e \circ u' ならば  u = u' となります。よって  e \circ p = e \circ q ならば  p = q となるので  e単射となります。*2

図式(4) \begin{CD}
C @> !_C >> 1 \\
@V \langle f, g \rangle \circ e VV @VV t V \\
B \times B @>> \delta_B > \Omega
\end{CD} が可換で図式(1)が引き戻しの図式であることから、 \langle f, g \rangle \circ e = \Delta_B \circ v を満たす  C \xrightarrow{v} B が一意的に存在します。よって  f \circ e = \pi_1 \circ \langle f, g \rangle \circ e = \pi_1 \circ \Delta_B \circ v = 1_B \circ v = v g \circ e = \pi_2 \circ \langle f, g \rangle \circ e = \pi_2 \circ \Delta_B \circ v = 1_B \circ v = v となり  f \circ e = g \circ e となります。

 D \xrightarrow{h} A f \circ h = g \circ h を満たすとします。 \langle f, g \rangle \circ h = \langle f \circ h, g \circ h \rangle = \langle f \circ h, f \circ h \rangle = \Delta_B \circ f \circ h となって、図式(5) \begin{CD}
D @> f \circ h >> B @> !_B >> 1 \\
@V h VV @V \Delta_B VV @VV t V \\
A @>> \langle f, g \rangle > B \times B @>> \delta_B > \Omega
\end{CD} は可換となります。図式(1)が引き戻しの図式であることから  D \xrightarrow{w} C が一意的に存在して  e \circ w = h となります。

よって  C \xrightarrow{e} A A \overset{f}{\underset{g}{\rightrightarrows}} Bイコライザーとなっています。】

<2> 積、イコライザーが存在するなら、引き戻しが存在する。
[証明] A \xrightarrow{f} C \xleftarrow{g} B とすると、イコライザーが存在することから \begin{CD}
X @> e >> A \times B \\
@V e VV @VV g \circ \pi_2 V \\
A \times B @>> f \circ \pi_1 > C
\end{CD} が可換となるイコライザー  X \xrightarrow{e} A が存在します。\begin{CD}
Y @> q >> B \\
@V p VV @VV g V \\
A @>> f > C
\end{CD} が可換とすると、\begin{CD}
Y @> \langle p, q \rangle >> A \times B \\
@V \langle p, q \rangle VV @VV g \circ \pi_2 V \\
A \times B @>> f \circ \pi_1 > C
\end{CD} は可換となり、 X \xrightarrow{e} Aイコライザーなので  Y \xrightarrow{u} X e \circ u = \langle p, q \rangle であるものが存在します。 \pi_1 \circ e \circ u = \pi_1 \circ \langle p, q \rangle = p \pi_2 \circ e \circ u = \pi_2 \circ \langle p, q \rangle = q となるので \begin{CD}
X @> \pi_2 \circ e >> B \\
@V \pi_1 \circ e VV @VV g V \\
A @>> f > C
\end{CD} は引き戻しの図式となります。】

<3> 定義 1 の (1)~(4) が成立するなら、始対象、直和、押し出しが存在する。この証明は省略されています。

定義 2 (トポス) 圏が以下の条件 (1)~(4) を満たすときトポスと呼びます。

  • (1) 終対象が存在する。
  • (2) 任意の射  A \to C \gets B に対して引き戻しが存在する。
  • (3) 任意の対象  A, B に対して冪  B^A が存在する。
  • (4) 部分対象分類子が存在する。

<4> 終対象と引き戻しが存在するなら、積が存在する。
[証明]【 図式(1) \begin{CD}
X @> g >> B \\
@V f VV @VVV \\
A @>>> 1
\end{CD} を引き戻しの図式とします。 A \xleftarrow{p} Y \xrightarrow{q} B とすると、
\begin{CD}
Y @> q >> B \\
@V p VV @VVV \\
A @>>> 1
\end{CD} は可換となります。図式(1)が引き戻しの図式であることから、 Y \xrightarrow{u} X f \circ u = p g \circ u = q であるものが存在します。よって  A \xleftarrow{f} X \xrightarrow{g} B は積の図式となります。】 

[3] 層・圏・トポス―現代的集合像を求めて

定義 (部分対象分類子) 部分対象分類子(subobject classifier)とは  \mathcal{C} の射  1 \xrightarrow{t} \Omegaで、以下の二つの条件を満たすものをいいます。

(1) 任意の  B \xrightarrow{f} \Omega に対して  A \xrightarrow{g} B で \begin{CD}
A @> !_A >> 1 \\
@V g VV @VV t V \\
B @>> f > \Omega
\end{CD} が引き戻しの図式となるようなものが存在する。

(2) 任意の単射  A \xrightarrow{m} B に対して射  B \xrightarrow{\chi_m} \Omega で \begin{CD}
A @> !_A >> 1 \\
@V m VV @VV t V \\
B @>> \chi_m > \Omega
\end{CD} が引き戻しの図式となるようなものが一意に存在する。

部分対象分類子の定義は[1]の定義に条件(1)が追加されたものです。

定義 (トポス) \mathcal{C} が CCC であり、部分対象分類子を持つとき、トポスと呼びます。

トポスの定義も同様に[1]の定義に条件(1)が追加されたものとなっています。

[4] Introduction to Higher-Order Categorical Logic

  • Part II Type theory and toposes
    • 3 The internal language of a topos

定義 (部分対象分類子) 部分対象分類子(subobject classifier)とは  \mathcal{C} の射  1 \xrightarrow{t} \Omegaで、以下の二つの条件を満たすものをいいます。

  • (1) 任意の  B \xrightarrow{f} \Omega に対して  B \xrightarrow{f} \Omega B \xrightarrow{!_B} 1 \xrightarrow{t} \Omegaイコライザー  A \xrightarrow{g} B が存在する
  • (2) [3]の(2)と同じ

トポスの定義では自然数対象を持つという条件が増えています。自然数対象の定義は[1]と同じです。

定義 3.1 (トポス) \mathcal{C} が CCC であり、部分対象分類子と自然数対象を持つとき、トポスと呼びます。

[5] Categories, Types, and Structures

  • 2 Constructions
    • 2.7 Subobject Classifiers and Topoi

定義 2.7.2 (トポス) [2]定義 2 と同じです。

[6] Computational Category Theory

  • 7 Toposes
    • 7.2 Toposes

定義 26 (トポス) 圏が以下の条件 (1)~(3) を満たすときトポスと呼びます。

  • (1) 有限図式に対する極限が存在する(有限完備)。有限図式に対する余極限が存在する(有限余完備)。
  • (2) 任意の対象  A, B に対して冪  B^A が存在する。
  • (3) 部分対象分類子が存在する。

[7] Sheaves in Geometry and Logic

  • IV. First Properties of Elementary Topoi
    • 1. Definition of a Topos

定義 (トポス) 圏が以下の条件 (1)~(4) を満たすときトポスと呼びます。

  • (1) 終対象が存在する。
  • (2) 任意の射  A \to C \gets B に対して引き戻しが存在する。
  • (3) 部分対象分類子が存在する。
  • (4) 任意の対象  B に対して、以下の条件を満たす対象  PB、射  B \times PB \xrightarrow{\in_B} \Omega が存在する:
    • 任意の射  B \times A \xrightarrow{f} \Omega に対して、以下の図式を可換にする射  A \xrightarrow{g} PB が一意的に存在する:

\begin{CD}
B \times A @> f >> \Omega \\
@V 1_B \times g VV @| \\
B \times PB @>> \in_B > \Omega
\end{CD}

*1:この理由は不明。引き戻しが存在すると仮定すると成り立ちますが、後で引き戻しの存在の証明に使われているのでそれでは意味がない。 集合の場合は  h = \delta_B \circ \langle f, g \rangle とおくと  C = h^{-1}(true) = \bigcup \{ X \mid X \subseteq A \ で図式が可換 \} となります。 集合のように書くと  C \xrightarrow{e} A = \{ X \xrightarrow{m} A \mid \ 単射で図式が可換 \} という射が存在すると仮定すれば成り立ちます。\begin{CD} X @> !_X >> 1 \\ @V m VV @VV t V \\ A @>> \delta_B \circ \langle f, g \rangle > \Omega \end{CD}

*2: e が最初から単射としたときはこの議論は不要。

中間報告(6)

このブログは、論理プログラミングに実行順序を指定する機能を追加するため、現在は主に数学的帰納法や可換モノイドについてプログラミング言語で記述する方法を調査しています。

前回の中間報告以降更新したもの

代数的構造による圏論 ← 斜めの線を使わない圏論

このブログでは普通の圏論の本に載っているような図式を書くことができないらしいので、「斜めの線を使わない圏論」では、自由生成モノイド、自由生成可換モノイド、自由生成半環などを構成するような方法で、極限、随伴などを説明することができないか検討していました。圏論の本に載っているような説明は私にはわかりにくいので、別の説明の方法があるかどうか考えていましたが、特に進展はありませんでした。

このシリーズでは、「圏論の道案内」を読みながら上記のような問題を考えていきます。

圏論の道案内」では自然変換を中心に説明されています。「第4章 自然変換」、その前の「第3章 関手」ではたぶん自然変換に関連した例が書かれていています。その前に「前順序」の説明があります。このあたりは何かの説明に使えるかもしれません。

続いて、この本では「コンマ圏」を使って「第5章 普遍性 ⑥射圏,そして一般射圏」で極限が説明されています。この本では「コンマ圏」のことを「一般射圏」と呼んでいます。

「エレファントな整数論」で写像から作られる前順序集合について調べているのですが、そのような議論をするには「第7章 圏論集合論」の「①トポス(topos)」、「②圏論集合論」まで読んだほうが良いようなので、そこまでは読みました。

今の段階で

  • 数学的帰納法の記述
  • 帰納的定義の記述
  • 可換モノイドに関する帰納法の記述
  • 外積の定義と計算
  • 連立一次方程式の順序に依存しない解法
  • 論理プログラミングとしての半環の標準化

を結合律を使った書き方で書く方法を考えることができると思われます。しかし、トポスの定義がまだよくわかっていないので、他の本も参考にして調べています。「直観主義論理」や「型理論」に関する本もあったので読んでみることにします。これは無限に動くプログラムの連携に使えるのではないかと思っています。

「論理プログラミングとしての半環の標準化」というのは論理プログラミングの実行を「選言標準形」のような形に変形することと考えた場合どうなるかというものです。結合律のような法則により自然数より少し一般的な全順序集合の合成と考えることができます。これはモナドが関連するかもしれないのでモナドのところまで読んでみます。今のところこの「変形」を説明する言葉がないので、まずそれを考えた後で次に進もうと思います。

エレファントな整数論

の説明のところまで終わった状況です。これらは定義から自動的に実行できるはずだが、実行順序によっては実行できないことがあり、それを記述するためのプログラミング言語の要素がないと考えられます。今後はこれらの記述方法について考えていきます。

前回の中間報告以降更新していないもの

エレファントな線形代数

連立一次方程式の解法や行列のランクなどを、行列を使わずに説明することを引き続き考えていきます。

エレファントな関数論

コーシーの積分定理の証明について調査中です。

群論の計算

数学的帰納法や可換モノイドの記述について調査した後、以下のような計算が簡単に書けるようになるかどうか調査する予定です。

  • 群の簡単な計算
  • 可解群の定義
  • 対称式の基本定理
  • ガロア理論の基本定理
  • 可解群と代数方程式の代数的解法の関係

保留中のシリーズ

以下の記事のシリーズは、他の案件で進展があるまで保留中です。

今後の予定

まだどのような形で数式の「変形」を書けば良いのかわかっていないので、まずそこから考えていきます。その後いろいろな数学の問題について考えて、プログラミング言語で表すことができるのかどうか考えていきます。