エレファント・コンピューティング調査報告

極限に関する順序を論理プログラミングの手法を使って指定することを目指すブロクです。

論理計算と随伴関手(2)

随伴関手の説明をする前に自由群などについて説明をしておきます。

半群・モノイド・群の定義

集合  S と結合律を満たす二項演算(積と呼びます)  \cdot : S \times S \rightarrow S の組  (S, \cdot ) 半群と言います。単位元を持つ半群をモノイドと呼びます。モノイドが任意の元に対して逆元を持つとき群と呼びます。

自由半群・自由モノイド・自由群

文字の集合  S に対して、 S の元の1個以上の有限個からなる文字列全体の集合を  S^* とおきます。 S^* は文字列の連結を演算として半群になります。これを自由半群と呼びます。
自由半群に対して、以下の自由半群の普遍性が成り立ちます。 G半群 f: S \rightarrow G を任意の写像とすると、 f を拡張した( S上では一致する)半群の準同型(積を保存する写像)  \widetilde{f} : S^* \rightarrow G を( x_1, x_2, \cdots, x_n という文字列に  f(x_1)f(x_2) \cdots f(x_n) を対応させることにより)定義することができます。

自由半群の定義で、0個の文字からなる文字列も許すとすると、 S^* は0個の文字からなる文字列を単位元とするモノイドとなります。これを自由モノイドと呼びます。
自由モノイドに対して、以下の自由モノイドの普遍性が成り立ちます。 G をモノイド、 f: S \rightarrow G を任意の写像とすると、 f を拡張した( S上では一致する)モノイドの準同型(積と単位元を保存する写像)  \widetilde{f} : S^* \rightarrow G半群の場合と同様に定義することができます。

文字の集合  S に対して、 X = S + S (集合の直和)を考えます。 X の元の0個以上の有限個からなる文字列全体の集合を  X^* とおきます。 X^* は文字列の連結を演算としてモノイドになります。 X = S + S の元を区別するために  X = S \cup S' と書くことにして、 x \in S に対応する  S' の元を  x' と書くことにします( h: X \rightarrow X x \in S x' \in S' x' \in S' x \in S に写す写像とします)。 X^* の元  y z X の元  x に対して  yz yxh(x)z を対応させることの反射推移閉包による  X^* の同値類を  \widetilde{X} とおき、 X^* の元をその同値類に写す写像 g: X^* \rightarrow \widetilde{X} とおきます。 X^* の元  y z に対して  \widetilde{X} の積を  g(y)g(z) = g(yz) と定義すると  g(x_1 x_2 \cdots x_n) の逆元は  g(h(x_n) h(x_{n-1}) \cdots h(x_1)) となって  \widetilde{X} は群となります。これを自由群と呼びます。

自由群に対して、以下の自由群の普遍性が成り立ちます。 G を群、 f: S \rightarrow G を任意の写像とすると、 f を拡張した( S上では一致する)群の準同型(積と単位元を保存する写像)  \widetilde{f} : \widetilde{X} \rightarrow G を以下のように定義することができます。
 f を拡張した  f_2: X \rightarrow G x \in S' に対して  f_2(x) = f(h(x))^{-1} と定義します。  \widetilde{X} の元  g(x_1 x_2 \cdots x_n) ( x_1, x_2, \cdots, x_n \in X) に対して  \widetilde{f}(g(x_1 x_2 \cdots x_n)) = f_2(x_1)f_2(x_2) \cdots f_2(x_n) と定義します。