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

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

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