A description/proof of that for diffeomorphism from \(C^\infty\) manifold with boundary onto neighborhood of point image on \(C^\infty\) manifold with boundary, differential at point is 'vectors spaces - linear morphisms' isomorphism
Topics
About: \(C^\infty\) manifold
The table of contents of this article
Starting Context
- The reader knows a definition of \(C^\infty\) manifold with boundary.
- The reader knows a definition of neighborhood of point.
- The reader knows a definition of map between arbitrary subsets of \(C^\infty\) manifolds with boundary \(C^k\) at point, where \(k\) excludes \(0\) and includes \(\infty\).
- The reader knows a definition of diffeomorphism between arbitrary subsets of \(C^\infty\) manifolds with boundary.
- The reader knows a definition of differential of \(C^\infty\) map between \(C^\infty\) manifolds with boundary at point.
- The reader knows a definition of %category name% isomorphism.
- The reader admits the proposition that any \(C^\infty\) manifold with boundary is locally compact.
- The reader admits the proposition that for any locally compact Hausdorff topological space, in any neighborhood around any point, there is an open neighborhood of the point whose (the open neighborhood's) closure is compact and contained in the former neighborhood.
- 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 maps between any arbitrary subsets of any \(C^\infty\) manifolds with boundary \(C^k\) at corresponding points, where \(k\) includes \(\infty\), the composition is \(C^k\) at the point.
- The reader admits the proposition that for any \(C^\infty\) function from any closed subset of any \(C^\infty\) manifold with boundary and any open neighborhood of the closed subset, there is a \(C^\infty\) extension over the manifold with boundary that is supported in the open neighborhood.
- The reader admits the proposition that any tangent vector at any point on any \(C^\infty\) manifold with boundary is realized by a \(C^\infty\) curve.
- The reader admits the proposition that any bijective linear morphism is a 'vectors spaces - linear morphisms' isomorphism.
Target Context
- The reader will have a description and a proof of the proposition that for any diffeomorphism from any \(C^\infty\) manifold with boundary onto any neighborhood of any point image on any \(C^\infty\) manifold with boundary, the differential of the diffeomorphism or any its codomain extension at the point is a 'vectors spaces - linear morphisms' isomorphism.
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: Note
For any diffeomorphism between any \(C^\infty\) manifolds with boundary, the corresponding proposition is well-known; this proposition is on the case that the codomain is not any whole \(C^\infty\) manifold with boundary.
The domain has to be the whole \(C^\infty\) manifold with boundary, because the definition of differential requires that \(g \circ f\) is a \(C^\infty\) function over the whole \(C^\infty\) manifold with boundary, unless the definition of differential is extended somehow.
2: Description
For any \(C^\infty\) manifolds with (possibly empty) boundary, \(M_1, M_2\), any point, \(p \in M_1\), and any diffeomorphism, \(f: M_1 \to N_{f (p)}\), where \(N_{f (p)} \subseteq M_2\) is any neighborhood of \(f (p)\), the differential of \(f\) at \(p\), \(d f \vert_p: T_pM_1 \to T_{f (p)}M_2\) is a 'vectors spaces - linear morphisms' isomorphism.
In fact, for any subset, \(S \subseteq M_2\), such that \(N_{f (p)} \subseteq S\) (especially, \(S = M_2\)), and the extension of \(f\) on the codomain, \(f': M_1 \to S\), such that \(f' = f\), \(d f' \vert_p: T_pM_1 \to T_{f (p)}M_2\) is a 'vectors spaces - linear morphisms' isomorphism.
3: Proof
Let us prove that \(d f \vert_p\) is injective.
Let \(v \neq v' \in T_pM_1\) be any tangent vector.
\(d f \vert_p v \neq d f \vert_p v'\)? Is there a \(C^\infty\) function, \(g: M_2 \to \mathbb{R}\), such that \(d f \vert_p v (g) \neq d f \vert_p v' (g)\)?
\(d f \vert_p v (g) = v (g \circ f)\); \(d f \vert_p v' (g) = v' (g \circ f)\).
There is a \(C^\infty\) function, \(h: M_1 \to \mathbb{R}\), such that \(v (h) \neq v' (h)\).
As \(M_2\) is locally compact Hausdorff, by the proposition that any \(C^\infty\) manifold with boundary is locally compact, there is an open neighborhood, \(U_{f (p)} \subseteq M_2\), of \(f (p)\) such that \(\overline{U_{f (p)}} \subseteq N_{f (p)}\), by the proposition that for any locally compact Hausdorff topological space, in any neighborhood around any point, there is an open neighborhood of the point whose (the open neighborhood's) closure is compact and contained in the former neighborhood.
\(f^{-1} \vert_{\overline{U_{f (p)}}}: \overline{U_{f (p)}} \to M_1\) is \(C^\infty\) over \(\overline{U_{f (p)}}\), 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. \(h \circ f^{-1} \vert_{\overline{U_{f (p)}}}: \overline{U_{f (p)}} \to \mathbb{R}\) is \(C^\infty\) over \(\overline{U_{f (p)}}\), by the proposition that for any maps between any arbitrary subsets of any \(C^\infty\) manifolds with boundary \(C^k\) at corresponding points, where \(k\) includes \(\infty\), the composition is \(C^k\) at the point.
There is a \(C^\infty\) extension, \(g: M_2 \to \mathbb{R}\), such that \(g \vert_{\overline{U_{f (p)}}} = h \circ f^{-1} \vert_{\overline{U_{f (p)}}}\), by the proposition that for any \(C^\infty\) function from any closed subset of any \(C^\infty\) manifold with boundary and any open neighborhood of the closed subset, there is a \(C^\infty\) extension over the manifold with boundary that is supported in the open neighborhood.
As \(f\) is continuous at \(p\), there is an open neighborhood, \(U_p \subseteq M_1\), of \(p\) such that \(f (U_p) \subseteq U_{f (p)}\). \(g \circ f \vert_{U_p} = h \circ f^{-1} \vert_{\overline{U_{f (p)}}} \circ f \vert_{U_p} = h \vert_{U_p}\). As any tangent vector is a local operator, its action depends only on any open neighborhood of the point, and so, \(v (g \circ f) = v (h) \neq v' (h) = v' (g \circ f)\).
So, yes, there is a \(g\) such that \(d f \vert_p v (g) = v (g \circ f) \neq v' (g \circ f) = d f \vert_p v' (g)\), and yes, \(d f \vert_p v \neq d f \vert_p v'\), and \(d f \vert_p\) is injective.
Let us prove that \(d f \vert_p\) is surjective.
As any tangent vector on \(T_{f (p)}M_2\) is realized by a \(C^\infty\) curve, \(\gamma: J \to U_{f (p)}\), where \(J = (- \epsilon, \epsilon)\text{, } [0, \epsilon)\text{, or } (- \epsilon, 0]\), by the proposition that any tangent vector at any point on any \(C^\infty\) manifold with boundary is realized by a \(C^\infty\) curve, let us specify a \(C^\infty\) curve, \(\gamma': J \to M_1\), such that \(\gamma = f \circ \gamma'\).
\(\gamma' := f^{-1} \circ \gamma\) will do, because \(f \circ \gamma' = f \circ f^{-1} \circ \gamma = \gamma\). \(\gamma'\) is indeed \(C^\infty\), by the proposition that for any maps between any arbitrary subsets of any \(C^\infty\) manifolds with boundary \(C^k\) at corresponding points, where \(k\) includes \(\infty\), the composition is \(C^k\) at the point.
When \(p\) is a boundary point, whatever the type of \(J\) is, \(\gamma'\) realizes a tangent vector on \(T_pM_1\).
When \(p\) is not any boundary point and \(J = (- \epsilon, \epsilon)\), \(\gamma'\) realizes a tangent vector on \(T_pM_1\).
When \(p\) is not any boundary point and \(J = [0, \epsilon) \text{ or } (- \epsilon, 0]\), there are a positive \(\epsilon' \le \epsilon\) and a chart, \((U_p \subseteq M_1, \phi_p)\), and \(J' := [0, \epsilon') \text{ or } (- \epsilon', 0]\) and \(\phi_p \circ \gamma' \vert_{J'}: J' \to \phi_p (U_p)\) is \(C^\infty\), and so, there is a \(C^\infty\) extension, \(\gamma'': (- \epsilon'', \epsilon'') \to \mathbb{R}^d\), of \(\phi_p \circ \gamma' \vert_{J'}\), where \(\epsilon''\) can be and will be chosen such that \(\epsilon'' \le \epsilon'\), but as \(\gamma''\) is continuous at \(0\), \(\epsilon''\) can be chosen such that \(\gamma'' ((- \epsilon'', \epsilon'')) \subseteq \phi_p (U_p) \subseteq \mathbb{R}^d\) because \(\phi_p (U_p)\) is open on \(\mathbb{R}^d\), and let us define \(\gamma''': (- \epsilon'', \epsilon'') \to M_1 = {\phi_p}^{-1} \circ \gamma''\), which realizes a tangent vector on \(T_pM_1\), still satisfying \(\gamma \vert_{[0, \epsilon'') \text{ or } (- \epsilon'', 0]} = f \circ \gamma''' \vert_{[0, \epsilon'') \text{ or } (- \epsilon'', 0]}\), because \(f \circ \gamma''' \vert_{[0, \epsilon'') \text{ or } (- \epsilon'', 0]} = f \circ {\phi_p}^{-1} \circ \gamma'' \vert_{[0, \epsilon'') \text{ or } (- \epsilon'', 0]} = f \circ {\phi_p}^{-1} \circ \phi_p \circ \gamma' \vert_{[0, \epsilon'') \text{ or } (- \epsilon'', 0]} = f \circ \gamma' \vert_{[0, \epsilon'') \text{ or } (- \epsilon'', 0]} = \gamma \vert_{[0, \epsilon'') \text{ or } (- \epsilon'', 0]}\). In fact, \(\gamma\) could be taken to be from \((- \epsilon'', \epsilon'')\) in the first place.
\(d f \vert_p\) indeed maps the tangent vector realized by \(\gamma'\) (or \(\gamma'''\), but we will call both \(\gamma'\) hereafter) to the tangent vector realized by \(\gamma\), because \(d f \vert_p d \gamma' / d t \vert_0 (g) = d \gamma' / d t \vert_0 (g \circ f) = d (g \circ f \circ \gamma') / d t \vert_0 = d (f \circ \gamma') / d t \vert_0 (g) = d \gamma / d t \vert_0 (g)\).
So, \(d f \vert_p\) is surjective.
\(d f \vert_p\) is a 'vectors spaces - linear morphisms' isomorphism, by the proposition that any bijective linear morphism is a 'vectors spaces - linear morphisms' isomorphism.
For \(d f' \vert_p\), in fact, \(d f' \vert_p = d f \vert_p\), because \(d f' \vert_p v (g) = v (g \circ f') = v (g \circ f) = d f \vert_p v (g)\).
So, \(d f' \vert_p\) is a 'vectors spaces - linear morphisms' isomorphism.
