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

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

中間報告(7)

このブログは、論理プログラミングを無限に実行する場合、実行順序を指定する機能を追加することを目的としています。現在は「無限の項書き換え」のような方法で記述する方法を検討しています。

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

項書き換えと同様の方法で群やリー代数で成り立つ関係を示すということをやっています。現在はマグマとモノイドで成り立つ関係について書いています。項書き換えの標準的な記述方法は『Universal Algebra for Computer Scientists (Monographs in Theoretical Computer Science. An EATCS Series, 25)』または『計算論理に基づく推論ソフトウェア論』に書かれていると思われますが、まだ全部読んでいないのでよくわかりません。また、項書き換えを無限に繰り返したものを扱うには「多項式の代入」の記述方法の方が良いのではないかと思われるため、現在はそのような記述方法になっています。この方法が有効かどうかはまだわかりません。

現在は環で成り立つ関係を示すということをやっています。この内容は『環の演算』で書いたものです。ここでは書き換え規則を合成するということをやっています。これを説明するために、現在は単一化について説明しています。単一化については『計算論理に基づく推論ソフトウェア論』に書かれているようなのでこの本を見ています。

今後は合成を無限に繰り返したものを記述する方法について考えていきます。このような記述方法があれば、数学の理論でプログラムとして記述することができるものがあると考えられます。このような記述方法がないために記述する方法がないという誤解があるという気がするので、それを解消したいと考えています。

代数的構造による圏論

現在は『圏論の道案内 ~矢印でえがく数学の世界~ 数学への招待』という本を随伴の項目まで読んでいます。「項書き換え」のような方法で随伴を記述するということが目標ですが、現在はまだ随伴のことがよくわかっていないので本の引用だけになっています。

数学的帰納法、可換モノイド、連立一次方程式については、残念ながらこの本にはこの後とくに記述がありませんでした。

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

エレファントな整数論

この項目も「項書き換え」のような方法で

の記述ができないか、今後考えていきます。

エレファントな線形代数

この項目も「項書き換え」のような方法で、連立一次方程式の解法や行列のランクなどを、行列を使わずに記述できるかを今後考えていきます。

エレファントな関数論

この項目も「項書き換え」のような方法で、コーシーの積分定理の証明について記述できないか、今後考えていきます。

群論の計算

この項目も「項書き換え」のような方法で、

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

について記述できないか、今後考えていきます。

今後の予定

現在は「無限の項書き換え」のような方法で数学の問題を記述する方法を検討しています。今後は他の方法も検討していき、プログラミング言語で表すことを目標としています。

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

一般マグマの多項式の単一化アルゴリズム(2)

この項目の内容は「一階の項」の理論と内容は同じものになると思われます。書き方を変えることで極限や普遍性について考えるときに多項式の考え方が使えると思うのですが、今のところどうなるかわかりません。

前回の  u(\alpha, \beta, \sigma) の定義は、 \alpha, \beta を固定しても、変化させても定義できるのですが、両方が混じっていたので変化させるように書き直します。また、記述が複雑になってしまったので  M[X] T として書き直します。

 T f_i(t_1, t_2, \cdots, t_n) という形の元の全体を  T_{f_i}、 T_{f_0} = M とします。すると、 T = X \cup T_{f_0} \cup T_{f_1} \cup T_{f_2} \cup \cdots \cup T_{f_m} となります。 T_+ = T_{f_0} \cup T_{f_1} \cup T_{f_2} \cup \cdots \cup T_{f_m} とします。

 \Sigma を置換全体の集合とします。 v(\alpha) \alpha の部分項として現れる  X の元全体の集合とします。

 u(\alpha, \beta) u: T \times T \to \Sigma \sqcup \{F\} ( F は失敗を表す)を(場合分け(*)) \begin{cases}
(1) & α \in M, & β \in M, & α = β & のとき & σ \\
(2) & α \in M, & β \in M, & α \ne β & のとき & F \\
(3) & α \in X, & β \in X, & α = β & のとき & σ \\
(4) & α \in X, & β \in X, & α \ne β & のとき & σ \succ (α \mapsto β) \\
(5) & α \in X, & β \in T_+, & α \notin v(β) & のとき & σ \succ (α \mapsto β) \\
(6) & α \in X, & β \in T_+, & α \in v(β) & のとき & F \\
(7) & α \in T_+, & β \in X , & β \notin v(α) & のとき & σ \succ (β \mapsto α) \\
(8) & α \in T_+, & β \in X , & β \in v(α) & のとき & F \\
(9) & α \in T_f, & β \in T_g , & f = g & のとき & 以下を参照 \\
(10) & α \in T_f, & β \in T_g , & f \ne g & のとき & F \\
\end{cases} と定義します(定義できるかどうかは以下で検討)。(9)は \begin{cases}
σ \in Σ & のとき & σ \triangleright u(s, t) = u(s[σ], t[σ]) \\
F & のとき & F \triangleright u(s, t) = F \\
\end{cases} としたとき \begin{eqnarray*}
(9) & & u(f(s_1, s_2, \cdots, s_n), f(t_1, t_2, \cdots, t_n)) \\
& = & 1 \triangleright u(s_1, t_1) \triangleright u(s_2, t_2) \triangleright \cdots \triangleright u(s_n, t_n) \\
\end{eqnarray*} と定義します( \triangleright は左から順に適用)。このとき \begin{cases}
u(α, β) = σ \in Σ & のとき & σ \ は \ α, β \ の最汎単一化子 \\
u(α, β) = F & のとき & α, β \ は単一化不可能 \\
\end{cases} が成り立ちます。

