description/proof of that for tensor product of \(k\) finite-dimensional vectors spaces over field, transition of standard bases w.r.t. bases for vectors spaces is this
Topics
About: vectors space
The table of contents of this article
Starting Context
Target Context
- The reader will have a description and a proof of the proposition that for the tensor product of any \(k\) finite-dimensional vectors spaces over any field, the transition of the standard bases with respect to any bases for the vectors spaces is this.
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 }\}\)
\(V_1 \otimes ... \otimes V_k\): \(= \text{ the tensor product }\)
\(\{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 \in \{\text{ the bases for } V_j\} = \{{b'_j}_l \vert 1 \le l \le dim V_j\}\)
\(B\): \(= \{[(({b_1}_{l_1}, ..., {b_k}_{l_k}))] \vert {b_j}^{l_j} \in B_j\}\), \(\in \{\text{ the bases for } V_1 \otimes ... \otimes V_k\}\)
\(B'\): \(= \{[(({b'_1}_{l_1}, ..., {b'_k}_{l_k}))] \vert {b'_j}^{l_j} \in B'_j\}\), \(\in \{\text{ the bases for } V_1 \otimes ... \otimes V_k\}\)
//
Statements:
\({b'_j}_l = {b_j}_m {M_j}^m_l\)
\(\implies\)
\([(({b'_1}_{l_1}, ..., {b'_k}_{l_k}))] = [(({b_1}_{m_1}, ..., {b_k}_{m_k}))] {M_1}^{m_1}_{l_1} ... {M_k}^{m_k}_{l_k}\)
//
2: Proof
Whole Strategy: Step 1: see that \(B\) and \(B'\) are some bases for \(V_1 \otimes ... \otimes V_k\); Step 2: conclude the proposition.
Step 1:
\(B\) and \(B'\) are indeed some bases for \(V_1 \otimes ... \otimes V_k\), by the proposition that the tensor product of any \(k\) finite-dimensional vectors spaces has the basis that consists of the classes induced by any basis elements.
Step 2:
\([(({b'_1}_{l_1}, ..., {b'_k}_{l_k}))] = [(({b_1}_{m_1} {M_1}^{m_1}_{l_1}, ..., {b_k}_{m_k} {M_k}^{m_k}_{l_k}))]\).
We note the fact that in general, \([((v_1, ..., r v_j+ r' v'_j, ..., v_k))] = r [((v_1, ..., v_j, ..., v_k))] + r' [((v_1, ..., v'_j, ..., v_k))]\): refer to Note for the definition of tensor product of \(k\) vectors spaces over field.
So, \([(({b_1}_{m_1} {M_1}^{m_1}_{l_1}, ..., {b_k}_{m_k} {M_k}^{m_k}_{l_k}))] = [(({b_1}_{m_1}, ..., {b_k}_{m_k}))] {M_1}^{m_1}_{l_1} ... {M_k}^{m_k}_{l_k}\).
