ベクトルたちスペース（空間）エンドモーフィズム（自己準同形写像）に対して、もしも、ドメイン（定義域）の中へのマップ（写像）があってベーシス（基底）に関してサージェクティブ（全射）でありマップ（写像）がマップ（写像）の後にエンドモーフィズム（自己準同形写像）を作用させるのと等しい場合、エンドモーフィズム（自己準同形写像）はアイデンティティ（恒等写像）であることの記述/証明
話題
About: ベクトルたちスペース（空間）
この記事の目次
開始コンテキスト
- 読者は、%ストラクチャー（構造）種類名%エンドモーフィズム（自己準同形写像）の定義を知っている。
- 読者は、%フィールド（体）名%ベクトルたちスペース（空間）の定義を知っている。
- 読者は、リニアマップ（線形写像）の定義を知っている。
ターゲットコンテキスト
- 読者は、任意のベクトルたちスペース（空間）エンドモーフィズム（自己準同形写像）に対して、もしも、当該エンドモーフィズム（自己準同形写像）の当該ドメイン（定義域）の中への任意のマップ（写像）があって任意のベーシス（基底）に関してサージェクティブ（全射）であり当該マップ（写像）が当該マップ（写像）の後に当該エンドモーフィズム（自己準同形写像）を作用させるのと等しい場合、当該エンドモーフィズム（自己準同形写像）はアイデンティティ（恒等写像）であるという命題の記述および証明を得る。
オリエンテーション
本サイトにてこれまで議論された定義たちの一覧があります。
本サイトにてこれまで議論された命題たちの一覧があります。
本体
1: 構造化された記述
ここに'構造化された記述'のルールたちがある。
エンティティ（実体）たち:
\(F\): \(\in \{\text{ 全てのフィールド（体）たち }\}\)
\(V\): \(\in \{\text{ 全ての } F \text{ ベクトルたちスペース（空間）たち }\}\)
\(f\): \(: V \to V\), \(\in \{\text{ 全てのベクトルたちスペース（空間）エンドモーフィズム（自己準同形写像）たち }\}\)
//
ステートメント（言明）たち:
\(\exists S' \in \{\text{ 全てのセット（集合）たち }\}, \exists B \in \{V \text{ の全てのベーシス（基底）たち }\}, \exists f': S' \to V, \text{ で以下を満たすもの、つまり、 } B \subseteq f' (S') (f' = f \circ f')\)
\(\implies\)
\(f = id: V \to V\)
//
2: 証明
全体戦略: ステップ1: 任意の\(v \in V\)を取り、\(v = v^1 b_1 + ... + v^k b_k\)、ここで、\(\{b_1, ..., b_k\} \subseteq B\)、であることを見る; ステップ2: 各\(j\)に対して、ある\(s'_j \in S'\)に対して\(b_j = f' (s'_j)\)であることを見る; ステップ3: \(f (v) = v\)であることを見る。
ステップ1:
\(v \in V\)は任意のものであるとしよう。
\(v = v^1 b_1 + ... + v^k b_k\)、ここで、\(\{b_1, ..., b_k\} \subseteq B\)および\(\{v^1, ..., v^k\} \subseteq F\)。
ステップ2:
\(B \subseteq f' (S')\)であるから、各\(j \in \{1, ..., k\}\)に対して、以下を満たすある\(s'_j \in S'\)、つまり、\(b_j = f' (s'_j)\)、がある。
したがって、\(v = v^1 f' (s'_1) + ... + v^k f' (s'_k)\)。
ステップ3:
\(f\)はリニア（線形）であるから、\(f (v) = f (v^1 f' (s'_1) + ... + v^k f' (s'_k)) = v^1 f (f' (s'_1)) + ... + v^k f (f' (s'_k))\)、しかし、\(f' = f \circ f'\)であるから、\( = v^1 f' (s'_1) + ... + v^k f' (s'_k) = v\)。
\(v\)は恣意的であるから、\(f\)はアイデンティティマップ（恒等写像）である。
3: 注
\(f\)が単にセット（集合）エンドモーフィズム（自己準同形写像）であるケースに対しては、\(f'\)に対してより多くを要求する命題がある。