単一化アルゴリズムの定義

 u(\alpha, \beta) \alpha, \beta を変化させても定義できるならば、 u写像として定義できます。場合分け(*)の(1)から(10)の場合分けを1段階として、上位の部分項から順に実行することはアルゴリズムということができます。(9)の項は左から順に実行するとします。

 \alpha の部分項  f_i(t_1, t_2, \cdots, t_n) があるとき  f_i(t_1, t_2, \cdots, t_n) > t_j とします。 r+1 個の部分項が  t_0 > t_1 > \cdots > t_r という関係のとき  t_0 >^r t_r とします。 \alpha の部分項で  t >^r t' となる最大の  r r(\alpha) r(\alpha, \beta) = \max(r(\alpha), r(\beta)) とします。

 k(\alpha, \beta) v(\alpha) \cup v(\beta) の元の個数とします。

 k(\alpha, \beta) = 0 のとき、 u(\alpha, \beta) r(\alpha, \beta) 段階実行すると、ある  \sigma \in \Sigma または  F の結果を得ることができます。

 k= k(\alpha, \beta) とし、 u(\alpha, \beta) を段階的に実行して結果が得られるとき、その段階数を  s(\alpha, \beta) とします。結果が得られないとき、 s(\alpha, \beta) = \infty とします。

 r= r(\alpha, \beta) k= k(\alpha, \beta) のとき、 s(\alpha, \beta) の最大値があれば  t(r, k) とします。最大値がなければ  t(r, k) = \infty とします。

 k = 0 のとき  r = s(\alpha, \beta) = t(r, 0) となります。

 t(r, k) \le (2^{k+1}-1)r と仮定します。

 u(\alpha, \beta) r(\alpha, \beta) 段階実行すると、 \alpha または  \beta の部分項に  X の元が出現します。最初に現れた  X の元に対応する項を代入したものを  \alpha', \beta' とします。すると  r(\alpha', \beta') \le 2r(\alpha, \beta) k(\alpha', \beta') = k-1 となります。

帰納法の仮定より \begin{eqnarray*}
& & t(r(α', β'), k(α', β')) \\
& \le & r + (2^{k(α', β')+1}-1)r(α', β') \\
& \le & r + (2^{ (k - 1 ) + 1 }- 1) \cdot 2r \\
& = & (2^{k+1}-1)r
\end{eqnarray*} となって、任意の  \alpha, \beta に対して  t(r(\alpha, \beta), k(\alpha, \beta)) \le (2^{k(\alpha, \beta)+1}-1)r(\alpha, \beta) が成り立ちます。

よって  s(\alpha, \beta) \le t(r, k) \le (2^{k+1}-1)r となります。 u(\alpha, \beta) \alpha, \beta を変化させても定義できるので写像となり、上位の部分項から順に実行する手順はアルゴリズムということができます。

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

一般マグマの多項式の単一化

(および自然数の演算)(日本語が正しく表示されない可能性がありますがいつか書き直します)の使い方を説明すると書きましたが、ここで行っている「規則の合成」を説明するには単一化(ユニフィケーション)について説明する必要があるのでまずそこから説明します。

wikipedia:ユニフィケーション」(Wikipedia)の項目に書かれている内容と同じなのですが、Wikipediaの用語はわかりにくいので、「最汎単一化子 (most general unifier, MGU)」(これは一般的な用語です。Wikipediaでは最大汎用単一子)という用語を使って説明します。また、「多項式の代入」を使って説明したほうが今後の説明がわかりやすくなると思われるため、その方針で説明します。

 M[X] を一般マグマの多項式(Wikipediaでは「一階の項」と呼ばれているものに相当します)とします。 X から  M[X] への写像を置換(これはWikipediaでも使われていますが一般的な用語のようです)と呼びます。「多項式 \alpha \in M[X] に置換  \sigma: X \to M[X] を「代入」したものを  \alpha[\sigma] = \sigma^*(\alpha) \in M[X] とします( \sigma^* \sigma を拡張したただ一つの一般マグマの準同型)。

 \alpha, \beta \in M[X] に対して、置換  \sigma: X \to M[X] が存在して  \alpha[\sigma] = \beta[\sigma] となるとき、 \alpha \beta は単一化可能といって、 \sigma を単一化子と呼びます。

置換  \sigma, \tau: X \to M[X] に対して、 \varphi \circ \sigma = \tau を満たす一般マグマの準同型  \varphi: M[X] \to M[X] が存在するとき  \sigma \le \tau と書くことにします。

 \alpha \beta が単一化可能であるとき、 \tau \alpha \beta の単一化子ならば  \sigma \le \tau となる単一化子  \sigma が存在します。 \sigma を最汎単一化子と呼びます。

一般マグマの多項式の単一化アルゴリズム

 M の演算を  f_1, f_2, \cdots, f_m とします。演算の結果を  f_i(t_1, t_2, \cdots, t_n) のように写像の形で書くことにします。 M[X] f_i(t_1, t_2, \cdots, t_n) という形の元の全体を  M[X]_{f_i} とすると、 M[X] = M \cup X \cup M[X]_{f_1} \cup M[X]_{f_2} \cup \cdots \cup M[X]_{f_m} となります。 M[X]_{f_0} = M M[X]_+ = M[X]_{f_0} \cup M[X]_{f_1} \cup M[X]_{f_2} \cup \cdots \cup M[X]_{f_m} とします。

 \Sigma を置換全体の集合とします。 x \in X \alpha \in M に対して、置換  (x \mapsto \alpha) を \begin{cases}
x \mapsto \alpha \\
y \mapsto \alpha & (y \ne x) \\
\end{cases} という写像とし、 (x \mapsto \alpha) を拡張したただ一つの一般マグマの準同型を  (x \mapsto \alpha)^*、 置換  \sigma に対して  (x \mapsto \alpha)^* \circ \sigma \sigma \succ (x \mapsto \alpha) と書くことにします。

 v(\alpha) \alpha の部分項として現れる  X の元全体の集合とします。 u: M[X] \times M[X] \times \Sigma \to \Sigma \sqcup \{F\} ( F は失敗を表す)、 u(\alpha, \beta, \sigma) を \begin{cases}
