description/proof of that for local diffeomorphism between arbitrary subsets of \(C^\infty\) manifolds with boundary, open neighborhood of domain point, and open neighborhood of point image, diffeomorphism can be chosen to be contained in neighborhoods
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 admits the proposition that any map between arbitrary subsets of any \(C^\infty\) manifolds with boundary locally diffeomorphic at any point is \(C^\infty\) 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 \(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 topological space and any topological subspace that is open on the base space, any subset of the subspace is open on the subspace if and only if it is open on the base space.
Target Context
- The reader will have a description and a proof of 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.
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 }\}\)
\(S_1\): \(\subseteq M_1\)
\(S_2\): \(\subseteq M_2\)
\(f\): \(: S_1 \to S_2\), \(\in \{\text{ the local diffeomorphisms }\}\)
\(s\): \(\in S_1\)
\(U'_s\): \(\in \{\text{ the open neighborhoods of } s \text{ on } S_1\}\)
\(U'_{f (s)}\): \(\in \{\text{ the open neighborhoods of } f (s) \text{ on } S_2\}\)
//
Statements:
\(\exists U_s \in \{\text{ the open neighborhoods of } s \text{ on } S_1\}, \exists U_{f (s)} \in \{\text{ the open neighborhoods of } f (s) \text{ on } S_2\} (U_s \subseteq U'_s \land U_{f (s)} \subseteq U'_{f (s)} \land f \vert_{U_s}: U_s \to U_{f (s)} \in \{\text{ the diffeomorphisms }\})\)
//
2: Note
This proposition tends to be accepted as obvious, but we will prove it for sure, for once.
Typically, \(S_1 = M_1\) and \(S_2 = M_2\), but we do not exclude the other cases.
3: Proof
Whole Strategy: Step 1: take an open neighborhood of \(s\), \(U''_s \subseteq M_1\), and an open neighborhood of \(f (s)\), \(U''_{f (s)} \subseteq M_2\), such that \(f \vert_{U''_s \cap S_1}: U''_s \cap S_1 \to U''_{f (s)} \cap S_2\) is a diffeomorphism; Step 2: take an open neighborhood of \(s\), \(U'''_s \subseteq S_1\), such that \(f (U'''_s) \subseteq U'_{f (s)}\); Step 3: take \(U_s := U'_s \cap U''_s \cap U'''_s\) and \(U_{f (s)} := f (U_s)\), and see that \(U_s \subseteq S_1\) is an open neighborhood of \(s\), \(U_{f (s)} \subseteq S_2\) is an open neighborhood of \(f (s)\), and \(U_s \subseteq U'_s\), \(U_{f (s)} \subseteq U'_{f (s)}\), and \(f \vert_{U_s}: U_s \to U_{f (s)}\) is a diffeomorphism.
Step 1:
Let us take an open neighborhood of \(s\), \(U''_s \subseteq M_1\), and an open neighborhood of \(f (s)\), \(U''_{f (s)} \subseteq M_2\), such that \(f \vert_{U''_s \cap S_1}: U''_s \cap S_1 \to U''_{f (s)} \cap S_2\) is a diffeomorphism, which is possible because \(f\) is a local diffeomorphism.
Step 2:
Let us take an open neighborhood of \(s\), \(U'''_s \subseteq S_1\), such that \(f (U'''_s) \subseteq U'_{f (s)}\), which is possible because \(f\) is continuous, by the proposition that any map between arbitrary subsets of any \(C^\infty\) manifolds with boundary locally diffeomorphic at any point is \(C^\infty\) at the point: being \(C^\infty\) implies being continuous as is mentions in Note for the definition of map between arbitrary subsets of \(C^\infty\) manifolds with boundary \(C^k\) at point, where \(k\) excludes \(0\) and includes \(\infty\).
Step 3:
Let us take \(U_s := U'_s \cap U''_s \cap U'''_s\) and \(U_{f (s)} := f (U_s)\).
\(U_s \subseteq S_1\) is an open neighborhood of \(s\), because \(s \in U_s\), and \(U_s\) is an open subset of \(S_1\), because \(U_s = U'_s \cap U''_s \cap U'''_s \cap S_1 = U'_s \cap (U''_s \cap S_1) \cap U'''_s\), but \(U''_s \cap S_1\) is open on \(S_1\) by the definition of subspace topology and \(U'_s\) and \(U'''_s\) are open on \(S_1\).
\(U_{f (s)} \subseteq S_2\) is an open neighborhood of \(f (s)\), because \(f (s) \in U_{f (s)}\), because as \(s \in U_s\), \(f (s) \in f (U_s) = U_{f (s)}\), \(U_{f (s)}\) is a subset of \(S_2\), because as \(U_s \subseteq U'''_s\), \(f (U_s) \subseteq f (U'''_s) \subseteq U'_{f (s)} \subseteq S_2\), and it is open on \(S_2\), because \(U_s := U'_s \cap U''_s \cap U'''_s\) is open on \(U''_s \cap S_1\) because \(= U''_s \cap S_1 \cap (U'_s \cap U'''_s) = (U''_s \cap S_1) \cap U''''_s \cap S_1\) where \(U''''_s \subseteq M_1\) is an open neighborhood of \(s\) on \(M_1\), \(= (U''_s \cap S_1) \cap U''''_s\), so, \(f (U_s)\) is open on \(U''_{f (s)} \cap S_2\) because \(f \vert_{U''_s \cap S_1}: U''_s \cap S_1 \to U''_{f (s)} \cap S_2\) is a diffeomorphism, but as \(U''_{f (s)} \cap S_2\) is open on \(S_2\), \(f (U_s)\) is open on \(S_2\), by the proposition that for any topological space and any topological subspace that is open on the base space, any subset of the subspace is open on the subspace if and only if it is open on the base space.
\(U_s \subseteq U'_s\).
\(U_{f (s)} \subseteq U'_{f (s)}\), because \(U_s \subseteq U'''_s\), and \(f (U_s) \subseteq f (U'''_s) \subseteq U'_{f (s)}\).
\(f \vert_{U_s}: U_s \to U_{f (s)}\) is a diffeomorphism, because it is a bijection as the restriction of the bijective \(f \vert_{U''_s \cap S_1}: U''_s \cap S_1 \to U''_{f (s)} \cap S_2\), and it 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 and 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, and its inverse is \(C^\infty\), likewise.
