description/proof of that for \(C^\infty\) manifold with boundary and local \(C^\infty\) frame on cotangent vectors bundle, predual local frame 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\) \(q\)-covectors bundle over \(C^\infty\) manifold with boundary.
- The reader knows a definition of local \(C^\infty\) frame on \(C^\infty\) vectors bundle.
- The reader knows a definition of predual basis for finite-dimensional vectors space of basis for covectors space.
- The reader knows a definition of exterior derivative of \(C^\infty\) function over \(C^\infty\) manifold with boundary.
- The reader admits the proposition that for any \(C^\infty\) vectors bundle, any rough section over any trivializing open subset is \(C^\infty\) if and only if the coefficients of the rough section with respect to any local \(C^\infty\) frame over the trivializing open subset are \(C^\infty\).
- The reader admits the proposition that for any \(C^\infty\) vectors bundle, any \(C^\infty\) frame exists over and only over any trivializing open subset.
- The reader admits the proposition that any rough vectors field is \(C^\infty\) if and only if its operation result on any \(C^\infty\) function is \(C^\infty\).
Target Context
- The reader will have a description and a proof of the proposition that for any \(C^\infty\) manifold with boundary and any local \(C^\infty\) frame on the cotangent vectors bundle, the predual local frame 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 } d \text{ -dimensional } C^\infty \text{ manifolds with boundary }\}\)
\((TM^*, M, \pi^*)\): \(= \text{ the cotangent vectors bundle }\)
\((TM, M, \pi)\): \(= \text{ the tangent vectors bundle }\)
\(U\): \(\in \{\text{ the open subsets of } M\}\)
\(\{t^1, ..., t^d\}\): \(\in \{\text{ the local } C^\infty \text{ frames over } U \text{ on } TM^*\}\)
\(\{v_1, ..., v_d\}\): \(= \text{ the predual local frame of } \{t^1, ..., t^d\}\)
//
Statements:
\(\{v_1, ..., v_d\} \in \{\text{ the local } C^\infty \text{ frames over } U \text{ on } TM\}\)
//
2: Proof
Whole Strategy: Step 1: see what "the predual local frame of \(\{t^1, ..., t^d\}\)" means; Step 2: see that \(v_j\) is \(C^\infty\).
Step 1:
Let us see what "the predual local frame of \(\{t^1, ..., t^d\}\)" means.
For each \(u \in U\), \(\{t^1 (u), ..., t^d (u)\}\) is a basis for \({\pi^*}^{-1} (u)\).
\(\{v_1 (u), ..., v_d (u)\}\) is the predual basis of \(\{t^1 (u), ..., t^d (u)\}\).
So, we have defined for each \(j \in \{1, ..., d\}\), \(v_j: U \to \pi^{-1} (U)\).
\(\pi (v_j (u)) = u\), so, \(v_j\) is a rough section.
The remaining issue is whether \(v_j\) is \(C^\infty\) (then, inevitably is continuous).
Step 2:
Let \(f: U \to \mathbb{R}\) be any \(C^\infty\) function.
For each \(l \in \{1, ..., d\}\), \(v_l (f) = d f (v_l)\), where \(d f \) is the exterior derivative of \(f\).
\(d f\) is a \(C^\infty\) 1-form, by Note for the definition of exterior derivative of \(C^\infty\) function over \(C^\infty\) manifold with boundary.
So, \(d f = (d f)_j t^j\), where \((d f)_j: U \to \mathbb{R}\) is a \(C\infty\) function, by the proposition that for any \(C^\infty\) vectors bundle, any rough section over any trivializing open subset is \(C^\infty\) if and only if the coefficients of the rough section with respect to any local \(C^\infty\) frame over the trivializing open subset are \(C^\infty\): \(U\) is a trivializing open subset, by the proposition that for any \(C^\infty\) vectors bundle, any \(C^\infty\) frame exists over and only over any trivializing open subset.
So, \(v_l (f) = d f (v_l) = (d f)_j t^j (v_l) = (d f)_j \delta^j_l = (d f)_l\), which is \(C^\infty\).
So, \(v_l\) is \(C^\infty\), by the proposition that any rough vectors field is \(C^\infty\) if and only if its operation result on any \(C^\infty\) function is \(C^\infty\).
