エレファントな群とリー代数(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} となって、上記の結果が得られます。