description/proof of that between tensors space w.r.t. field and \(k\) finite-dimensional vectors spaces over field and field and tensors space w.r.t. field and \(k\) 'vectors spaces - linear morphisms' isomorphic vectors spaces over field and field, there is canonical 'vectors spaces - linear morphisms' isomorphism
Topics
About: vectors space
The table of contents of this article
- Starting Context
- Target Context
- Orientation
- Main Body
- 1: Structured Description
- 2: Note 1
- 3: Proof
- 4: Note 2
Starting Context
- The reader knows a definition of tensors space w.r.t. field and k vectors spaces and vectors space over field.
- The reader knows a definition of %category name% isomorphism.
- The reader admits the proposition that for any field and any k finite-dimensional vectors spaces over the field, the tensors space with respect to the field and the vectors spaces and the field has the basis that consists of the tensor products of the elements of the dual bases of any bases of the vectors spaces.
- The reader admits the proposition that between any vectors spaces, any map that maps any basis onto any basis bijectively and expands the mapping linearly is a 'vectors spaces - linear morphisms' isomorphism.
- The reader admits the proposition that any finite-dimensional vectors spaces over any same field are 'vectors spaces - linear morphisms' isomorphic if and only if they have any same dimension.
Target Context
- The reader will have a description and a proof of the proposition that between the tensors space with respect to any field and any \(k\) finite-dimensional vectors spaces over the field and the field and the tensors space with respect to the field and any \(k\) 'vectors spaces - linear morphisms' isomorphic vectors spaces over the field and the field, there is the canonical 'vectors spaces - linear morphisms' isomorphism.
Orientation
There is a list of definitions discussed so far in this site.
There is a list of propositions discussed so far in this site.
Main Body
1: Structured Description
Here is the rules of Structured Description.
Entities:
\(F\): \(\in \{\text{ the fields }\}\)
\(\{V_1, ..., V_k\}\): \(\subseteq \{\text{ the finite-dimensional } F \text{ vectors spaces }\}\)
\(\{B_1, ..., B_k\}\): \(B_j \in \{\text{ the bases for } V_j\} = \{{b_j}_l \vert 1 \le l \le dim V_j\}\)
\(\{B^*_1, ..., B^*_k\}\): \(B^*_j = \text{ the dual basis of } B_j = \{{b_j}^l \vert 1 \le l \le dim V_j\}\)
\(L (V_1, ..., V_k: F)\): \(= \text{ the tensors space }\)
\(\{V'_1, ..., V'_k\}\): \(V_j \cong_{\text{ vectors spaces }} V'_j\)
\(\{B'_1, ..., B'_k\}\): \(B'_j \in \{\text{ the bases for } V'_j\} = \{{b'_j}_l \vert 1 \le l \le dim V_j\}\)
\(\{B'^*_1, ..., B'^*_k\}\): \(B'^*_j = \text{ the dual basis of } B'_j = \{{b'_j}^l \vert 1 \le l \le dim V_j\}\)
\(L (V'_1, ..., V'_k: F)\): \(= \text{ the tensors space }\)
\(f\): \(: L (V_1, ..., V_k: F) \to L (V'_1, ..., V'_k: F), v_{j_1, ..., j_k} {b_1}^{j_1} \otimes ... \otimes {b_k}^{j_k} \mapsto v_{j_1, ..., j_k} {b'_1}^{j_1} \otimes ... \otimes {b'_k}^{j_k}\)
//
Statements:
\(f \in \{\text{ the 'vectors spaces - linear morphisms' isomorphisms }\}\)
//
Being called "canonical", it depends on the bases, \(\{B_1, ..., B_k, B'_1, ..., B'_k\}\): this is saying that it is canonical once the bases are fixed.
2: Note 1
\(L (V_1, ..., V_k: F) \cong_{\text{ vectors spaces }} L (V'_1, ..., V'_k: F)\) is immediately deduced from the proposition that for any field and any k finite-dimensional vectors spaces over the field, the tensors space with respect to the field and the vectors spaces and the field has the basis that consists of the tensor products of the elements of the dual bases of any bases of the vectors spaces and the proposition that any finite-dimensional vectors spaces over any same field are 'vectors spaces - linear morphisms' isomorphic if and only if they have any same dimension; the objective of this proposition is to produce an explicit isomorphism.
3: Proof
Whole Strategy: Step 1: see that \(f\) is well-defined; Step 2: see that \(f\) is mapping the standard basis for \(L (V_1, ..., V_k: F)\) onto the standard basis for \(L (V'_1, ..., V'_k: F)\) bijectively and expanding the mapping; Step 3: conclude the proposition.
Step 1:
Let us see that \(f\) is well-defined.
\(B^* = \{{b_1}^{j_1} \otimes ... \otimes {b_k}^{j_k} \vert \forall l \in \{1, ..., k\} (1 \le j_l \le dim V_l)\}\) is the standard basis for \(L (V_1, ..., V_k: F)\), by the proposition that for any field and any k finite-dimensional vectors spaces over the field, the tensors space with respect to the field and the vectors spaces and the field has the basis that consists of the tensor products of the elements of the dual bases of any bases of the vectors spaces.
\(B'^* = \{{b'_1}^{j_1} \otimes ... \otimes {b'_k}^{j_k} \vert \forall l \in \{1, ..., k\} (1 \le j_l \le dim V_l)\}\) is the standard basis for \(L (V'_1, ..., V'_k: F)\), likewise.
So, each \(v \in L (V_1, ..., V_k: F)\) is uniquely expressed as \(v = v_{j_1, ..., j_k} {b_1}^{j_1} \otimes ... \otimes {b_k}^{j_k}\).
So, \(f\) maps each element of \(L (V_1, ..., V_k: F)\) uniquely.
Step 2:
\(f\) is mapping \(B^*\) onto \(B'^*\) bijectively.
\(f\) is linearly expanding the mapping of \(B^*\).
Step 3:
By the proposition that between any vectors spaces, any map that maps any basis onto any basis bijectively and expands the mapping linearly is a 'vectors spaces - linear morphisms' isomorphism, \(f\) is a 'vectors spaces - linear morphisms' isomorphism.
4: Note 2
Especially, between \(L (T_mM^*, ..., T_mM^*, {T_mM^*}^*, ..., {T_mM^*}^*)\) and \(L (T_mM^*, ..., T_mM^*, T_mM, ..., T_mM)\), \(f\) can be defined that way: the proposition that the double dual of any finite dimensional real vectors space is 'vectors spaces - linear morphisms' isomorphic to the original vectors space.