α[σ] \in M, & β[σ] \in M, & α[σ] = β[σ] & のとき & σ \\
α[σ] \in M, & β[σ] \in M, & α[σ] \ne β[σ] & のとき & F \\
α[σ] \in X, & β[σ] \in X, & α[σ] = β[σ] & のとき & σ \\
α[σ] \in X, & β[σ] \in M[X]_+, & α[σ] \notin v(β[σ]) & のとき & σ \succ (α[σ] \mapsto β[σ]) \\
α[σ] \in X, & β[σ] \in M[X]_+, & α[σ] \in v(β[σ]) & のとき & F \\
α[σ] \in M[X]_+, & β[σ] \in X , & β[σ] \notin v(α[σ]) & のとき & σ \succ (β[σ] \mapsto α[σ]) \\
α[σ] \in M[X]_+, & β[σ] \in X , & β[σ] \in v(α[σ]) & のとき & F \\
α[σ] \in M[X]_f, & β[σ] \in M[X]_g , & f = g & のとき & 以下の(*)を参照 \\
α[σ] \in M[X]_f, & β[σ] \in M[X]_g , & f \ne g & のとき & F \\
\end{cases} と(演算の回数に関して)帰納的に定義することができます。(*)は \begin{cases}
σ \in Σ & のとき & σ \triangleright u(s, t) = u(s[σ], t[σ], σ) \\
F & のとき & F \triangleright u(s, t) = F \\
\end{cases} としたとき \begin{eqnarray*}
(*) & & u(f(s_1, s_2, \cdots, s_n), f(t_1, t_2, \cdots, t_n), σ) \\
& = & σ \triangleright u(s_1, t_1) \triangleright u(s_2, t_2) \triangleright \cdots \triangleright u(s_n, t_n) \\
\end{eqnarray*} と定義します。

 1 X の恒等写像 X から  M[X] への写像とみなした置換とします。\begin{cases}
u(α, β, 1) = σ \in Σ & のとき & σ \ は \ α, β \ の最汎単一化子 \\
u(α, β, 1) = F & のとき & α, β \ は単一化不可能 \\
\end{cases} が成り立ちます。この結果は項の順序に依存しません。

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

環の性質(2)

任意の  n 項演算を任意の個数もつ代数的構造に対しても「±マグマ」と同様の議論が成り立ちます。これを「一般マグマ」と呼ぶことにします。「一般マグマ」によって環の性質を証明することができます。

前回の続きを書いていきます。\begin{cases}
\rho_{1} & = & ( & x & \mapsto & 0 + x & \to & x & ) \\
\rho_{2} & = & ( & x & \mapsto & x & \to & 0 + x & ) \\
\rho_{3} & = & ( & x & \mapsto & x + 0 & \to & x & ) \\
\rho_{4} & = & ( & x & \mapsto & x & \to & x + 0 & ) \\
\rho_{5} & = & ( & x & \mapsto & (-x) + x & \to & 0 & ) \\
\rho_{6} & = & ( & x & \mapsto & 0 & \to & (-x) + x & ) \\
\rho_{7} & = & ( & x & \mapsto & x + (-x) & \to & 0 & ) \\
\rho_{8} & = & ( & x & \mapsto & 0 & \to & x + (-x) & ) \\
\rho_{9} & = & ( & x, y, z & \mapsto & (x + y) + z & \to & x + (y + z) & ) \\
\rho_{10} & = & ( & x, y, z & \mapsto & x + (y + z) & \to & (x + y) + z & ) \\
\rho_{11} & = & ( & x, y, z & \mapsto & (x y) z & \to & x (y z) & ) \\
\rho_{12} & = & ( & x, y, z & \mapsto & x (y z) & \to & (x y) z & ) \\
\rho_{13} & = & ( & y, x, z & \mapsto & x (y + z) & \to & x y + x z & ) \\
\rho_{14} & = & ( & x, y, z & \mapsto & x y + x z & \to & x (y + z) & ) \\
\rho_{15} & = & ( & x, y, z & \mapsto & (x + y) z & \to & x z + y z & ) \\
\rho_{16} & = & ( & x, y, z & \mapsto & x z + y z & \to & (x + y) z & ) \\
\rho_{17} & = & ( & x & \mapsto & x 0 & \to & 0 & ) \\
\rho_{18} & = & ( & x & \mapsto & 0 & \to & x 0 & ) \\
\rho_{19} & = & ( & x & \mapsto & 0 x & \to & 0 & ) \\
\rho_{20} & = & ( & x & \mapsto & 0 & \to & 0 x & ) \\
\end{cases} から \begin{matrix}
x ( -y ) & \xrightarrow{\rho_{4}} & x ( -y ) + 0 \\
& \xrightarrow{\rho_{8}} & x ( -y ) + ( x_{8,2} + ( -x_{8,2} ) ) \\
& \xrightarrow{\rho_{10}} & ( x ( -y ) + y_{10,3} ) + ( -y_{10,3} ) \\
& \xrightarrow{\rho_{14}} & x ( ( -y ) + z_{14,4} ) + ( -x z_{14,4} ) \\
& \xrightarrow{\rho_{5}} & x 0 + ( -x y ) \\
& \xrightarrow{\rho_{17}} & 0 + ( -x y ) \\
& \xrightarrow{\rho_{1}} & -x y \\
( -x ) y & \xrightarrow{\rho_{4}} & ( -x ) y + 0 \\
& \xrightarrow{\rho_{8}} & ( -x ) y + ( x_{8,2} + ( -x_{8,2} ) ) \\
& \xrightarrow{\rho_{10}} & ( ( -x ) y + y_{10,3} ) + ( -y_{10,3} ) \\
& \xrightarrow{\rho_{16}} & ( ( -x ) + y_{16,4} ) y + ( -y_{16,4} y ) \\
& \xrightarrow{\rho_{5}} & 0 y + ( -x y ) \\
& \xrightarrow{\rho_{19}} & 0 + ( -x y ) \\
& \xrightarrow{\rho_{1}} & -x y \\
\end{matrix} が成り立ちます。

