description/proof of that exterior derivation of \(C^\infty\) function over \(C^\infty\) manifold with boundary satisfies Leibniz rule
Topics
About: \(C^\infty\) manifold
The table of contents of this article
Starting Context
Target Context
- The reader will have a description and a proof of the proposition that the exterior derivation of \(C^\infty\) function over \(C^\infty\) manifold with boundary 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:
\(M\): \(\in \{\text{ the } d \text{ -dimensional } C^\infty \text{ manifolds with boundary }\}\)
\(d\): \(: \Omega_0 (TM) \to \Omega_1 (TM)\), \(= \text{ the exterior derivation of function }\)
\(f_1\): \(\in \Omega_0 (TM)\)
\(f_2\): \(\in \Omega_0 (TM)\)
//
Statements:
\(d (f_1 f_2) = f_2 d f_1 + f_1 d f_2\)
//
2: Proof
Whole Strategy: Step 1: for each \(m \in M\), take any chart, \((U_m \subseteq M, \phi_m)\), and take the chart expression of \(d (f_1 f_2)\), and see that \(d (f_1 f_2) = f_2 d f_1 + f_1 d f_2\) in the chart expressions.
Step 1:
Let \(m \in M\) be any.
Let \((U_m \subseteq M, \phi_m)\) be any chart around \(m\).
With respect to the chart, \(d (f_1 f_2) = \partial (f_1 f_2) / \partial x^j d x^j\), by Note for the definition of exterior derivative of \(C^\infty\) function over \(C^\infty\) manifold with boundary.
\(= (f_2 \partial f_1 / \partial x^j + f_1 \partial f_2 / \partial x^j) d x^j\), because any tangent vector is a derivation.
\(= f_2 (\partial f_1 / \partial x^j d x^j) + f_1 (\partial f_2 / \partial x^j d x^j) = f_2 d f_1 + f_1 d f_2\).
