description/proof of that for finite-product \(C^\infty\) manifold with boundary and point, there is 'vectors spaces - linear morphisms' isomorphism from tangent space at point onto direct sum of tangent spaces of constituent manifolds with boundary at corresponding points as para-product of differentials of projections
Topics
About: \(C^\infty\) manifold
The table of contents of this article
Starting Context
- The reader knows a definition of finite-product \(C^\infty\) manifold with boundary.
- The reader knows a definition of tangent vectors space at point on \(C^\infty\) manifold with boundary.
- The reader knows a definition of direct sum of modules.
- The reader knows a definition of %category name% isomorphism.
- The reader knows a definition of differential of \(C^\infty\) map between \(C^\infty\) manifolds with boundary at point.
- The reader admits the proposition that for any finite-product \(C^\infty\) manifold with boundary, each projection is \(C^\infty\).
- The reader admits the proposition that for any \(C^\infty\) map between any \(C^\infty\) manifolds with boundary and any corresponding charts, the components function of the differential of the map with respect to the standard bases is this.
- The reader admits the proposition that any bijective linear map between any vectors spaces is a 'vectors spaces - linear morphisms' isomorphism.
Target Context
- The reader will have a description and a proof of the proposition that for any finite-product \(C^\infty\) manifold with boundary and any point, there is the 'vectors spaces - linear morphisms' isomorphism from the tangent vectors space at the point onto the direct sum of the tangent vectors spaces of the constituent manifolds with boundary at the corresponding points as the para-product of the differentials of the projections.
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, ..., M_{n - 1}\}\): \(\subseteq \{\text{ the } C^\infty \text{ manifolds }\}\)
\(M_n\): \(\in \{\text{ the } C^\infty \text{ manifolds with boundary }\}\)
\(M\): \(= M_1 \times ... \times M_n\), \(= \text{ the product } C^\infty \text{ manifold with boundary }\)
\(m\): \(\in M\), \(= (m^1, ..., m^n)\)
\(T_mM\): \(= \text{ the tangent vectors space of } M \text{ at } m\)
\(\{T_{m^1}M_1, ..., T_{m^n}M_n\}\): \(T_{m^j}M_j = \text{ the tangent vectors space of } M_j \text{ at } m^j\)
\(\{\pi_1, ..., \pi_n\}\): \(\pi_j: M \to M_j, (m^1, ..., m^n) \mapsto m^j\)
\(f\): \(: T_mM \to T_{m^1}M_1 \oplus ... \oplus T_{m^n}M_n, v \mapsto (d \pi_1 (v), ..., d \pi_n (v))\)
//
Statements:
\(f \in \{\text{ the 'vectors spaces - linear morphisms' isomorphisms }\}\)
//
2: Note
We say "para-product", because \(f\) is not really product map.
3: Proof
Whole Strategy: Step 1: see that \(f\) is well-defined; Step 2: see that \(f\) is linear; Step 3: see that \(f\) is bijective, by taking the components expression of \(f\); Step 4: conclude the proposition.
Step 1:
Let us see that \(f\) is well-defined.
Each \(\pi_j\) is \(C^\infty\), by the proposition that for any finite-product \(C^\infty\) manifold with boundary, each projection is \(C^\infty\).
So, each \(d \pi_j\) is well-defined.
So, \(f\) is well-defined.
Step 2:
Let us see that \(f\) is linear.
Let \(v_1, v_2 \in T_mM\) and \(r_1, r_2 \in \mathbb{R}\) be any.
\(f (r_1 v_1 + r_2 v_2) = (d \pi_1 (r_1 v_1 + r_2 v_2), ..., d \pi_n (r_1 v_1 + r_2 v_2)) = (r_1 d \pi_1 (v_1) + r_2 d \pi_1 (v_2), ..., r_1 d \pi_n (v_1) + r_2 d \pi_n (v_2)) = (r_1 d \pi_1 (v_1), ..., r_1 d \pi_n (v_1)) + (r_2 d \pi_1 (v_2), ..., r_2 d \pi_n (v_2)) = r_1 (d \pi_1 (v_1), ..., d \pi_n (v_1)) + r_2 (d \pi_1 (v_2), ..., d \pi_n (v_2)) = r_1 f (v_1) + r_2 f (v_2)\).
So, \(f\) is linear.
Step 3:
Let us see that \(f\) is bijective.
Let us take any chart around \(m^j\), \((U_{m^j} \subseteq M_j, \phi_{m^j})\), such that \(\phi_{m^j}: U_{m^j} \to \mathbb{R}^{d_j}, m^j \mapsto (x^{j, 1}, ..., x^{j, d_j})\).
Let us take the chart around \(m\), \((U_m = U_{m^1} \times ... \times U_{m^n} \subseteq M, \phi_m = \phi_{m^1} \times ... \times \phi_{m^n})\).
Let \(v, v' \in T_mM\) be any such that \(v \neq v'\).
\(v = \sum_{j \in \{1, ..., n\}} v^{j, l_j} \partial / \partial x^{j, l_j}\) with respect to the standard basis for \(T_mM\) with respect to the chart.
\(v' = \sum_{j \in \{1, ..., n\}} v'^{j, l_j} \partial / \partial x^{j, l_j}\), likewise.
\(d \pi_j (v) = v^{j, l_j} \partial / \partial x^{j, l_j}\), by the proposition that for any \(C^\infty\) map between any \(C^\infty\) manifolds with boundary and any corresponding charts, the components function of the differential of the map with respect to the standard bases is this: the components function of \(\pi_j\) is \(: (x^{1, 1}, ..., x^{1, d_1}, ..., x^{j, 1}, ..., x^{j, d_j}, ... , x^{n, 1}, ..., x^{n, d_n}) \mapsto (x^{j, 1}, ..., x^{j, d_j})\).
\(d \pi_j (v') = v'^{j, l_j} \partial / \partial x^{j, l_j}\), likewise.
As \(v \neq v'\), \(v^{j, l_j} \neq v'^{j, l_j}\) for a \((j, l_j)\).
So, \(d \pi_j (v) = v^{j, l_j} \partial / \partial x^{j, l_j} \neq v'^{j, l_j} \partial / \partial x^{j, l_j} = d \pi_j (v')\).
So, \(f (v) \neq f (v')\).
So, \(f\) is injective.
Let \((v^1, ..., v^n) \in T_{m^1}M_1 \oplus ... \oplus T_{m^n}M_n\) be any.
\(v^j = v^{j, l_j} \partial / \partial x^{j, l_j}\).
There is \(v := \sum_{j \in \{1, ..., n\}} v^{j, l_j} \partial / \partial x^{j, l_j} \in T_mM\).
Then, \(f (v) = (d \pi_1 (v), ..., d \pi_n (v)) = (v^{1, l_1} \partial / \partial x^{1, l_1}, ..., v^{n, l_n} \partial / \partial x^{n, l_n}) = (v^1, ..., v^n)\).
So, \(f\) is surjective.
Step 4:
So, \(f\) is a 'vectors spaces - linear morphisms' isomorphism, by the proposition that any bijective linear map between any vectors spaces is a 'vectors spaces - linear morphisms' isomorphism.