\begin{cases}
\rho_{21} & = & ( & x, y & \mapsto & x (-y) & \to & -x y & ) \\
\rho_{22} & = & ( & x, y & \mapsto & -x y & \to & x (-y) & ) \\
\rho_{23} & = & ( & x, y & \mapsto & (-x) y & \to & -x y & ) \\
\rho_{24} & = & ( & x, y & \mapsto & -x y & \to & (-x) y & ) \\
\end{cases} を追加すると \begin{matrix}
( -x ) ( -y ) & \xrightarrow{\rho_{21}} & -( -x ) y \\
& \xrightarrow{\rho_{23}} & -( -x y ) \\
& \xrightarrow{\rho_{4}} & ( -( -x y ) ) + 0 \\
& \xrightarrow{\rho_{6}} & ( -( -x y ) ) + ( ( -x_{6,4} ) + x_{6,4} ) \\
& \xrightarrow{\rho_{10}} & ( ( -( -x y ) ) + ( -z_{10,5} ) ) + z_{10,5} \\
& \xrightarrow{\rho_{5}} & 0 + x y \\
& \xrightarrow{\rho_{1}} & x y \\
\end{matrix} が成り立ちます。

 \rho_{1} から  \rho_{20} に \begin{cases}
\rho_{21} & = & ( & x & \mapsto & 1 x & \to & x & ) \\
\rho_{22} & = & ( & x & \mapsto & x & \to & 1 x & ) \\
\rho_{23} & = & ( & x & \mapsto & x 1 & \to & x & ) \\
\rho_{24} & = & ( & x & \mapsto & x & \to & x 1 & ) \\
\end{cases} を追加すると \begin{matrix}
x + y & \xrightarrow{\rho_{4}} & ( x + y ) + 0 \\
& \xrightarrow{\rho_{8}} & ( x + y ) + ( x_{8,2} + ( -x_{8,2} ) ) \\
& \xrightarrow{\rho_{10}} & ( ( x + y ) + y_{10,3} ) + ( -y_{10,3} ) \\
& \xrightarrow{\rho_{9}} & ( x + ( y + z_{9,4} ) ) + ( -z_{9,4} ) \\
& \xrightarrow{\rho_{2}} & ( 0 + ( x + ( y + z_{9,4} ) ) ) + ( -z_{9,4} ) \\
& \xrightarrow{\rho_{6}} & ( ( ( -x_{6,6} ) + x_{6,6} ) + ( x + ( y + z_{9,4} ) ) ) + ( -z_{9,4} ) \\
& \xrightarrow{\rho_{9}} & ( ( -y_{9,7} ) + ( y_{9,7} + ( x + ( y + z_{9,4} ) ) ) ) + ( -z_{9,4} ) \\
& \xrightarrow{\rho_{10}} & ( ( -x_{10,8} ) + ( ( x_{10,8} + x ) + ( y + z_{9,4} ) ) ) + ( -z_{9,4} ) \\
& \xrightarrow{\rho_{22}} & ( ( -x_{10,8} ) + ( ( x_{10,8} + x ) + ( y + 1 x_{22,9} ) ) ) + ( -x_{22,9} ) \\
& \xrightarrow{\rho_{22}} & ( ( -x_{10,8} ) + ( ( x_{10,8} + x ) + ( 1 y + 1 x_{22,9} ) ) ) + ( -x_{22,9} ) \\
& \xrightarrow{\rho_{24}} & ( ( -x_{10,8} ) + ( ( x_{10,8} + x 1 ) + ( 1 y + 1 x_{22,9} ) ) ) + ( -x_{22,9} ) \\
& \xrightarrow{\rho_{14}} & ( ( -x_{10,8} ) + ( ( x_{10,8} + x 1 ) + 1 ( y + z_{14,12} ) ) ) + ( -z_{14,12} ) \\
& \xrightarrow{\rho_{14}} & ( ( -x y_{14,13} ) + ( x ( y_{14,13} + 1 ) + 1 ( y + z_{14,12} ) ) ) + ( -z_{14,12} ) \\
& \xrightarrow{\rho_{16}} & ( ( -x y ) + ( x + 1 ) ( y + 1 ) ) + ( -1 ) \\
& \xrightarrow{\rho_{13}} & ( ( -x y ) + ( ( x + 1 ) y + ( x + 1 ) 1 ) ) + ( -1 ) \\
& \xrightarrow{\rho_{15}} & ( ( -x y ) + ( ( x y + 1 y ) + ( x + 1 ) 1 ) ) + ( -1 ) \\
& \xrightarrow{\rho_{15}} & ( ( -x y ) + ( ( x y + 1 y ) + ( x 1 + 1 \cdot 1 ) ) ) + ( -1 ) \\
& \xrightarrow{\rho_{21}} & ( ( -x y ) + ( ( x y + y ) + ( x 1 + 1 \cdot 1 ) ) ) + ( -1 ) \\
& \xrightarrow{\rho_{23}} & ( ( -x y ) + ( ( x y + y ) + ( x + 1 \cdot 1 ) ) ) + ( -1 ) \\
& \xrightarrow{\rho_{21}} & ( ( -x y ) + ( ( x y + y ) + ( x + 1 ) ) ) + ( -1 ) \\
& \xrightarrow{\rho_{9}} & ( ( -x y ) + ( x y + ( y + ( x + 1 ) ) ) ) + ( -1 ) \\
& \xrightarrow{\rho_{10}} & ( ( ( -x y ) + x y ) + ( y + ( x + 1 ) ) ) + ( -1 ) \\
& \xrightarrow{\rho_{5}} & ( 0 + ( y + ( x + 1 ) ) ) + ( -1 ) \\
& \xrightarrow{\rho_{1}} & ( y + ( x + 1 ) ) + ( -1 ) \\
& \xrightarrow{\rho_{10}} & ( ( y + x ) + 1 ) + ( -1 ) \\
& \xrightarrow{\rho_{9}} & ( y + x ) + ( 1 + ( -1 ) ) \\
& \xrightarrow{\rho_{7}} & ( y + x ) + 0 \\
& \xrightarrow{\rho_{3}} & y + x \\
\end{matrix} が成り立ちます。

