A description/proof of that for map between arbitrary subsets of \(C^\infty\) manifolds with boundary \(C^k\) at point, restriction or expansion on codomain that contains range is \(C^k\) at point
Topics
About: \(C^\infty\) manifold with boundary
The table of contents of this article
Starting Context
Target Context
- The reader will have a description and a proof of 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.
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: Description
For any \(C^\infty\) manifolds with (possibly empty) boundary, \(M_1, M_2\), any subsets, \(S_1 \subseteq M_1, S_2 \subseteq M_2\), any point, \(p \in S_1\), any natural number (including 0) or \(\infty\) \(k\), any map, \(f: S_1 \to S_2\), such that \(f\) is \(C^k\) at \(p\), and any subset, \(S'_2 \subseteq M_2\), such that \(f (S_1) \subseteq S'_2\), the codomain restriction or expansion, \(f': S_1 \to S'_2\) is \(C^k\) at \(p\).
2: Proof
Let us suppose that \(k = 0\).
Let \(U_{f' (p)} \subseteq S'_2\) be any open neighborhood of \(f' (p)\). \(U_{f' (p)} = U'_{f' (p)} \cap S'_2\), where \(U'_{f' (p)} \subseteq M_2\) is an open neighborhood of \(f' (p)\) on \(M_2\). Let \(U''_{f' (p)} = U'_{f' (p)} \cap S_2 \subseteq S_2\) be the open neighborhood of \(f' (p)\) on \(S_2\). There is an open neighborhood, \(U_p \subseteq S_1\), of \(p\) such that \(f' (U_p) = f (U_p) \subseteq U''_{f' (p)}\). Then, \(f' (U_p) \subseteq U_{f' (p)}\), because \(f' (U_p) \subseteq U'_{f' (p)} \cap S'_2 = U_{f' (p)}\).
Let us suppose that \(1 \le k\) including \(\infty\).
There are a chart, \((U'_p \subseteq M_1, \phi'_p)\), around \(p\) and a chart, \((U_{f (p)} \subseteq M_2, \phi_{f (p)})\), around \(f (p)\) such that \(f (U'_p \cap S_1) \subseteq U_{f (p)}\) and \(\phi_{f (p)} \circ f \circ {\phi'_p}^{-1} \vert_{\phi'_p (U'_p \cap S_1)}: \phi'_p (U'_p \cap S_1) \to \phi_{f (p)} (U_{f (p)})\) is \(C^k\) at \(\phi'_p (p)\).
But the same charts pair can be used for \(f'\), because \(f' (U'_p \cap S_1) \subseteq U_{f (p)}\) and \(\phi_{f (p)} \circ f' \circ {\phi'_p}^{-1} \vert_{\phi'_p (U'_p \cap S_1)}: \phi'_p (U'_p \cap S_1) \to \phi_{f (p)} (U_{f (p)})\) is \(C^k\) at \(\phi'_p (p)\).
