description/proof of that for surjective local diffeomorphism between \(C^\infty\) manifolds with boundary and section along open subset of codomain, section is \(C^\infty\)
Topics
About: \(C^\infty\) manifold
The table of contents of this article
Starting Context
- The reader knows a definition of map between arbitrary subsets of \(C^\infty\) manifolds with boundary locally diffeomorphic at point.
- The reader knows a definition of surjection.
- The reader knows a definition of section along subset of codomain of continuous surjection.
- The reader admits the proposition that for any local diffeomorphism between any arbitrary subsets of any \(C^\infty\) manifolds with boundary, any open neighborhood of any domain point, and any open neighborhood of the point image, a diffeomorphism can be chosen to be contained in the neighborhoods.
- The reader admits the proposition that for any map between any arbitrary subsets of any \(C^\infty\) manifolds with boundary \(C^k\) at any point, where \(k\) includes \(\infty\), the restriction or expansion on any codomain that contains the range is \(C^k\) at the point.
- The reader admits the proposition that for any map between any arbitrary subsets of any \(C^\infty\) manifolds with boundary \(C^k\) at any point, where \(k\) includes \(\infty\), the restriction on any domain that contains the point is \(C^k\) at the point.
- The reader admits the proposition that for any map between any arbitrary subsets of any \(C^\infty\) manifolds with boundary, the map is \(C^k\) at any point if the restriction on any subspace open neighborhood of the point domain is \(C^k\) at the point, where \(k\) includes \(\infty\).
Target Context
- The reader will have a description and a proof of the proposition that for any surjective local diffeomorphism between any \(C^\infty\) manifolds with boundary and any section along any open subset of the codomain, the section 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_1\): \(\in \{\text{ the } C^\infty \text{ manifolds with boundary }\}\)
\(M_2\): \(\in \{\text{ the } C^\infty \text{ manifolds with boundary }\}\)
\(f\): \(: M_1 \to M_2\), \(\in \{\text{ the surjections }\} \land \{\text{ the local diffeomorphisms }\}\)
\(U_2\): \(\in \{\text{ the open subsets of } M_2\}\)
\(s\): \(: U_2 \to M_1\), \(\in \{\text{ the sections of } f \text{ along } U_2\}\)
//
Statements:
\(s \in \{\text{ the } C^\infty \text{ maps }\}\)
//
2: Note
So, \(s\) inevitably becomes \(C^\infty\) by virtue of \(f\) being a local diffeomorphism.
As Proof shows, this proposition is possible because \(s\) is guaranteed to be continuous by definition.
3: Proof
Whole Strategy: Step 1: take any \(u \in U_2\), an open neighborhood of \(s (u)\), \(U'_{s (u)} \subseteq M_1\), and an open neighborhood of \(u\), \(U'_u \subseteq M_2\), such that \(U'_u \subseteq U_2\) and \(f \vert_{U'_{s (u)}}: U'_{s (u)} \to U'_u\) is a diffeomorphism; Step 2: take an open neighborhood of \(u\), \(U_u \subseteq U_2\), such that \(U_u \subseteq U'_u\) and \(s (U_u) \subseteq U'_{s (u)}\); Step 3: see that \(s \vert_{U_u}: U_u \to U'_{s (u)}\) is the restriction of \({f \vert_{U'_{s (u)}}}^{-1}\).
Step 1:
Let \(u \in U_2\) be any.
\(f (s (u)) = u\).
Let us take an open neighborhood of \(s (u)\), \(U'_{s (u)} \subseteq M_1\), and an open neighborhood of \(u\), \(U'_u \subseteq M_2\), such that \(U'_u \subseteq U_2\) and \(f \vert_{U'_{s (u)}}: U'_{s (u)} \to U'_u\) is a diffeomorphism, which is possible by the proposition that for any local diffeomorphism between any arbitrary subsets of any \(C^\infty\) manifolds with boundary, any open neighborhood of any domain point, and any open neighborhood of the point image, a diffeomorphism can be chosen to be contained in the neighborhoods.
Step 2:
Let us take an open neighborhood of \(u\), \(U_u \subseteq U_2\), such that \(U_u \subseteq U'_u\) and \(s (U_u) \subseteq U'_{s (u)}\), which is possible because \(s\) is continuous by definition: if \(U_u\) is not contained in \(U'_u\), \(U_u \cap U'_u\) can be taken to be \(U_u\) instead.
Step 3:
Let us think of \(s \vert_{U_u}: U_u \to U'_{s (u)}\).
\({f \vert_{U'_{s (u)}}}^{-1}: U'_u \to U'_{s (u)}\) is \(C^\infty\).
\(s \vert_{U_u}\) is the domain restriction of \({f \vert_{U'_{s (u)}}}^{-1}\), because for each \(u' \in U_u\), \(f \circ s \vert_{U_u} (u') = u'\), but as \(s \vert_{U_u} (u') \in U'_{s (u)}\), \(f \circ s \vert_{U_u} (u') = f \vert_{U'_{s (u)}} \circ s \vert_{U_u} (u')\), so, \({f \vert_{U'_{s (u)}}}^{-1} \circ f \vert_{U'_{s (u)}} \circ s \vert_{U_u} (u') = {f \vert_{U'_{s (u)}}}^{-1} (u')\), but the left hand side is \(s \vert_{U_u} (u')\).
So, \(s \vert_{U_u}\) is \(C^\infty\), by the proposition that for any map between any arbitrary subsets of any \(C^\infty\) manifolds with boundary \(C^k\) at any point, where \(k\) includes \(\infty\), the restriction on any domain that contains the point is \(C^k\) at the point.
Also the codomain extension, \(s \vert_{U_u}: U_u \to M_1\), is \(C^\infty\), by the proposition that for any map between any arbitrary subsets of any \(C^\infty\) manifolds with boundary \(C^k\) at any point, where \(k\) includes \(\infty\), the restriction or expansion on any codomain that contains the range is \(C^k\) at the point.
So, \(s: U_2 \to M_1\) is \(C\infty\), by the proposition that for any map between any arbitrary subsets of any \(C^\infty\) manifolds with boundary, the map is \(C^k\) at any point if the restriction on any subspace open neighborhood of the point domain is \(C^k\) at the point, where \(k\) includes \(\infty\).