さらに \begin{cases}
\rho_{25} & = & ( & & \mapsto & 1 & \to & 0 & ) \\
\rho_{26} & = & ( & & \mapsto & 0 & \to & 1 & ) \\
\end{cases} を追加すると \begin{matrix}
x & \xrightarrow{\rho_{22}} & 1 x & \xrightarrow{\rho_{25}} & 0 x & \xrightarrow{\rho_{19}} & 0 \\
\end{matrix} が成り立ちます。

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

±マグマ

集合  M が二項演算  + と単項演算  - を持つとき  (M, +, -) を±マグマと呼ぶことにします。「単項・二項マグマ」と呼んでいましたが長いのでこう呼ぶことにします。ここでは、マグマに関する議論に演算を付け加えたものをまとめて説明していきます。

この議論に関する一般論があると思うのですが、ウェブで検索しても見つかりませんでした。「Universal Algebra for Computer Scientists」という本に少し書かれているようです。この本を持っているので今後読んでみたいと思います。「完備化」についてはWikipediaに「クヌース・ベンディックス完備化アルゴリズム」という記事があります。「完備化」についても今後調査したいと思います。

部分±マグマ

 (M, +, -) を±マグマとします。 X, Y \subseteq M に対して  X + Y = \{ x + y \mid x \in X, y \in Y \} - X = \{ - x \mid x \in X \} と書くことにします。 X \subseteq M X + X \subseteq X - X \subseteq X を満たすとき  X + - X への制限に関して±マグマとなります。このような  X M の部分±マグマと呼ぶことにします。

±マグマの準同型

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

  •  f(x + y) = f(x) \oplus f(y)
  •  f(- x) = \ominus f(x)

