逆元による群と除法による群

群の公理について

群の公理は通常は各元が逆元を持つモノイドとして与えられます。逆元から乗法の逆の演算である除法を定義することができます。たとえば、整数の引き算は符号を反転した数を足すという演算として導入できます。これの逆を考えることはできないでしょうか。つまり、除法を持つモノイドとして群を考えて、逆元を除法から考えるということです。
　それは可能です。この記事では、２つの群の公理の定式化を行い、それが同値であることを示します。

２つの群の公理

まず、通常の群の公理から確認します。

逆元による群の公理

集合Gは次のような二項演算・と定数eを持つ。
・乗法は結合的
\[ x \cdot (y \cdot z) = (x \cdot y) \cdot z \]
・eは単位元
\[ x \cdot e = x = e \cdot x\]
・逆元の存在
\[x^{-1} \cdot x = e = x \cdot x^{-1} \]
　ただし、x、y、zはGの任意の元です。
　これに代わると思われる除法による群の公理は次のようなものです。

除法による群の公理

集合Gは次のような二項演算・と二項演算／と定数eを持つ。
・乗法は結合的
\[ x \cdot (y \cdot z) = (x \cdot y) \cdot z \]
・eは単位元
\[ x \cdot e = x = e \cdot x\]
・除法は乗法の逆演算
\[ (x \cdot y) / y = x = (x / y) \cdot y \]
・乗法と除法は結合的
\[ (x \cdot y) / z = x \cdot (y / z) \]
　ただし、x、y、zはGの任意の元です。

　逆元の条件の部分が、除法について２つの条件に置き換わりました。また、逆演算という言葉については、次を参照してください。

• 逆演算について



2つの公理が同じ代数を与えること

この２つの公理が同じ代数の定義を与えることを示しましょう。次の２つを行います。

（１）逆元による群から除法を定義して、それが除法の条件を満たすことを確かめる。

（２）除法による群から逆元を定義して、それが逆元の条件を満たすことを確かめる。

　

（１）

　Gを逆元による群の公理を満たす代数であるとします。

除法の定義

G上で次のような二項演算／を定義します。

\[ x / y = x \cdot y^{-1}\]

　これが除法の条件を満たすことを示しましょう。

逆演算であること

\[ (x \cdot y) / y = x =  (x / y) \cdot y\]

　左辺と右辺がそれぞれxに等しくなることを示します。

左辺

\[\begin{eqnarray*} (x \cdot y) / y &=& (x \cdot y) \cdot y^{-1} \\ &=& x \cdot (y \cdot y^{-1}) \\ &=& x \cdot e \\ &=& x \end{eqnarray*}\]

右辺

\[\begin{eqnarray*} (x / y) \cdot y &=& (x \cdot y^{-1}) \cdot y \\ &=& x \cdot (y^{-1} \cdot y) \\ &=& x \cdot e \\ &=& x \end{eqnarray*}\]

結合的であること

\[ (x \cdot y) / z = x \cdot (y / z) \]

　左辺が右辺と等しくなることを示します。

\[\begin{eqnarray*} (x \cdot y) / z &=& (x \cdot y) \cdot z^{-1} \\ &=& x \cdot (y \cdot z^{-1}) \\ &=& x \cdot  (y / z) \end{eqnarray*}\]

　以上で（１）は達成されました。

（２）

　Gを除法による群を満たす代数であるとします。

逆元の定義

各元xに対してx^-1を次のように定義します。
\[ x^{-1} = e / x\]

　これが逆元の条件を満たすことを示します。

逆元の条件

\[x^{-1} \cdot x = e = x \cdot x^{-1} \]

　左辺と右辺がそれぞれeと等しくなることを確かめます。

左辺
\[\begin{eqnarray*} x^{-1} \cdot x &=& (e / x) \cdot x \\ &=& e \end{eqnarray*}\]

右辺

\[\begin{eqnarray*} x \cdot x^{-1} &=& x \cdot (e / x) \\ &=& (x \cdot e) / x \\ &=& (e \cdot x) / x  \\ &=& e \end{eqnarray*}\]

　以上で（２）が達成されたので、２つの群の公理が同値であることを確かめられました。

除法による群の公理について

　通常は除法による群の公理というのは行われません。私の調べる限りでは、そのような仕事を見つけることはできなかったので、以上の公理化は自前で行いました。このような仕事がなかった背景には、需要がないこと、逆元に比べて複雑であること、この２つが主要であると思われます。この２つの状況について、この公理が持っている可能性について説明しましょう。
　まず、需要についてですが、この公理化の意義を説明することで回答になるでしょう。これは群を構成するときに有効です。たとえば、ある集合から自由群を生成する場合にそれが群であることを確かめるときに、除法の公理を確かめるほうが簡単です。自然数から整数を構成する場合も同様です。
　別の記事で、符号付き文字列というものを与える予定です。文字集合から再帰的な定義により与えた自由群です。これが群であることを示すために、演算を定義するのですが、再帰的に与えた場合は、除法の方が先に出てきます。また、その証明も除法による群の公理のほうが容易です。
　次に、その複雑さについてですが、逆演算はコモナドの視点からかなり自然に定式化できます。それについては先程も参照を与えましたが、次の記事で示しています。

• 逆演算について

これにより、合成して単位元になるという形で逆演算というものを定義できます。