description/proof of that for \(C^\infty\) manifold with boundary and open submanifold with boundary, differential of inclusion at point on open submanifold with boundary 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 open submanifold with boundary 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\) function on any point open neighborhood of any \(C^\infty\) manifold with boundary, there exists a \(C^\infty\) function on the whole manifold with boundary that equals the original function on a possibly smaller neighborhood of the point.
- 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 \(C^\infty\) manifold with boundary and any open submanifold with boundary, the differential of the inclusion at each point on the open submanifold with boundary 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 open submanifolds with boundary 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: 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 for each \(f \in C^\infty (M)\), \(v f = v' \overline{f}\) is mapped to \(v'\), where \(\overline{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.
\(f\) would be \(C^\infty\) also as a function with \(M\) regarded as the subset of \(M'\) (instead of as the submanifold): each chart of \(M\) is also a chart of \(M'\).
By the proposition that for any \(C^\infty\) function on any point open neighborhood of any \(C^\infty\) manifold with boundary, there exists a \(C^\infty\) function on the whole manifold with boundary that equals the original function on a possibly smaller neighborhood of the point, there would be an open neighborhood of \(m\), \(U_m \subseteq M'\), such that \(U_m \subseteq \iota (M)\), and a \(C^\infty\) function, \(\overline{f}: M' \to \mathbb{R}\), such that \(f \vert_{U_m} = \overline{f} \vert_{U_m}\).
\(v_1 (\overline{f} \circ \iota) = d \iota_m (v_1) \overline{f} = d \iota_m (v_2) \overline{f} = v_2 (\overline{f} \circ \iota)\).
But \(\overline{f} \circ \iota \vert_{U_m} = f \vert_{U_m}\).
So, \(v_j (\overline{f} \circ \iota) = v_j f\), because any tangent vector is a local operator.
So, \(v_1 f = v_1 (\overline{f} \circ \iota) = v_2 (\overline{f} \circ \iota) = v_2 f\), 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' \overline{f}\), where \(\overline{f} \in C^\infty (M')\) is gotten from \(f\) as above.
Let us see that \(v\) is well-defined. An \(\overline{f}\) exists as before. \(v' \overline{f}\) does not depend on the choice of \(\overline{f}\), because \(v'\) is a local operator.
Let us see that \(v\) is indeed a derivation.
\(v (r f) = v' \overline{r f} = v' (r \overline{f}) = r v' \overline{f} = r v f\). \(v (f_1 f_2) = v' (\overline{f_1 f_2}) = v' (\overline{f_1} \text{ } \overline{f_2}) = (v' \overline{f_1}) \overline{f_2} (m) + \overline{f_1} (m) v' \overline{f_2} = (v f_1) f_2 (m) + f_1 (m) v f_2\): although \(\overline{f_1}\) and \(\overline{f_2}\) may have some different open neighborhoods of \(m\), the intersection of the open neighborhoods is an open neighborhood of \(m\) on which \(\overline{f_1} \text{ } \overline{f_2}\) equals \(f_1 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' \overline{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 morphism is a 'vectors spaces - linear morphisms' isomorphism.
