description/proof of that for \(C^\infty\) vectors bundle and set of local \(C^\infty\) sections over open domain that is linearly independent, of each point of domain, there is possibly smaller open neighborhood over which there is local \(C^\infty\) frame that contains restricted sections set
Topics
About: \(C^\infty\) manifold
The table of contents of this article
Starting Context
- The reader knows a definition of local \(C^\infty\) frame on \(C^\infty\) vectors bundle.
- The reader admits the proposition that for any \(C^\infty\) vectors bundle, any \(C^\infty\) section along any closed subset of the base space can be extended to over the whole base space with the support contained in any open neighborhood of the subset.
- The reader admits the proposition that the set of any \(C^\infty\) sections of any \(C^\infty\) vectors bundle that (the set) is linearly independent at a point is linearly independent on an open neighborhood of the point.
Target Context
- The reader will have a description and a proof of the proposition that for any \(C^\infty\) vectors bundle and any set of local \(C^\infty\) sections over any open domain that is linearly independent, of each point of the domain, there is a possibly smaller open neighborhood over which there is a local \(C^\infty\) frame that contains the restricted sections set.
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:
\((E, M, \pi)\): \(\in \{\text{ the } C^\infty \text{ vectors bundles of rank } k\}\)
\(U\): \(\in \{\text{ the open subsets of } M\}\)
\(\{s_1, ..., s_n\}\): \(s_j: U \to E \in \{\text{ the local } C^\infty \text{ sections of } \pi\}\) such that \(\forall u \in U (\{s_1 (u), ..., s_n (u)\} \in \{\text{ the linearly independent subsets of } \pi^{-1} (u)\})\)
//
Statements:
\(\forall u \in U (\exists U_u \subseteq M \in \{\text{ the open neighborhoods of } u\} \text{ such that } U_u \subseteq U, \exists \{s_{n + 1}, ..., s_k\} \text{ where } s_{n + j}: M \to E \in \{\text{ the } C^\infty \text{ sections of } \pi\} (\{s_1 \vert_{U_u}, ..., s_k \vert_{U_u}\} \in \{\text{ the local } C^\infty \text{ frames }\}))\)
//
2: Proof
Whole Strategy: Step 1: take any basis for \(\pi^{-1} (u)\), \(\{s_1 (u), ..., s_n (u), v_{n + 1}, ..., v_k\}\); Step 2: for each \(j \in \{1, ..., k - n\}\), take a \(C^\infty\) section of \(\pi\), \(s_{n + j}: M \to E\), such that \(s_{n + j} (u) = v_{n + j}\); Step 3: see that there is an open neighborhood of \(u\), \(U_u \subseteq M\), such that \(U_u \subseteq U\) over which \(\{s_1, ..., s_n, s_{n + 1}, ..., s_k\}\) is linearly independent.
Step 1:
There is a basis for \(\pi^{-1} (u)\), \(\{s_1 (u), ..., s_n (u), v_{n + 1}, ..., v_k\}\).
Step 2:
Let \(j \in \{1, ..., k - n\}\) be any.
\(\{u\} \subseteq M\) is a closed subset of \(M\).
\(s_{n + j}: \{u\} \to E, u \mapsto v_{n + j}\) is a \(C^\infty\) section along \(\{u\}\): take a trivializing chart around \(u\) and the corresponding chart for \(E\), then, the components function of \(s_{n + j}\) has the obvious \(C^\infty\) extension over the trivializing chart, \(: x \mapsto (v_{n + j}^1, ..., v_{n + j}^k, x)\).
There is a \(C^\infty\) section of \(\pi\), \(s_{n + j}: M \to E\), such that \(s_{n + j} (u) = v_{n + j}\), by the proposition that for any \(C^\infty\) vectors bundle, any \(C^\infty\) section along any closed subset of the base space can be extended to over the whole base space with the support contained in any open neighborhood of the subset.
Step 3:
Now, we have a set of local \(C^\infty\) sections over \(U\), \(\{s_1, ..., s_n, s_{n + 1} \vert_U, ..., s_k \vert_U\}\), such that \(\{s_1 (u), ..., s_k (u)\}\) is linearly independent.
There is an open neighborhood of \(u\), \(U_u \subseteq M\), such that \(U_u \subseteq U\) over which \(\{s_1, ..., s_k\}\) is linearly independent, by the proposition that the set of any \(C^\infty\) sections of any \(C^\infty\) vectors bundle that (the set) is linearly independent at a point is linearly independent on an open neighborhood of the point: although the proposition ostensibly requires the sections to be over the entire \(M\), the proposition can be applied to this case with the local sections as is clear from that Proof.
So, \(\{s_1 \vert_{U_u}, ..., s_k \vert_{U_u}\}\) is a local \(C^\infty\) frame over \(U_u\).
