グループ（群）、サブグループ（部分群）、サブグループ（部分群）の左または右コセット（剰余類）たちクオシエント（商）セット（集合）に対して、サブセット（部分集合）のクラシフィケーションマップ（クラス分け写像）後にプリイメージ（前像）を取るコンポジション（合成）は、サブグループ（部分群）に左または右からサブセット（部分集合）を掛けたものであることの記述/証明
話題
About: グループ（群）
この記事の目次
開始コンテキスト
ターゲットコンテキスト
- 読者は、任意のグループ（群）、任意のサブグループ（部分群）、当該サブグループ（部分群）の左または右コセット（剰余類）たちクオシエント（商）セット（集合）に対して、任意のサブセット（部分集合）のクラシフィケーションマップ（クラス分け写像）後にプリイメージ（前像）を取るコンポジション（合成）は、当該サブグループ（部分群）に左または右から当該サブセット（部分集合）を掛けたものであるという命題の記述および証明を得る。
オリエンテーション
本サイトにてこれまで議論された定義たちの一覧があります。
本サイトにてこれまで議論された命題たちの一覧があります。
本体
1: 構造化された記述
ここに'構造化された記述'のルールたちがある。
エンティティ（実体）たち:
\(G'\): \(\in \{\text{ 全てのグループ（群）たち }\}\)
\(G\): \(\in \{G' \text{ の全てのサブグループ（部分群）たち }\}\)
\(G' / \sim_{G, l}\): \(= G' \text{ の } G \text{ の左コセット（剰余類）たちクオシエント（商）セット（集合） }\)
\(G' / \sim_{G, r}\): \(= G' \text{ の } G \text{ の右コセット（剰余類）たちクオシエント（商）セット（集合） }\)
\(f_l\): \(: G' \to G' / \sim_{G, l}\), \(= \text{ 当該クラシフィケーションマップ（クラス分け写像） }\)
\(f_r\): \(: G' \to G' / \sim_{G, r}\), \(= \text{ 当該クラシフィケーションマップ（クラス分け写像） }\)
\(S'\): \(\subseteq G'\)
//
ステートメント（言明）たち:
\({f_l}^{- 1} \circ f_l (S') = S' G\)
\(\land\)
\({f_r}^{- 1} \circ f_r (S') = G S'\)
//
2: 注
\(G' / \sim_{G, l}\)および\(G' / \sim_{G, r}\)の各々は、グループ（群）やトポロジカルスペース（空間）ではなく、単にあるセット（集合）である、一般には: \(G\)があるノーマルサブグループ（正規部分群）でない限り、\(G' / \sim_{G, l}\)はグループ（群）ではない、任意のグループ（群）および任意のサブグループ（部分群）に対して、同一コセット（剰余類）内にいることによるクウォシェント（商）セット（集合）はグループ（群）である、当該サブグループ（部分群）はノーマルサブグループ（正規部分群）である場合に限って、という命題によって、そして、\(G'\)はトポロジーを持たないので、当該クウォシェント（商）セット（集合）には当該クウォシェント（商）トポロジーを与えることができない。
しかし、いずれにせよ、\(G' / \sim_{G, l}\)および\(G' / \sim_{G, r}\)の各々は妥当である、任意のグループ（群）および任意のサブグループ（部分群）に対して、同一コセット（剰余類）内にいることはイクイバレンスリレーション（同値関係）であるという命題によって。
3: Proof
Whole Strategy: Step 1: see that for each \(g' \in {f_l}^{- 1} \circ f_l (S')\), \(g' \in S' G\), and for each \(g' \in S' G\), \(g' \in {f_l}^{- 1} \circ f_l (S')\); Step 2: see that for each \(g' \in {f_r}^{- 1} \circ f_r (S')\), \(g' \in G S'\), and for each \(g' \in G S'\), \(g' \in {f_r}^{- 1} \circ f_r (S')\).
Step 1:
Let \(g' \in {f_l}^{- 1} \circ f_l (S')\) be any.
\(f_l (g') \in f_l (S')\).
\(f_l (g') = g' G \in f_l (S')\).
So, \(g' G = f_l (s') = s' G\) for an \(s' \in S'\).
\(g' \in s' G\), by the proposition that with respect to any subgroup, the coset by any element of the group equals a coset if and only if the element is a member of the latter coset, whether they are left cosets or right cosets.
So \(g' \in S' G\).
So, \({f_l}^{- 1} \circ f_l (S') \subseteq S' G\).
Let \(g' \in S' G\) be any.
\(g' = s' g\) for an \(s' \in S'\) and a \(g \in G\).
\(f_l (g') = s' g G = s' G\), because \(s' g \in s' G\), and the proposition that with respect to any subgroup, the coset by any element of the group equals a coset if and only if the element is a member of the latter coset, whether they are left cosets or right cosets applies, \(\in f_l (S')\).
So, \(g' \in {f_l}^{- 1} \circ f_l (S')\).
So, \(S' G \subseteq {f_l}^{- 1} \circ f_l (S')\).
So, \({f_l}^{- 1} \circ f_l (S') = S' G\).
Step 2:
Let \(g' \in {f_r}^{- 1} \circ f_r (S')\) be any.
\(f_r (g') \in f_r (S')\).
\(f_r (g') = G g' \in f_r (S')\).
So, \(G g' = f_r (s') = G s'\) for an \(s' \in S'\).
\(g' \in G s'\), by the proposition that with respect to any subgroup, the coset by any element of the group equals a coset if and only if the element is a member of the latter coset, whether they are left cosets or right cosets.
So \(g' \in G S'\).
So, \({f_r}^{- 1} \circ f_r (S') \subseteq G S'\).
Let \(g' \in G S'\) be any.
\(g' = g s'\) for an \(s' \in S'\) and a \(g \in G\).
\(f_r (g') = G g s' = G s'\), because \(g s' \in G s'\), and the proposition that with respect to any subgroup, the coset by any element of the group equals a coset if and only if the element is a member of the latter coset, whether they are left cosets or right cosets applies, \(\in f_r (S')\).
So, \(g' \in {f_r}^{- 1} \circ f_r (S')\).
So, \(G S' \subseteq {f_r}^{- 1} \circ f_r (S')\).
So, \({f_r}^{- 1} \circ f_r (S') = G S'\).
