A description/proof of that regular submanifold of regular submanifold is regular submanifold of base \(C^\infty\) manifold of specific codimension
Topics
About: \(C^\infty\) manifold
The table of contents of this article
Starting Context
- The reader knows a definition of \(C^\infty\) manifold.
- The reader knows a definition of regular submanifold.
- The reader admits the proposition that any chart on any regular submanifold of any \(C^\infty\) manifold is an extension of an adapting chart.
Target Context
- The reader will have a description and a proof of the proposition that any regular submanifold of any regular submanifold of any \(C^\infty\) manifold is a regular submanifold of the base manifold, of codimension of the codimension of the child submanifold plus the codimension of the grandchild submanifold with respect to the child submanifold.
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\) manifold, \(M\), of dimension \(n\), any regular submanifold of \(M\), \(M_1 \subseteq M\), of dimension \(n_1\), and any regular submanifold of \(M_1\), \(M_2 \subseteq M_1\), of dimension \(n_2\), \(M_2\) is a regular submanifold of \(M\) of codimension of \((n - n_1) + (n_1 - n_2) = n - n_2\).
2: Proof
As \(M_2\) is a regular submanifold of \(M_1\), around any point, \(p \in M_2\), there is an adopted chart on \(M_1\), \((U'_p, \phi')\), where \(U'_p \subseteq M_1\) and \((U'_p \cap M_2, \phi'|_{U'_p \cap M_2})\) is the adopting chart on \(M_2\).
By the proposition that any chart on any regular submanifold of any \(C^\infty\) manifold is an extension of an adapting chart, \((U'_p, \phi')\) is an extension of an adapting char, \((U''_p \cap M_1, \phi''|_{U''_p \cap M_1})\) where \(U''_p \subseteq M\).
\(\phi''(U''_p)\) with the \(n_1 + 1\) ~ \(n\) components vanished equals \(\phi'' (U''_p \cap M_1)\), but as \((U''_p \cap M_1, \phi''|_{U''_p \cap M_1})\) is a restriction of \((U'_p, \phi')\), \(\phi'' (U''_p \cap M_1 \cap M_2)\) equals \(\phi'' (U''_p \cap M_1)\) with the \(n_2 + 1\) ~ \(n_1\) coordinates vanished, but as \(\phi'' (U''_p \cap M_1)\) equals \(\phi''(U''_p)\) with the \(n_1 + 1\) ~ \(n\) components vanished, \(\phi'' (U''_p \cap M_1 \cap M_2)\) equals \(\phi'' (U''_p)\) with the \(n_2 + 1\) ~ \(n_1, n_1 + 1\) ~ \(n\) components vanished, because any \(p' \in \phi'' (U''_p)\) whose one of the \(n_2 + 1\) ~ \(n\) components is not 0 is not on \(\phi'' (U''_p \cap M_1 \cap M_2)\) and any \(p' \in \phi'' (U''_p)\) whose all the \(n_2 + 1\) ~ \(n\) components are 0 is on \(\phi'' (U''_p \cap M_1 \cap M_2)\).
As around any \(p \in M_2\), there is an adopting chart, \((U''_p \cap M_2, \phi''|_{U''_p \cap M_2})\), where \((U''_p, \phi'')\) is the adopted chart on \(M\), \(M_2\) is a regular submanifold of \(M\) whose codimension is \(n - n_2 = (n - n_1) + (n_1 - n_2)\).
