description/proof of that rough vectors field over \(C^\infty\) manifold with boundary is \(C^\infty\) if and only if operation result on any \(C^\infty\) function is \(C^\infty\)
Topics
About: \(C^\infty\) manifold
The table of contents of this article
Starting Context
- The reader knows a definition of \(C^\infty\) manifold with boundary.
- The reader knows a definition of rough vectors field over \(C^\infty\) manifold with boundary.
- The reader admits the proposition that for any \(C^\infty\) function on any point open neighborhood of any \(C^\infty\) manifold, there exists a \(C^\infty\) function on the whole manifold that equals the original function on a possibly smaller neighborhood of the point.
Target Context
- The reader will have a description and a proof of the proposition that any rough vectors field over any \(C^\infty\) manifold with boundary is \(C^\infty\) if and only if its operation result on any \(C^\infty\) function is \(C^\infty\).
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 } C^\infty \text{ manifolds with boundary }\}\)
\((TM, M, \pi)\): \(= \text{ the } C^\infty \text{ tangent vectors bundle }\)
\(s\): \(: M \to TM\), \(\in \{\text{ the rough sections of } \pi\}\)
//
Statements:
\(s \in \{\text{ the } C^\infty \text{ maps }\}\)
\(\iff\)
\(\forall f \in \{\text{ the } C^\infty \text{ functions over } M\} (s f \in \{\text{ the } C^\infty \text{ functions over } M\})\)
//
2: Proof
Whole Strategy: Step 1: suppose that \(s f\) is \(C^\infty\), and see that \(s\) is \(C^\infty\), by taking a chart, \((U_m \subseteq M, \phi_m)\), and the induced chart, \((\pi^{-1} (U_m) \subseteq TM, \widetilde{\phi_m})\); Step 2: suppose that \(s\) is \(C^\infty\), and see that \(s f\) is \(C^\infty\), by taking a chart, \((U_m \subseteq M, \phi_m)\), and the induced chart, \((\pi^{-1} (U_m) \subseteq TM, \widetilde{\phi_m})\).
Step 1:
Let us suppose that \(s f\) is \(C^\infty\).
Let \(m \in M\) be any.
There are a chart around \(m\), \((U_m \subseteq M, \phi_m)\), and the induced chart, \((\pi^{-1} (U_m) \subseteq TM, \widetilde{\phi_m})\).
\(s = s^j \partial / \partial x^j\) over there.
Each coordinate function, \(x^j: U_m \to \mathbb{R}\), is a \(C^\infty\) function.
There is a \(C^\infty\) function, \(\widetilde{x^j}: M \to \mathbb{R}\), over \(M\) that equals \(x^j\) on a possibly smaller open neighborhood of \(m\), \(U'_m \subseteq U_m\), by the proposition that for any \(C^\infty\) function on any point open neighborhood of any \(C^\infty\) manifold, there exists a \(C^\infty\) function on the whole manifold that equals the original function on a possibly smaller neighborhood of the point.
Over \(U'_m\), \(s \widetilde{x^l} = s^j \partial / \partial x^j \widetilde{x^l} = s^j \partial / \partial x^j x^l = s^j \delta^l_j = s^l\), \(C^\infty\) over \(U'_m\), by the supposition.
So, with respect to the charts, \((U'_m \subseteq M, \phi_m \vert_{U'_m})\) and \((\pi^{-1} (U'_m) \subseteq TM, \widetilde{\phi_m \vert_{U'_m}})\), the components function of \(s\) is \(C^\infty\).
So, \(s\) is \(C^\infty\) over \(M\).
Step 2:
Let us suppose that \(s\) is \(C^\infty\).
Let \(m \in M\) be any point.
There are a chart around \(m\), \((U_m \subseteq M, \phi_m)\), and the induced chart, \((\pi^{-1} (U_m) \subseteq TM, \widetilde{\phi_m})\).
Over \(U_m\), \(s = s^j \partial / \partial x^j\), where \(s^j: U_m \to \mathbb{R}\) is \(C^\infty\).
Over \(U_m\), \(s f = s^j \partial / \partial x^j f = s^j \partial_j f\), which is \(C^\infty\).
As \(s f\) is \(C^\infty\) over a neighborhood of each point on \(M\), it is \(C^\infty\) over \(M\).
