A description/proof of that restriction of \(C^\infty\) vectors bundle on regular submanifold base space is \(C^\infty\) vectors bundle
Topics
About: \(C^\infty\) manifold
The table of contents of this article
Starting Context
- The reader knows a definition of restriction of \(C^\infty\) vectors bundle on regular submanifold base space.
- The reader admits the proposition that for any transversal map from any \(C^\infty\) manifold to any regular submanifold, the preimage of the regular submanifold under the transversal map is a regular submanifold of the domain.
- The reader admits the proposition that for any \(C^\infty\) map between \(C^\infty\) manifolds, the restriction of the map on any regular submanifold domain and any regular submanifold codomain is \(C^\infty\).
- The reader admits the proposition that for any \(C^\infty\) manifold and its any regular submanifold, any open subset of the super manifold is canonically a \(C^\infty\) manifold, and the intersection of the open subset and the regular submanifold is a regular submanifold of the open subset manifold.
- The reader admits the proposition that for any map, the map preimage of any intersection of sets is the intersection of the map preimages of the sets.
- The reader admits the proposition that the intersection of the same-indices-set products of possibly uncountable number of sets is the product of the intersections of the subsets.
- The reader admits the proposition that for the product of any 2 \(C^\infty\) manifolds, the product for which one of the constituents is replaced with any regular submanifold is a regular submanifold of the original product.
Target Context
- The reader will have a description and a proof of the proposition that for any \(C^\infty\) vectors bundle, the restriction of the vectors bundle on any regular submanifold base space is a \(C^\infty\) vectors bundle.
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\) vectors bundle, \(\pi: M_1 \rightarrow M_2\), and any regular submanifold, \(M_3 \subseteq M_2\), the restriction of \(\pi\) on \(M_3\), \(\pi_{M_3}: \pi^{-1} (M_3) \rightarrow M_3\), is a \(C^\infty\) vectors bundle.
2: Proof
\(\pi\) is a submersion, \(\pi\) is a transversal map to \(M_3\), and \(\pi^{-1} (M_3)\) is a regular submanifold of \(M_1\) as a preimage of a regular submanifold under a transversal map, by the proposition that for any transversal map from any \(C^\infty\) manifold to any regular submanifold, the preimage of the regular submanifold under the transversal map is a regular submanifold of the domain.
\(\pi_{M_3}\) is \(C^\infty\) as a restriction of a \(C^\infty\) map on a regular submanifold domain and a regular submanifold codomain, by the proposition that for any \(C^\infty\) map between \(C^\infty\) manifolds, the restriction of the map on any regular submanifold domain and any regular submanifold codomain is \(C^\infty\). \(\pi_{M_3}\) is obviously surjective.
For any \(p \in M_3\), \({\pi_{M_3}}^{-1} (p)\) is a real vectors space, because \({\pi_{M_3}}^{-1} (p) = \pi^{-1} (p)\).
For any \(p \in M_3\), there is an open neighborhood, \(U_p \subseteq M_2\), such that there is a fiber-preserving diffeomorphism, \(f': \pi^{-1} (U_p) \rightarrow U_p \times \mathbb{R}^r\). There is the fiber-preserving bijection, \(f = f'\vert_{\pi^{-1} (U_p \cap M_3)}: \pi^{-1} (U_p \cap M_3) \rightarrow (U_p \cap M_3) \times \mathbb{R}^r\), because \(f'\) is fiber-preserving.
Is \(f\) diffeomorphic? \(\pi^{-1} (U_p)\) is an open subset of \(M_1\), because \(\pi\) is continuous, and is a \(C^\infty\) manifold, by the proposition that for any \(C^\infty\) manifold and its any regular submanifold, any open subset of the super manifold is canonically a \(C^\infty\) manifold, and the intersection of the open subset and the regular submanifold is a regular submanifold of the open subset manifold. \(U_p \times \mathbb{R}^r\) is an open subset of \(M_2 \times \mathbb{R}^r\), and is a \(C^\infty\) manifold likewise.
\(\pi^{-1} (U_p \cap M_3) = \pi^{-1} (U_p) \cap \pi^{-1} (M_3)\), by the proposition that for any map, the map preimage of any intersection of sets is the intersection of the map preimages of the sets. So, \(\pi^{-1} (U_p \cap M_3)\) is a regular submanifold of \(\pi^{-1} (U_p)\), by the proposition that for any \(C^\infty\) manifold and its any regular submanifold, any open subset of the super manifold is canonically a \(C^\infty\) manifold, and the intersection of the open subset and the regular submanifold is a regular submanifold of the open subset manifold. \((U_p \cap M_3) \times \mathbb{R}^r = (U_p \times \mathbb{R}^r) \cap (M_3 \times \mathbb{R}^r)\), by the proposition that the intersection of the same-indices-set products of possibly uncountable number of sets is the product of the intersections of the subsets, and \(M_3 \times \mathbb{R}^r\) is a regular submanifold of \(M_2 \times \mathbb{R}^r\), by the proposition that for the product of any 2 \(C^\infty\) manifolds, the product for which one of the constituents is replaced with any regular submanifold is a regular submanifold of the original product, and \((U_p \cap M_3) \times \mathbb{R}^r\) is a regular submanifold of \(U_p \times \mathbb{R}^r\) likewise.
So, \(f = f'\vert_{\pi^{-1} (U_p \cap M_3)}: \pi^{-1} (U_p \cap M_3) \rightarrow (U_p \cap M_3) \times \mathbb{R}^r\) is a restriction of the \(C^\infty\) \(f'\) on a regular submanifold domain and a regular submanifold codomain, and is \(C^\infty\), by the proposition that for any \(C^\infty\) map between \(C^\infty\) manifolds, the restriction of the map on any regular submanifold domain and any regular submanifold codomain is \(C^\infty\). As \(f\) is a bijection, there is the inverse, \(f^{-1}\), which is a restriction of the \(C^\infty\) \(f'^{-1}\) on a regular submanifold domain and a regular submanifold codomain, and is \(C^\infty\), likewise.
For any point, \(p' \in U_p \cap M_3\), \(f \vert_{{\pi}^{-1} (p')}: {\pi}^{-1} (p') \to \{p'\} \times \mathbb{R}^r\) is a 'vectors spaces - linear morphisms' isomorphism, because it is the same with \(f' \vert_{{\pi}^{-1} (p')}\).