を満たすとき、 f を±マグマ  (M. +, -) から±マグマ  (M', \oplus, \ominus) への±マグマの準同型と呼びます。

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

 X を±マグマ  M の部分集合とします。 N \subseteq M に対して、 N X を含む  M の部分マグマであり、 X を含む  M の部分±マグマの最小のものであるとき、 N X で生成された  M の部分±マグマと呼ぶことにします。±マグマ  M X で生成された  M の部分±マグマであるとき  M X で生成された±マグマと呼ぶことにします。

 \displaystyle \bigcap \{ N \mid N \ は \ X \ を含む \ M \ の部分±マグマ \} X で生成された  M の部分±マグマとなります。

±マグマの「多項式

±マグマと  M と集合  X の元に、「  (\!\!(」、「 )\!\!)」、「 \oplus」、「 \ominus」をを付け加えたものからなる、有限個の列全体の集合を  S(M, X) とします。

 a \in M だけの長さ  1 の列を  [a] とし、 M' = \{ [a] \mid a \in M\} とします。同様に  x \in X だけの長さ  1 の列を  [x] とし、 X' = \{ [x] \mid x \in X\} とします。 \alpha \in M' に対して  \alpha = [a] となる  a \grave{\alpha} とします。

 S(M, X) に二項演算  \boxplus: S(M, X) \times S(M, X) \to S(M, X) を \begin{cases}
α \boxplus β = [\grave{α} + \grave{β}] & (α, β \in M' \ のとき) \\
α \boxplus β = (\!\!(α \oplus β)\!\!) & (それ以外のとき) \\
\end{cases}、単項演算  \boxminus: S(M, X) \times S(M, X) を \begin{cases}
\boxminus α = [- \grave{α}] & (α \in M' \ のとき) \\
\boxminus α = (\!\!(\ominus α)\!\!) & (それ以外のとき) \\
\end{cases} と定義すると  (S(M, X), \boxplus, \boxminus) は±マグマとなります。

 M' \cup X' で生成された  (S(M, X), \boxplus, \boxminus) の部分±マグマを  M[X] と書くことにします。 M[X] の演算を  + - と書くことにします。以下では  M' M X' X と書きます。

多項式」からの写像の準同型への拡張

 (M[X], +, -) の台集合  M[X] の部分集合  B に対して \begin{cases}
B^{\pm(1)} = B \\
B^{\pm(n+1)} = (B^{\pm(n)} + B^{\pm(n)}) \cup (- B^{\pm(n)}) \\
\end{cases} と帰納的に  B^{\pm(n)} を定義します。 \displaystyle M[X] = \bigcup_{n \in \mathbb{N}} (M \cup X)^{\pm(n)} となります。

 (M', +, -) を±マグマ、 g: M \sqcup X \to M'単射( M \sqcup X は集合の直和)、 g M への制限が±マグマの準同型であるとします。

 \alpha \in M[X] に対して  \displaystyle n_\alpha = \min \{ n \in \mathbb{N} \mid \alpha \in \bigcup_{k \le n} (M \cup X)^{\pm(k)} \} が存在します。 \alpha \in M \cup X または  \alpha = \beta + \gamma となる  \displaystyle \beta, \gamma \in \bigcup_{k \le n_\alpha-1} (M \cup X)^{\pm(k)} が存在する( \alpha \in M[X]^+ とします)か、または  \alpha = - \beta となる  \displaystyle \beta \in \bigcup_{k \le n_\alpha-1} (M \cup X)^{\pm(k)} が存在します( \alpha \in M[X]^- とします)。\begin{cases}
g^*(\alpha) = g(\alpha) & (\alpha \in M \cup X \ のとき) \\
g^*(\alpha) = g^*(\beta) + g^*(\gamma) & (\alpha \in M[X]^+, \alpha = \beta + \gamma \ のとき) \\
g^*(\alpha) = - g^*(\beta) & (\alpha \in M[X]^-, \alpha = - \beta \ のとき) \\
\end{cases} と帰納的に定義することにより、±マグマの準同型  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]^+ に対して、 \alpha = \alpha_L + \alpha_R となる  \alpha_L, \alpha_R が一意的に存在します。 \alpha \alpha_L に写す写像 L: M[X]^+ \to M[X] \alpha \alpha_R に写す写像 R: M[X]^+ \to M[X] と定義することができます。 \alpha \notin M[X]^+ のときは  M[X] に含まれない元  \bot (失敗を表す)を追加した  M[X] \sqcup \{\bot\} を考え、 L(\alpha) = R(\alpha) = \bot と定義することによってこれらを拡張して、 L, R: M[X] \to M[X] \sqcup \{\bot\} とします。さらに  L(\bot) = R(\bot) = \bot と定義することによって拡張して、 L, R: M[X] \sqcup \{\bot\} \to M[X] \sqcup \{\bot\} とします。

同様に、 \alpha \in M[X]^- に対して、 \alpha = - \alpha_B となる  \alpha_B が一意的に存在します。 \alpha \alpha_B に写す写像 B: M[X]^- \to M[X] と定義することができます。 \alpha \notin M[X]^- のときは  B(\alpha) = \bot と定義することによって拡張して、 B: M[X] \to M[X] \sqcup \{\bot\} とします。さらに  B(\bot) = \bot と定義することによって拡張して、 B: M[X] \sqcup \{\bot\} \to M[X] \sqcup \{\bot\} とします。

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

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

 \displaystyle M[X] = \bigcup_{n \in \mathbb{N}} (M \cup X)^{(n)} であることから  \displaystyle n_\alpha = \min \{ n \in \mathbb{N} \mid \alpha \in \bigcup_{k \le n} (M \cup X)^{(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 β) + R(α) & (n>0, δ_1 = L) \\
L(α) + R(α)(δ_2 \cdots δ_n \gets β) & (n>0, δ_1 = R) \\
- B(α)(δ_2 \cdots δ_n \gets β) & (n>0, δ_1 = B) \\
\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]) を書き換え後の項と呼ぶことにします。これを \begin{eqnarray*}
α & \xrightarrow{ρ, σ, p} & α(p \gets γ[σ])
\end{eqnarray*} または \begin{eqnarray*}
α & \xrightarrow{ρ} & α(p \gets γ[σ])
\end{eqnarray*} と書くことにします。

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

環の性質

「群の性質」で考えた「単項・二項マグマ」に二項演算を付け加えたものを考えます。これをここでは「単項・二項・二項マグマ」と呼ぶことにします。「単項・二項・二項マグマ」について「代入」を考えることで「群の性質」と同様に環で成り立つ関係を求めることができます。

Ring でこの式の変形ができるようになっているのですが、群の場合と違って半自動的にできるようになっていないので、式の変形のやり方がわかっていないとできません。以下で説明します。

環の定義から得られる関係

集合  R に二つの二項演算  x+y (加法)、 xy (乗法)が定義されていて、 次の条件が成り立っているとき、 R は環であるといいます。

  1. 加法に関して可換群である。 すなわち
    1.  (x + y) + z = x + (y + z) (結合法則)(associative law) が成り立つ。
    2.  x + y = y + x (交換法則)(commutative law) が成り立つ。
    3. ある  R の元  0 が存在して、すべての  R の元  x に対し  0 + x = x + 0 = x が成り立つ。 0 R の零元(zero element)という。
    4. すべての  R の元  x に対して、 R の元  y が存在して  y + x = x + y = 0 が成り立つ。  y - x と書く。
  2. 乗法に関して結合法則が成り立つ。すなわち  (xy)z = x(yz) が成り立つ。
  3. 分配法則(distributive law)が成り立つ。すなわち
    1.  x(y + z) = xy + xz
    2.  (x + y)z = xz + yz

 R の乗法に関する単位元を単に単位元と呼びます。単位元 1 と書きます。以下の関係が成り立ちます。

  •  x0 = x(0 + 0) = x0 + x0
  •  x0 = x0 + (x0 + (- x0)) = (x0 + x0) + (- x0) = x0 + (- x0) = 0
  •  0x = (0 + 0)x = 0x + 0x
  •  0x = 0x + (0x + (- 0x)) = (0x + 0x) + (- 0x) = 0x + (- 0x) = 0
  •  x(-y) + xy = x( (-y) + y) = x0 = 0
  •  x(-y) = x(-y) + 0 = x(-y) + (xy + (-xy)) \\ = (x(-y) + xy) + (-xy) = 0 + (-xy) = -xy
  •  (-x)y + xy = ( (-x) + x)y = 0y = 0
  •  (-x)y = (-x)y + 0 = (-x)y + (xy + (-xy)) \\ = ( (-x)y + xy) + (-xy) = 0 + (-xy) = -xy
  •  -(-x) = (-(-x)) + 0 = (-(-x)) + ( (-x) + x) \\ = ( (-(-x)) + (-x) ) + x = 0 + x = x
  •  (-x)(-y) = -(-x)y = -(-xy) = xy
  •  (x + 1)(y + 1) = (x + 1)y + (x + 1)1 = (xy + 1y) + (x1 + 1\cdot 1) \\ = (xy + y) + (x + 1)
  •  (x + 1)(y + 1) + (-1) = ( (xy + y) + (x + 1) ) + (-1) \\ = ( ( (xy + y) + x ) + 1) + (-1) = ( (xy + y) + x ) + (1 + (-1)) \\ = ( (xy + y) + x ) + 0 = (xy + y) + x
  •  (-xy) + ( (x + 1)(y + 1) + (-1) ) = (-xy) + ( (xy + y) + x) \\ = (-xy) + (xy +( y + x)) = ( (-xy) + xy ) +( y + x) \\ = 0 + (y + x) = y + x
  •  (x + 1)(y + 1) = x(y + 1) + 1(y + 1) = (xy + x1) + (1y + 1\cdot 1) \\ = (xy + x) + (y + 1)
  •  (x + 1)(y + 1) + (-1) = ( (xy + x) + (y + 1) ) + (-1) \\ = ( ( (xy + x) + y ) + 1) + (-1) = ( (xy + x) + y ) + (1 + (-1)) \\ = ( (xy + x) + y ) + 0 = (xy + x) + y
  •  (-xy) + ( (x + 1)(y + 1) + (-1) ) = (-xy) + ( (xy + x) + y) \\ = (-xy) + (xy +( x + y)) = ( (-xy) + xy ) +( x + y) \\ = 0 + (x + y) = x + y
  •  x + y = (-xy) + ( (x + 1)(y + 1) + (-1) ) = y + x
  •  x = 1x = 0x = 0

これは長くてわかりにくいので、加法の結合法則  (x + y) + z = x + (y + z) が成り立つことを考慮して  (x + y) + z = x + (y + z) x + y + z と書くことにして書き直すと

  •  x0 = x(0 + 0) = x0 + x0
  •  x0 = x0 + x0 + (- x0) = x0 + (- x0) = 0
  •  0x = (0 + 0)x = 0x + 0x
  •  0x = 0x + 0x + (- 0x) = 0x + (- 0x) = 0
  •  x(-y) + xy = x( (-y) + y) = x0 = 0
  •  x(-y) = x(-y) + 0 = x(-y) + xy + (-xy) = 0 + (-xy) = -xy
  •  (-x)y + xy = ( (-x) + x)y = 0y = 0
  •  (-x)y = (-x)y + 0 = (-x)y + xy + (-xy) = 0 + (-xy) = -xy
  •  -(-x) = (-(-x)) + 0 = (-(-x)) + (-x) + x = 0 + x = x
  •  (-x)(-y) = -(-x)y = -(-xy) = xy
  •  (x + 1)(y + 1) = (x + 1)y + (x + 1)1 = xy + 1y + x1 + 1\cdot 1 = xy + y + x + 1
  •  (x + 1)(y + 1) + (-1) = xy + y + x + 1 + (-1) = xy + y + x + 0 = xy + y + x
  •  (-xy) + (x + 1)(y + 1) + (-1) = (-xy) + xy + y + x = 0 + y + x = y + x
  •  (x + 1)(y + 1) = x(y + 1) + 1(y + 1) = xy + x1 + 1y + 1\cdot 1 = xy + x + y + 1
  •  (x + 1)(y + 1) + (-1) = xy + x + y + 1 + (-1) = xy + x + y + 0 = xy + x + y
  •  (-xy) + (x + 1)(y + 1) + (-1) = (-xy) + xy + x + y = 0 + x + y = x + y
  •  x + y = (-xy) + (x + 1)(y + 1) + (-1) = y + x
  •  x = 1x = 0x = 0

となります。よって

  • 環の定義(加法の交換法則を除く)から、 x0 = 0x = 0 x(-y) = (-x)y = -xy (-x)(-y) = xy が成り立ちます。
  • 環の定義(加法の交換法則を除く)と単位元の存在から、 x + y = y + x が成り立ちます。
  • 環の定義(加法の交換法則を除く)と単位元の存在から、 1 = 0 ならば任意の  x \in R に対して  x = 0 が成り立ちます。
「単項・二項・二項マグマ」の「代入」による方法

「単項・二項・二項マグマ」の「代入」による式の変形によってこの関係を求めることができます。\begin{cases}
\rho_{1} & = & ( & x & \mapsto & 0 + x & \to & x & ) \\
\rho_{2} & = & ( & x & \mapsto & x & \to & 0 + x & ) \\
\rho_{3} & = & ( & x & \mapsto & x + 0 & \to & x & ) \\
\rho_{4} & = & ( & x & \mapsto & x & \to & x + 0 & ) \\
\rho_{5} & = & ( & x & \mapsto & (-x) + x & \to & 0 & ) \\
\rho_{6} & = & ( & x & \mapsto & 0 & \to & (-x) + x & ) \\
\rho_{7} & = & ( & x & \mapsto & x + (-x) & \to & 0 & ) \\
\rho_{8} & = & ( & x & \mapsto & 0 & \to & x + (-x) & ) \\
\rho_{9} & = & ( & x, y, z & \mapsto & (x + y) + z & \to & x + (y + z) & ) \\
\rho_{10} & = & ( & x, y, z & \mapsto & x + (y + z) & \to & (x + y) + z & ) \\
\rho_{11} & = & ( & x, y, z & \mapsto & (x y) z & \to & x (y z) & ) \\
\rho_{12} & = & ( & x, y, z & \mapsto & x (y z) & \to & (x y) z & ) \\
\rho_{13} & = & ( & y, x, z & \mapsto & x (y + z) & \to & x y + x z & ) \\
\rho_{14} & = & ( & x, y, z & \mapsto & x y + x z & \to & x (y + z) & ) \\
\rho_{15} & = & ( & x, y, z & \mapsto & (x + y) z & \to & x z + y z & ) \\
\rho_{16} & = & ( & x, y, z & \mapsto & x z + y z & \to & (x + y) z & ) \\
\end{cases} から \begin{matrix}
x 0 & \xrightarrow{\rho_{4}} & x 0 + 0 & \xrightarrow{\rho_{8}} & x 0 + ( x_{8,2} + ( -x_{8,2} ) ) \\ & \xrightarrow{\rho_{10}} & ( x 0 + y_{10,3} ) + ( -y_{10,3} ) & \xrightarrow{\rho_{14}} & x ( 0 + z_{14,4} ) + ( -x z_{14,4} ) \\ & \xrightarrow{\rho_{1}} & x x_{1,5} + ( -x x_{1,5} ) & \xrightarrow{\rho_{7}} & 0 \\
0 x & \xrightarrow{\rho_{4}} & 0 x + 0 & \xrightarrow{\rho_{8}} & 0 x + ( x_{8,2} + ( -x_{8,2} ) ) \\ & \xrightarrow{\rho_{10}} & ( 0 x + y_{10,3} ) + ( -y_{10,3} ) & \xrightarrow{\rho_{16}} & ( 0 + y_{16,4} ) x + ( -y_{16,4} x ) \\ & \xrightarrow{\rho_{1}} & x_{1,5} x + ( -x_{1,5} x ) & \xrightarrow{\rho_{7}} & 0 \\
\end{matrix} が得られます。この続きは次回以降で説明したいと思います。

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

群の性質(2)

今回は群の性質の続きを調べていきます。

前回の結果

「エレファントな群とリー代数(3)」では書き換え規則の集合  \rho_1 - \rho_{10} \begin{cases}
\rho_{1} & = & ( & x & \mapsto & e x & \to & x & ) \\
\rho_{2} & = & ( & x & \mapsto & x & \to & e x & ) \\
\rho_{3} & = & ( & x & \mapsto & x^{-1} x & \to & e & ) \\
\rho_{4} & = & ( & x & \mapsto & e & \to & x^{-1} x & ) \\
\rho_{5} & = & ( & x, y, z & \mapsto & (x y) z & \to & x (y z) & ) \\
\rho_{6} & = & ( & x, y, z & \mapsto & x (y z) & \to & (x y) z & ) \\
\rho_{7} & = & ( & x & \mapsto & e^{-1} x & \to & x & ) \\
\rho_{8} & = & ( & x & \mapsto & x & \to & e^{-1} x & ) \\
\rho_{9} & = & ( & x & \mapsto & (e^{-1})^{-1} x & \to & x & ) \\
\rho_{10} & = & ( & x & \mapsto & x & \to & (e^{-1})^{-1} x & ) \\
\end{cases} により  \rho_1 - \rho_6 から \begin{matrix}
e^{-1} x & \xrightarrow{\rho_{2}} & e^{-1} (e x) & \xrightarrow{\rho_{6}} & (e^{-1} e) x & \xrightarrow{\rho_{3}} & e x & \xrightarrow{\rho_{1}} & x \\
\end{matrix}  \rho_1 - \rho_8 から \begin{matrix}
(e^{-1})^{-1} x & \xrightarrow{\rho_{8}} & (e^{-1})^{-1} (e^{-1} x) & \xrightarrow{\rho_{6}} & ((e^{-1})^{-1} e^{-1}) x & \xrightarrow{\rho_{3}} & e x & \xrightarrow{\rho_{1}} & x \\
\end{matrix}  \rho_1 - \rho_{10} から \begin{matrix}
e^{-1} & \xrightarrow{\rho_{10}} & (e^{-1})^{-1} e^{-1} & \xrightarrow{\rho_{3}} & e \\
\end{matrix} が得られました。

前回の続き

以下の規則を付け加えます。\begin{cases}
\rho_{11} & = & ( & & \mapsto & e^{-1} & \to & e & ) \\
\rho_{12} & = & ( & & \mapsto & e & \to & e^{-1} & ) \\
\rho_{13} & = & ( & x & \mapsto & (x^{-1})^{-1} e & \to & x & ) \\
\rho_{14} & = & ( & x & \mapsto & x & \to & (x^{-1})^{-1} e & ) \\
\rho_{15} & = & ( & x & \mapsto & (x^{-1})^{-1} & \to & x & ) \\
\rho_{16} & = & ( & x & \mapsto & x & \to & (x^{-1})^{-1} & ) \\
\rho_{17} & = & ( & x & \mapsto & x x^{-1} & \to & e & ) \\
\rho_{18} & = & ( & x & \mapsto & e & \to & x x^{-1} & ) \\
\rho_{19} & = & ( & x & \mapsto & x e & \to & x & ) \\
\rho_{20} & = & ( & x & \mapsto & x & \to & x e & ) \\
\rho_{21} & = & ( & x, y & \mapsto & (x y)^{-1} x & \to & y^{-1} & ) \\
\rho_{22} & = & ( & y, x & \mapsto & y^{-1} & \to & (x y)^{-1} x & ) \\
\end{cases}  \rho_1 - \rho_6 から \begin{matrix}
( x^{-1} )^{-1} e & \xrightarrow{\rho_{4}} & ( x^{-1} )^{-1} ( x_{4,0}^{-1} x_{4,0} ) & \xrightarrow{\rho_{6}} & ( ( x^{-1} )^{-1} z_{6,1}^{-1} ) z_{6,1} & \xrightarrow{\rho_{3}} & e x & \xrightarrow{\rho_{1}} & x \\
\end{matrix}  \rho_1 - \rho_{14} から \begin{matrix}
( x^{-1} )^{-1} & \xrightarrow{\rho_{14}} & ( ( ( x^{-1} )^{-1} )^{-1} )^{-1} e & \xrightarrow{\rho_{2}} & ( ( ( x^{-1} )^{-1} )^{-1} )^{-1} ( e e ) \\ & \xrightarrow{\rho_{6}} & ( ( ( ( x^{-1} )^{-1} )^{-1} )^{-1} e ) e & \xrightarrow{\rho_{13}} & ( x^{-1} )^{-1} e & \xrightarrow{\rho_{13}} & x \\
\end{matrix}  \rho_1 - \rho_{16} から \begin{matrix}
x x^{-1} & \xrightarrow{\rho_{16}} & ( x^{-1} )^{-1} x^{-1} & \xrightarrow{\rho_{3}} & e \\
x e & \xrightarrow{\rho_{16}} & ( x^{-1} )^{-1} e & \xrightarrow{\rho_{13}} & x \\
\end{matrix}  \rho_1 - \rho_{20} から \begin{matrix}
( x y )^{-1} x & \xrightarrow{\rho_{20}} & ( x y )^{-1} ( x e ) & \xrightarrow{\rho_{18}} & ( x y )^{-1} ( x ( x_{18,1} x_{18,1}^{-1} ) ) \\ & \xrightarrow{\rho_{6}} & ( x y )^{-1} ( ( x y_{6,2} ) y_{6,2}^{-1} ) & \xrightarrow{\rho_{6}} & ( ( x y )^{-1} ( x y_{6,2} ) ) y_{6,2}^{-1} \\ & \xrightarrow{\rho_{3}} & e y^{-1} & \xrightarrow{\rho_{1}} & y^{-1} \\
\end{matrix}  \rho_1 - \rho_{21} から \begin{matrix}
( x y )^{-1} & \xrightarrow{\rho_{20}} & ( x y )^{-1} e & \xrightarrow{\rho_{18}} & ( x y )^{-1} ( x_{18,1} x_{18,1}^{-1} ) \\ & \xrightarrow{\rho_{6}} & ( ( x y )^{-1} y_{6,2} ) y_{6,2}^{-1} & \xrightarrow{\rho_{21}} & y^{-1} x^{-1} \\
\end{matrix} が得られます。これで群の完備化で書いた関係が得られました。