description/proof of that derivation of wedge product of multicovectors by real parameter satisfies Leibniz rule
Topics
About: vectors space
The table of contents of this article
Starting Context
- The reader knows a definition of wedge product of multicovectors.
- The reader knows a definition of derivative of real-1-parameter family of vectors in finite-dimensional real vectors space.
- The reader knows a definition of convergence of map from topological space minus point into topological space with respect to point.
- The reader admits the proposition that for any map from any topological space minus any point into any finite-dimensional real vectors space with the canonical topology, the convergence of the map with respect to the point exists if and only if the convergences of the component maps (with respect to any basis) with respect to the point exist, and then, the convergence Is expressed with the convergences.
- The reader admits the proposition that for any map from any topological space minus any point into any finite-dimensional real vectors space with the canonical topology, the convergence of the map with respect to the point exists if the convergences of the coefficients with respect to any constant vectors with respect to the point exist, and then, the convergence is expressed with the convergences.
- The reader admits the proposition that the \(q\)-covectors space of any vectors space has the basis that consists of the wedge products of the increasing elements of the dual basis of the vectors space.
Target Context
- The reader will have a description and a proof of the proposition that the derivation of the wedge product of any multicovectors by any real parameter satisfies the Leibniz rule.
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:
\(T\): \(= (r_1, r_2) \subseteq \mathbb{R}\), with the subspace topology with \(\mathbb{R}\) as the Euclidean topological space
\(r\): \(\in T\)
\(V\): \(\in \{\text{ the finite-dimensional } \mathbb{R} \text{ vectors spaces }\}\)
\(\Lambda_{k_1} (V: \mathbb{R})\): \(= \text{ the } k_1 \text{ -covectors space }\), with the canonical topology
\(\Lambda_{k_2} (V: \mathbb{R})\): \(= \text{ the } k_2 \text{ -covectors space }\), with the canonical topology
\(t^1\): \(: T \to \Lambda_{k_1} (V: \mathbb{R})\)
\(t^2\): \(: T \to \Lambda_{k_2} (V: \mathbb{R})\)
\(\Lambda_{k_1 + k_2} (V: \mathbb{R})\): \(= \text{ the } (k_1 + k_2) \text{ covectors space }\), with the canonical topology
\(t^1 \wedge t^2\): \(: T \to \Lambda_{k_1 + k_2} (V: \mathbb{R})\)
//
Statements:
\(\exists d t^1 / d r \land \exists d t^2 / d r\)
\(\implies\)
\(\exists d (t^1 \wedge t^2) / d r \land d (t^1 \wedge t^2) / d r = d t^1 / d r \wedge t^2 (r) + t^1 (r) \wedge d t^2 / d r\)
//
2: Proof
Whole Strategy: Step 1: for \(V\), take any basis, \(\{b_m\}\), and take the standard bases for \(\Lambda_{k_1} (V: \mathbb{R})\) and \(\Lambda_{k_2} (V: \mathbb{R})\), \(B_1\) and \(B_2\); Step 2: let \(t^1 (r')\) and \(t^2 (r')\) be expressed with the bases, and let \(t^1 (r') \wedge t^2 (r')\) be expanded using the expressions of \(t^1 (r')\) and \(t^2 (r')\); Step 3: take \(d (t^1 \wedge t^2) / d r = lim_{r' \to r} (t^1 (r') \wedge t^2 (r') - t^1 (r) \wedge t^2 (r)) / (r' - r)\) and apply the proposition that for any map from any topological space minus any point into any finite-dimensional real vectors space with the canonical topology, the convergence of the map with respect to the point exists if and only if the convergences of the component maps (with respect to any basis) with respect to the point exist, and then, the convergence Is expressed with the convergences and the proposition that for any map from any topological space minus any point into any finite-dimensional real vectors space with the canonical topology, the convergence of the map with respect to the point exists if the convergences of the coefficients with respect to any constant vectors with respect to the point exist, and then, the convergence is expressed with the convergences.
Step 1:
For \(V\), let us take any basis, \(\{b_m\}\).
Let us take the standard basis for \(\Lambda_{k_1} (V: \mathbb{R})\), \(B_1 = \{b^{m_1} \wedge ... \wedge b^{m_{k_1}}\}\), which is possible by the proposition that the \(q\)-covectors space of any vectors space has the basis that consists of the wedge products of the increasing elements of the dual basis of the vectors space.
Let us take the standard basis for \(\Lambda_{k_2} (V: \mathbb{R})\), \(B_2 = \{b^{m_1} \wedge ... \wedge b^{m_{k_2}}\}\), which is possible likewise.
Let us take the standard basis for \(\Lambda_{k_1 + k_2} (V: \mathbb{R})\), \(B = \{b^{m_1} \wedge ... \wedge b^{m_{k_1 + k_2}}\}\), which is possible likewise.
Step 2:
\(t^1 (r') = t^1_{m_1, ..., m_{k_1}} (r') b^{m_1} \wedge ... \wedge b^{m_{k_1}}\).
\(t^2 (r') = t^2_{m_1, ..., m_{k_2}} (r') b^{m_1} \wedge ... \wedge b^{m_{k_2}}\).
So, \(t^1 (r') \wedge t^2 (r') = (t^1_{m_1, ..., m_{k_1}} (r') b^{m_1} \wedge ... \wedge b^{m_{k_1}}) \wedge (t^2_{n_1, ..., n_{k_2}} (r') b^{n_1} \wedge ... \wedge b^{n_{k_2}})\).
By a property of wedge product of multicovectors mentioned in Note for the definition of wedge product of multicovectors, \(= t^1_{m_1, ..., m_{k_1}} (r') t^2_{n_1, ..., n_{k_2}} (r') b^{m_1} \wedge ... \wedge b^{m_{k_1}} \wedge b^{n_1} \wedge ... \wedge b^{n_{k_2}}\), which is not really any expansion of \(t^1 (r') \wedge t^2 (r')\) with respect to the standard basis for \(\Lambda_{k_1 + k_2} (V: \mathbb{R})\), because \(b^{m_1} \wedge ... \wedge b^{m_{k_1}} \wedge b^{n_1} \wedge ... \wedge b^{n_{k_2}}\) is not necessarily in the indexes increasing order, but anyway, it is the expansion with some constant vectors.
Step 3:
\(d (t^1 \wedge t^2) / d r = lim_{r' \to r} (t^1 (r') \wedge t^2 (r') - t^1 (r) \wedge t^2 (r)) / (r' - r)\).
\(= lim_{r' \to r} (t^1_{m_1, ..., m_{k_1}} (r') t^2_{n_1, ..., n_{k_2}} (r') b^{m_1} \wedge ... \wedge b^{m_{k_1}} \wedge b^{n_1} \wedge ... \wedge b^{n_{k_2}} - t^1_{m_1, ..., m_{k_1}} (r) t^2_{n_1, ..., n_{k_2}} (r) b^{m_1} \wedge ... \wedge b^{m_{k_1}} \wedge b^{n_1} \wedge ... \wedge b^{n_{k_2}}) / (r' - r) = lim_{r' \to r} (t^1_{m_1, ..., m_{k_1}} (r') t^2_{n_1, ..., n_{k_2}} (r') - t^1_{m_1, ..., m_{k_1}} (r) t^2_{n_1, ..., n_{k_2}} (r)) / (r' - r) b^{m_1} \wedge ... \wedge b^{m_{k_1}} \wedge b^{n_1} \wedge ... \wedge b^{n_{k_2}}\).
By the proposition that for any map from any topological space minus any point into any finite-dimensional real vectors space with the canonical topology, the convergence of the map with respect to the point exists if and only if the convergences of the component maps (with respect to any basis) with respect to the point exist, and then, the convergence Is expressed with the convergences, \(d t^1_{m_1, ..., m_{k_1}} / d r = lim_{r' \to r} (t^1_{m_1, ..., m_{k_1}} (r') - t^1_{m_1, ..., m_{k_1}} (r)) / (r' - r)\) and \(d t^2_{n_1, ..., n_{k_2}} / d r = lim_{r' \to r} (t^2_{n_1, ..., n_{k_2}} (r') - t^2_{n_1, ..., n_{k_2}} (r))/ (r' - r)\) exist.
By the well-known fact in real analytics, \(d (t^1_{m_1, ..., m_{k_1}} (r) t^2_{n_1, ..., n_{k_2}} (r)) / d r = lim_{r' \to r} (t^1_{m_1, ..., m_{k_1}} (r') t^2_{n_1, ..., n_{k_2}} (r') - t^1_{m_1, ..., m_{k_1}} (r) t^2_{n_1, ..., n_{k_2}} (r)) / (r' - r)\) exists and equals \(d t^1_{m_1, ..., m_{k_1}} / d r t^2_{n_1, ..., n_{k_2}} (r) + t^1_{m_1, ..., m_{k_1}} d t^2_{n_1, ..., n_{k_2}} (r) / d r\).
By the proposition that for any map from any topological space minus any point into any finite-dimensional real vectors space with the canonical topology, the convergence of the map with respect to the point exists if the convergences of the coefficients with respect to any constant vectors with respect to the point exist, and then, the convergence is expressed with the convergences, \(d (t^1 \wedge t^2) / d r = lim_{r' \to r} (t^1 (r') \wedge t^2 (r') - t^1 (r) \wedge t^2 (r)) / (r' - r)\) exists and equals \((d t^1_{m_1, ..., m_{k_1}} / d r t^2_{n_1, ..., n_{k_2}} (r) + t^1_{m_1, ..., m_{k_1}} d t^2_{n_1, ..., n_{k_2}} (r) / d r) b^{m_1} \wedge ... \wedge b^{m_{k_1}} \wedge b^{n_1} \wedge ... \wedge b^{n_{k_2}}\).
\(= d t^1_{m_1, ..., m_{k_1}} / d r t^2_{n_1, ..., n_{k_2}} (r) b^{m_1} \wedge ... \wedge b^{m_{k_1}} \wedge b^{n_1} \wedge ... \wedge b^{n_{k_2}} + t^1_{m_1, ..., m_{k_1}} d t^2_{n_1, ..., n_{k_2}} (r) / d r b^{m_1} \wedge ... \wedge b^{m_{k_1}} \wedge b^{n_1} \wedge ... \wedge b^{n_{k_2}}= d t^1_{m_1, ..., m_{k_1}} / d r b^{m_1} \wedge ... \wedge b^{m_{k_1}} \wedge t^2_{n_1, ..., n_{k_2}} (r) \wedge b^{n_1} \wedge ... \wedge b^{n_{k_2}} + t^1_{m_1, ..., m_{k_1}} b^{m_1} \wedge ... \wedge b^{m_{k_1}} \wedge d t^2_{n_1, ..., n_{k_2}} (r) / d r \wedge b^{n_1} \wedge ... \wedge b^{n_{k_2}} = d t^1 / d r \wedge t^2 (r) + t^1 (r) \wedge d t^2 / d r\).
