フィールド（体）、フィールド（体）上方の\(k\)個のファイナイト（有限）-ディメンショナル（次元）ベクトルたちスペース（空間）たちおよびフィールド（体）に関するテンソルたちスペース（空間）は\(k\)個のコベクトルたちスペース（空間）たちのテンソルプロダクト（積）へ'ベクトルたちスペース（空間）たち - リニア（線形）モーフィズム（射）たち'アイソモーフィック（同形写像）であることの記述/証明
話題
About: ベクトルたちスペース（空間）
この記事の目次
開始コンテキスト
- 読者は、フィールド（体）、フィールド（体）上方のk個のベクトルたちスペース（空間）たちおよびベクトルたちスペース（空間）に関するテンソルたちスペース（空間）の定義を知っている。
- 読者は、ベクトルたちスペース（空間）のコベクトルたち（デュアル）スペース（空間）の定義を知っている。
- 読者は、フィールド（体）上方の\(k\)個のベクトルたちスペース（空間）たちのテンソルプロダクト（積）の定義を知っている。
- 読者は、%カテゴリー名%アイソモーフィズム（同形写像）の定義を知っている。
- 読者は、テンソルたちのテンソルプロダクト（積）の定義を知っている。
- 読者は、任意のファイナイト（有限）プロダクト（積）ベクトルたちスペース（空間）からの任意のマルチリニアマップ（多重線形写像）に対して、当該ファイナイト（有限）個ベクトルたちスペース（空間）たちのテンソルプロダクト（積）からのユニークなリニアマップ（線形写像）で、当該マルチリニアマップ（多重線形写像）は、当該プロダクト（積）ベクトルたちスペース（空間）から当該テンソルプロダクト（積）の中へのカノニカル（正典）マップ（写像）の後に当該リニアマップ（写像）を作用させるものであるものがあるという命題を認めている。
- 読者は、任意のフィールド（体）、当該フィールド（体）上方の任意の\(k\)個のベクトルたちスペース（空間）たちに対して、当該フィールド（体）、当該ベクトルたちスペース（空間）たち、当該フィールド（体）に関するテンソルたちスペース（空間）は、ベーシス（基底）で当該ベクトルたちスペース（空間）たちの任意のベーシス（基底）たちのデュアルベーシス（基底）たちの全ての要素たちの全てのテンソルプロダクト（積）たちから構成されるものを持つという命題を認めている。
- 読者は、任意の\(k\)個のファイナイト（有限）-ディメンショナル（次元）ベクトルたちスペース（空間）たちのテンソルプロダクト（積）は任意のベーシス（基底）要素たちによってインデュースト（誘導された）クラスたちから構成されるベーシス（基底）を持つという命題を認めている。
- 読者は、ベーシス（基底）たちを持つ任意のモジュール（加群）たち間任意のリニアマップ（線形写像）に対して、もしも、その、任意のドメイン（定義域）ベーシス（基底）についてのリストリクション（制限）が任意のコドメイン（余域）ベーシス（基底）の上へのバイジェクション（全単射）である場合、当該マップ（写像）は'モジュール（加群）たち - リニア（線形）モーフィズム（射）たち'アイソモーフィズム（同形写像）であるという命題を認めている。
- 読者は、任意のベクトルたちスペース（空間）たち間の任意のバイジェクティブ（全単射）リニアマップ（線形写像）は'ベクトルたちスペース（空間）たち - リニア（線形）モーフィズム（射）たち'アイソモーフィズム（同形写像）であるという命題を認めている。
ターゲットコンテキスト
- 読者は、フィールド（体）、フィールド（体）上方の\(k\)個のファイナイト（有限）-ディメンショナル（次元）ベクトルたちスペース（空間）たちおよびフィールド（体）に関する任意のテンソルたちスペース（空間）は\(k\)個の当該コベクトルたちスペース（空間）たちのテンソルプロダクト（積）へ'ベクトルたちスペース（空間）たち - リニア（線形）モーフィズム（射）たち'アイソモーフィック（同形写像）であるという命題の記述および証明を得る。
オリエンテーション
本サイトにてこれまで議論された定義たちの一覧があります。
本サイトにてこれまで議論された命題たちの一覧があります。
本体
1: 構造化された記述
ここに'構造化された記述'のルールたちがある。
エンティティ（実体）たち:
\(F\): \(\in \{\text{ 全てのフィールド（体）たち }\}\)
\(\{V_1, ..., V_k\}\): \(\subseteq \{\text{ 全てのファイナイト（有限）-ディメンショナル（次元） } F \text{ ベクトルたちスペース（空間）たち }\}\)
\(L (V_1, ..., V_k: F)\): \(= \text{ 当該テンソルたちスペース（空間） }\)
\(\{V^*_1, ..., V^*_k\}\): \(V^*_j = V_j \text{ のコベクトルたちスペース（空間） }\)
\(V^*_1 \otimes ... \otimes V^*_k\): \(= \text{ 当該テンソルプロダクト（積） }\)
\(\{B^*_1, ..., B^*_k\}\): \(B^*_j = \{b_j^l\} \in \{V^*_j \text{ に対する全てのベーシス（基底）たち }\}\)
//
ステートメント（言明）たち:
\(\exists f': V^*_1 \otimes ... \otimes V^*_k \to L (V_1, ..., V_k: F), t_{j_1, ..., j_k} [((b_1^{j_1}, ..., b_k^{j_k}))] \mapsto t_{j_1, ..., j_k} b_1^{j_1} \otimes ... \otimes b_k^{j_k} \in \{\text{ 全ての'ベクトルたちスペース（空間）たち - リニア（線形）モーフィズム（射）たち'アイソモーフィズム（同形写像）たち }\}\)
//
2: 注
各\(V_j\)はファイナイト（有限）-ディメンショナル（次元）である必要がある、なぜなら、"証明"は任意のフィールド（体）、当該フィールド（体）上方の任意の\(k\)個のベクトルたちスペース（空間）たちに対して、当該フィールド（体）、当該ベクトルたちスペース（空間）たち、当該フィールド（体）に関するテンソルたちスペース（空間）は、ベーシス（基底）で当該ベクトルたちスペース（空間）たちの任意のベーシス（基底）たちのデュアルベーシス（基底）たちの全ての要素たちの全てのテンソルプロダクト（積）たちから構成されるものを持つという命題および任意の\(k\)個のファイナイト（有限）-ディメンショナル（次元）ベクトルたちスペース（空間）たちのテンソルプロダクト（積）は任意のベーシス（基底）要素たちによってインデュースト（誘導された）クラスたちから構成されるベーシス（基底）を持つという命題を使っているが、それらは、\(V_j\)たちがファイナイト（有限）-ディメンショナル（次元）であることを要求する。
3: 証明
全体戦略: ステップ1: あるマルチリニアマップ（多重線形写像）\(f: V^*_1 \times ... \times V^*_k \to L (V_1, ..., V_k: F), (v^1, ..., v^k) \mapsto v^1 \otimes ... \otimes v^k\)を取る; ステップ2: ユニークなリニアマップ（線形写像）\(f': V^*_1 \otimes ... \otimes V^*_k \to L (V_1, ..., V_k: F)\)を得る; ステップ3: \(f'\)は'ベクトルたちスペース（空間）たち - リニア（線形）モーフィズム（射）たち'アイソモーフィズム（同形写像）であることを見る。
ステップ1:
あるマップ（写像）\(f: V^*_1 \times ... \times V^*_k \to L (V_1, ..., V_k: F), (v^1, ..., v^k) \mapsto v^1 \otimes ... \otimes v^k\)を取ろう。
\(f\)はマルチリニアマップ（多重線形写像）であることを見よう。
\(f ((v^1, ..., r v^j + r' v'^j, ..., v^k)) = v^1 \otimes ... \otimes (r v^j + r' v'^j) \otimes ... \otimes v^k = r v^1 \otimes ... \otimes v^j \otimes ... \otimes v^k + r' v^1 \otimes ... \otimes v'^j \otimes ... \otimes v^k\)、テンソルたちのテンソルプロダクト（積）の定義に対する"注"内で言及されているテンソルたちのプロダクトのプロパティによって。
\(= r f ((v^1, ..., v^j, ..., v^k)) + r' f ((v^1, ..., v'^j, ..., v^k))\)、それが意味するのは、\(f\)はマルチリニア（多重線形）であること。
ステップ2:
任意のファイナイト（有限）プロダクト（積）ベクトルたちスペース（空間）からの任意のマルチリニアマップ（多重線形写像）に対して、当該ファイナイト（有限）個ベクトルたちスペース（空間）たちのテンソルプロダクト（積）からのユニークなリニアマップ（線形写像）で、当該マルチリニアマップ（多重線形写像）は、当該プロダクト（積）ベクトルたちスペース（空間）から当該テンソルプロダクト（積）の中へのカノニカル（正典）マップ（写像）の後に当該リニアマップ（写像）を作用させるものであるものがあるという命題によって、ユニークなリニアマップ（線形写像）\(f': V^*_1 \otimes ... \otimes V^*_k \to L (V_1, ..., V_k: F)\)で\(f = f' \circ g\), where \(g: V^*_1 \times ... \times V^*_k \to V^*_1 \otimes ... \otimes V^*_k, (v^1, ..., v^k) \mapsto [((v^1, ..., v^k))]\)を満たすものがある。
ステップ3:
残る課題は、\(f'\)が'ベクトルたちスペース（空間）たち - リニア（線形）モーフィズム（射）たち'アイソモーフィズム（同形写像）であることを見ることである。
\(V^*_1 \otimes ... \otimes V^*_k\)はスタンダード（標準）ベーシス（基底）\(B = \{[((b_1^{j_1}, ..., b_k^{j_k}))] \vert b_l^{j_l} \in B^*_l\}\)、ここで、\(B^*_l\)は\(V^*_l\)に対するベーシス（基底）である、を持つ、任意の\(k\)個のファイナイト（有限）-ディメンショナル（次元）ベクトルたちスペース（空間）たちのテンソルプロダクト（積）は任意のベーシス（基底）要素たちによってインデュースト（誘導された）クラスたちから構成されるベーシス（基底）を持つという命題によって。
\(L (V_1, ..., V_k: F)\)はスタンダード（標準）ベーシス（基底）\(B = \{b^{j_1}_1 \otimes ... \otimes b^{j_k}_k \vert b^{j_l}_l \in B^*_l\}\)を持つ、任意のフィールド（体）、当該フィールド（体）上方の任意の\(k\)個のベクトルたちスペース（空間）たちに対して、当該フィールド（体）、当該ベクトルたちスペース（空間）たち、当該フィールド（体）に関するテンソルたちスペース（空間）は、ベーシス（基底）で当該ベクトルたちスペース（空間）たちの任意のベーシス（基底）たちのデュアルベーシス（基底）たちの全ての要素たちの全てのテンソルプロダクト（積）たちから構成されるものを持つという命題によって。
\(f' ([((b_1^{j_1}, ..., b_k^{j_k}))]) = b_1^{j_1} \otimes ... \otimes b_k^{j_k}\)、なぜなら、\(f' \circ g = f\)、そして、\(f' \circ g ((b_1^{j_1}, ... b_k^{j_k})) = f ((b_1^{j_1}, ... b_k^{j_k})) = b_1^{j_1} \otimes ... \otimes b_k^{j_k}\)、ここで、\(f' \circ g ((b_1^{j_1}, ... b_k^{j_k})) = f' ([((b_1^{j_1}, ..., b_k^{j_k}))])\)。
それが意味するのは、\(f'\)は\(V^*_1 \otimes ... \otimes V^*_k\)の当該ベーシス（基底）を\(L (V_1, ..., V_k: F)\)の当該ベーシス（基底）へバイジェクティブ（全単射）にマップするということ。
ベーシス（基底）たちを持つ任意のモジュール（加群）たち間任意のリニアマップ（線形写像）に対して、もしも、その、任意のドメイン（定義域）ベーシス（基底）についてのリストリクション（制限）が任意のコドメイン（余域）ベーシス（基底）の上へのバイジェクション（全単射）である場合、当該マップ（写像）は'モジュール（加群）たち - リニア（線形）モーフィズム（射）たち'アイソモーフィズム（同形写像）であるという命題によって、\(f'\)は'モジュール（加群）たち - リニア（線形）モーフィズム（射）たち'アイソモーフィズム（同形写像）であるということ、それが意味するのは、\(f'\)はバイジェクション（全単射）であるということ、そして、\(f'\)は'ベクトルたちスペース（空間）たち - リニア（線形）モーフィズム（射）たち'アイソモーフィズム（同形写像）である、任意のベクトルたちスペース（空間）たち間の任意のバイジェクティブ（全単射）リニアマップ（線形写像）は'ベクトルたちスペース（空間）たち - リニア（線形）モーフィズム（射）たち'アイソモーフィズム（同形写像）であるという命題によって。
