description/proof of that between finite-dimensional vectors space and its double dual, there is canonical 'vectors spaces - linear morphisms' isomorphism
Topics
About: vectors space
The table of contents of this article
Starting Context
- The reader knows a definition of dual basis for covectors (dual) space of basis for finite-dimensional vectors space.
- The reader knows a definition of %category name% isomorphism.
- 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 for any finite-dimensional vectors space, the transition of the dual bases for the covectors space with respect to any bases for the vectors space is this.
Target Context
- The reader will have a description and a proof of the proposition that between any finite-dimensional vectors space and its double dual, 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\): \(\in \{\text{ the finite-dimensional } F \text{ vectors spaces }\}\)
\(V^*\): \(= L (V: F)\)
\({V^*}^*\): \(= L (L (V: F): F)\)
\(J\): \(\in \{\text{ the finite index sets }\}\)
\(B\): \(\in \{\text{ the bases for } V\}\), \(= \{b_j \vert j \in J\}\)
\(B^*\): \(= \text{ the dual basis of } B\), \(= \{b^j \vert j \in J\}\)
\({B^*}^*\): \(= \text{ the dual basis of } B^*\), \(= \{\widetilde{b}_j \vert j \in J\}\)
\(f\): \(: V \to {V^*}^*, v^j b_j \mapsto \sum_{j \in J} v^j \widetilde{b}_j\)
Statements:
\(f \in \{\text{ the 'vectors spaces - linear morphisms' isomorphisms }\}\)
\(\land\)
\(f\) does not depend on the choice of \(B\)
\(\land\)
\(\forall v \in V, \forall w \in V^* (w (v) = f (v) (w))\)
//
2: Proof
Whole Strategy: Step 1: see that \(f\) is a 'vectors spaces - linear morphisms' isomorphism; Step 2: see that \(f\) does not depend on the choice of \(B\) by taking another basis \(B'\) and seeing that the map constructed by \(B'\) is \(f\): Step 3: see that \(\forall v \in V, \forall w \in V^* (w (v) = f (v) (w))\) by extending \(v\), \(w\), and \(f (v)\) with the bases.
Step 1:
\(B^*\) is indeed a basis for \(V^*\), by Note for the definition of dual basis for covectors (dual) space of basis for finite-dimensional vectors space.
\({B^*}^*\) is indeed a basis for \({V^*}^*\), by Note for the definition of dual basis for covectors (dual) space of basis for finite-dimensional vectors space.
\(f\) is indeed a 'vectors spaces - linear morphisms' isomorphism, 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.
Step 2:
Let us see that \(f\) does not depend on the choice of \(B\).
Let \(B' = \{b'_j \vert j \in J\}\) be any other basis for \(V\).
\(b'_j = b_l M^l_j\) for an invertible matrix, \(M\). So, \(b_j = b'_l {M^{-1}}^l_j\).
The dual basis of \(B'\), \(B'^* = \{b'^j \vert j \in J\}\), is \(\{{M^{-1}}^j_l b^l\}\), by the proposition that for any finite-dimensional vectors space, the transition of the dual bases for the covectors space with respect to any bases for the vectors space is this.
The dual basis of \(B'^*\), \({B'^*}^* = \{\widetilde{b'}_j \vert j \in J\}\), is \(\{\widetilde{b}_l M^l_j\}\), by the proposition that for any finite-dimensional vectors space, the transition of the dual bases for the covectors space with respect to any bases for the vectors space is this.
The canonical 'vectors spaces - linear morphisms' isomorphism with respect to \(B'\), \(f': V \to {V^*}^*\), maps \(b_j = b'_l {M^{-1}}^l_j\) to \(\widetilde{b'}_l {M^{-1}}^l_j = \widetilde{b}_m M^m_l {M^{-1}}^l_j = \widetilde{b}_m \delta^m_j = \widetilde{b}_j\).
So, \(f' = f\).
Step 3:
Let us see that \(\forall v \in V, \forall w \in V^* (w (v) = f (v) (w))\).
\(v = v^j b_j\) and \(w = w_l b^l\), and \(w (v) = w_l b^l (v^j b_j) = w_l v^j b^l (b_j) = w_l v^j \delta^l_j = w_j v^j\).
\(f (v) (w) = f (v^j b_j) (w_l b^l) = v^j \widetilde{b}_j (w_l b^l) = v^j w_l \widetilde{b}_j (b^l) = v^j w_l \delta^l_j = v^j w_j\).
