description/proof of that for \(C^\infty\) manifold with boundary and regular domain, differential of inclusion at point on regular domain is 'vectors spaces - linear morphisms' isomorphism
Topics
About: \(C^\infty\) manifold
The table of contents of this article
- Starting Context
- Target Context
- Orientation
- Main Body
- 1: Structured Description
- 2: Natural Language Description
- 3: Proof
Starting Context
- The reader knows a definition of regular domain of \(C^\infty\) manifold 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 for any \(C^\infty\) manifold with boundary, any embedded submanifold with boundary of the manifold with boundary is properly embedded if and only if it is closed.
- The reader admits the proposition that for any \(C^\infty\) manifold with boundary, any closed subset, and any open neighborhood of the subset, any \(C^\infty\) map from the subset into \(\mathbb{R}^n\) can be extended to the whole space supported in the neighborhood.
- The reader admits the proposition that any tangent vector at any point on any \(C^\infty\) manifold with boundary is the velocity of a \(C^\infty\) curve, especially from a half closed interval, especially as linear in coordinates.
- The reader admits the proposition that any bijective linear map is a 'vectors spaces - linear morphisms' isomorphism.
Target Context
- The reader will have a description and a proof of the proposition that for any \(C^\infty\) manifold with boundary and any regular domain, the differential of the inclusion at each point on the regular domain 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: Structured Description
Here is the rules of Structured Description.
Entities:
\(M'\): \(\in \{ \text{ the } d \text{ -dimensional } C^\infty \text{ manifolds with boundary } \}\)
\(M\): \(\in \{\text{ the regular domains of } M'\}\)
\(\iota:\): \(: M \to M'\), \(= \text{ the inclusion }\)
\(m\): \(\in M\)
\(d \iota_m\): \(: T_mM \to T_mM'\), \(= \text{ the differential }\)
//
Statements:
\(d \iota_m \in \{\text{ the 'vectors spaces - linear morphisms' isomorphisms }\}\)
//
2: Natural Language Description
For any \(d\)-dimensional \(C^\infty\) manifold with boundary, \(M'\), any regular domain, \(M\), the inclusion, \(\iota: M \to M'\), any \(m \in M\), and the differential, \(d \iota_m: T_mM \to T_mM'\), \(d \iota_m\) is a 'vectors spaces - linear morphisms' isomorphism.
3: Proof
Whole Strategy: Step 1: see that \(d \iota_m\) is injective, by seeing that \(d \iota_m (v_1) = d \iota_m (v_2)\) implies that \(v_1 = v_2\); Step 2: see that \(d \iota_m\) is surjective, by seeing that for each \(v' \in T_mM'\), \(v \in T_mM\) as that \(v f = v' \tilde{f}\) is mapped to \(v'\), where \(\tilde{f}\) is any extension of \(f\) on \(M'\); Step 3: conclude the proposition.
Step 1:
Let us see that \(d \iota_m\) is injective.
Let \(v_1, v_2 \in T_mM\) be any such that \(v_1 \neq v_2\).
Let us suppose that \(d \iota_m (v_1) = d \iota_m (v_2)\).
\(d \iota_m (v_1 - v_2) = 0\). Let \(f \in C^\infty (M)\) be any. As \(M\) was closed on \(M'\) by the proposition that for any \(C^\infty\) manifold with boundary, any embedded submanifold of the manifold is properly embedded if and only if it is closed, there would be a \(C^\infty\) extension of \(f\) on \(M'\), \(\tilde{f} \in C^\infty (M')\), such that \(f = \tilde{f} \vert_M\), by the proposition that for any \(C^\infty\) manifold with boundary, any closed subset, and any open neighborhood of the subset, any \(C^\infty\) map from the subset into \(\mathbb{R}^n\) can be extended to the whole space supported in the neighborhood. \((v_1 - v_2) f = (v_1 - v_2) \tilde{f} \vert_M = (v_1 - v_2) \tilde{f} \circ \iota = d \iota_m (v_1 - v_2) \tilde{f} = 0\), which would imply that \(v_1 - v_2 = 0\), so, \(v_1 = v_2\), a contradiction.
So, \(d \iota_m (v_1) \neq d \iota_m (v_2)\).
Step 2:
Let us see that \(d \iota_m\) is surjective.
Let \(v' \in T_mM'\) be any.
Let us define \(v \in T_mM\) as that for each \(f \in C^\infty (M)\), \(v f = v' \tilde{f}\), where \(\tilde{f} \in C^\infty (M')\) is any extension of \(f\).
Let us see that \(v\) is well-defined. An \(\tilde{f}\) exists as before. As \(M\) is an embedded submanifold with boundary of \(M'\), let us take an adopted chart, \((U'_m \subseteq M', \phi'_m)\). \(v' = v'^j \partial / \partial x'^j\) is the velocity of a \(C^\infty\) curve, \(\gamma: J \to M', t \mapsto {\phi'_m}^{-1} ((\phi'_m (m)^1 + v'^1 (t - t_0), ..., \phi'_m (m)^d + v'^d (t - t_0)))\), where \(J = [t_0, t_2) \text{ or } (t_1, t_0]\) according to \(0 \le v'^d\) or \(v'^d \lt 0\), by the proposition that any tangent vector at any point on any \(C^\infty\) manifold with boundary is the velocity of a \(C^\infty\) curve, especially from a half closed interval, especially as linear in coordinates. As \(0 \le v'^d (t - t_0)\), which means that \(\gamma\) is into \(M\), \(v' \tilde{f} = d \gamma (d / d t \vert_{t_0}) \tilde{f} = d / d t \vert_{t_0} (\tilde{f} \circ \gamma)\), which is the one-sided derivative, \(= d / d t \vert_{t_0} (\tilde{f} \vert_M \circ \gamma)= d / d t \vert_{t_0} (f \circ \gamma)\), which does not depend on the choice of \(\tilde{f}\).
Let us see that \(v\) is indeed a derivation.
\(v (r f) = v' \widetilde{r f} = v' (r \tilde{f}) = r v' \tilde{f} = r v f\). \(v (f_1 f_2) = v' (\widetilde{f_1 f_2}) = v' (\widetilde{f_1} \widetilde{f_2}) = (v' \widetilde{f_1}) \widetilde{f_2} (m) + \widetilde{f_1} (m) v' \widetilde{f_2} = (v f_1) f_2 (m) + f_1 (m) v f_2\).
So, \(v\) is indeed a derivation.
Let us see that \(d \iota_m v = v'\).
For each \(f' \in C^\infty (M')\), \(d \iota_m v (f') = v (f' \circ \iota) = v' \widetilde{f' \circ \iota}\), but \(f'\) is a \(C^\infty\) extension of \(f' \circ \iota\), so, \(= v' f'\).
So, \(d \iota_m v = v'\).
Step 3:
\(d \iota_m\) is a 'vectors spaces - linear morphisms' isomorphism, by the proposition that any bijective linear map is a 'vectors spaces - linear morphisms' isomorphism.
