ベーシス（基底）を持つモジュール（加群）に対して、要素のベーシス（基底）に関するコンポーネントたちセット（集合）はユニークであることの記述/証明
話題
About: モジュール（加群）
この記事の目次
開始コンテキスト
- 読者は、モジュール（加群）のベーシス（基底）の定義を知っている。
ターゲットコンテキスト
- 読者は、任意のベーシス（基底）を持つ任意のモジュール（加群）に対して、任意の要素の当該ベーシス（基底）に関するコンポーネントたちセット（集合）はユニークであるという命題の記述および証明を得る。
オリエンテーション
本サイトにてこれまで議論された定義たちの一覧があります。
本サイトにてこれまで議論された命題たちの一覧があります。
本体
1: 構造化された記述
ここに'構造化された記述'のルールたちがある。
エンティティ（実体）たち:
\(R\): \(\in \{\text{ 全てのリング（環）たち }\}\)
\(M\): \(\in \{\text{ 全ての } R \text{ モジュール（加群）たち }\}\)
\(J\): \(\in \{\text{ 全てのアンカウンタブル（不可算）かもしれないインデックスセット（集合）たち }\}\)
\(B\): \(= \{b_j \vert j \in J\}\), \(\in \{M \text{ に対する全てのベーシス（基底）たち }\}\)
\(m\): \(\in M\), \(= \sum_{j \in S} m^j b_j\)、あるファイナイト（有限）\(S \subseteq J\)および\(m^j \neq 0\)に対して
//
ステートメント（言明）たち:
\(\exists S' \in \{J \text{ の全てのファイナイト（有限）サブセット（部分集合）たち }\} (m = \sum_{j \in S'} m'^j b_j \text{ 、ここで、 } m'^j \neq 0)\)
\(\implies\)
\(S' = S \land \forall j \in S (m^j = m'^j)\)
//
そうした\(S\)はある、モジュール（加群）のベーシス（基底）の定義によって。
2: 注
モジュール（加群）のベーシス（基底）の定義は、直接には、\(m\)の当該ベーシス（基底）に関する分解がユニークであるように要求しないが、本命題は、当該分解が不可避にユニークであると主張している。
3: 証明
全体戦略: ステップ1: \(S \cup S'\)を取り、\(m = \sum_{j \in S \cup S'} \widetilde{m}^j b_j = \sum_{j \in S \cup S'} \widetilde{m'}^j b_j\)とする; ステップ2: \(\widetilde{m}^j - \widetilde{m'}^j = 0\)であると結論する。
ステップ1:
\(S \cup S'\)を取ろう。
各\(j \in S \cup S'\)に対して、\(j \in S\)に対して\(\widetilde{m}^j = m^j\)で\(j \notin S\)に対して\(\widetilde{m}^j = 0\)であるとしよう。
すると、\(m = \sum_{j \in S \cup S'} \widetilde{m}^j b_j\)。
各\(j \in S \cup S'\)に対して、\(j \in S'\)に対して\(\widetilde{m'}^j = m'^j\)で\(j \notin S'\)に対して\(\widetilde{m'}^j = 0\)であるとしよう。
すると、\(m = \sum_{j \in S \cup S'} \widetilde{m'}^j b_j\)。
ステップ2:
\(\sum_{j \in S \cup S'} \widetilde{m}^j b_j = \sum_{j \in S \cup S'} \widetilde{m'}^j b_j\)であるから、\(\sum_{j \in S \cup S'} \widetilde{m}^j b_j - \sum_{j \in S \cup S'} \widetilde{m'}^j b_j = 0\)、しかし、\(= \sum_{j \in S \cup S'} (\widetilde{m}^j - \widetilde{m'}^j) b_j\)。
\(B\)はリニアにインディペンデント（線形独立）であるから、\(\widetilde{m}^j - \widetilde{m'}^j\)、各\(j \in S \cup S'\)に対して、したがって、\(\widetilde{m}^j = \widetilde{m'}^j\)。
ある\(j \in S \cup S'\)に対して\(\widetilde{m}^j = \widetilde{m'}^j = 0\)であると仮定しよう。\(j \notin S\)および\(j \notin S'\)、それが意味するのは、\(j \notin S \cup S'\)、矛盾。したがって、\(\widetilde{m}^j = \widetilde{m'}^j \neq 0\)、それが含意するのは、\(S = S'\)。
各\(j \in S\)に対して、\(m^j = \widetilde{m}^j = \widetilde{m'}^j = m'^j\)。
