description/proof of that for \(C^\infty\) map between \(C^\infty\) manifolds with boundary, restriction of map on embedded submanifold with boundary domain and embedded submanifold with boundary codomain is \(C^\infty\)
Topics
About: \(C^\infty\) manifold
The table of contents of this article
Starting Context
- The reader knows a definition of \(C^k\) map between arbitrary subsets of \(C^\infty\) manifolds with boundary, where \(k\) includes \(\infty\).
- The reader knows a definition of embedded submanifold with boundary of \(C^\infty\) manifold with boundary.
- The reader admits the proposition that for any maps between any arbitrary subsets of any \(C^\infty\) manifolds with boundary \(C^k\) at corresponding points, where \(k\) includes \(\infty\), the composition is \(C^k\) at the point.
- The reader admits the proposition that for any map between any arbitrary subsets of any \(C^\infty\) manifolds with boundary \(C^k\) at any point, where \(k\) includes \(\infty\), the restriction or expansion on any codomain that contains the range is \(C^k\) at the point.
- The reader admits the proposition that for any \(C^\infty\) manifold with boundary and any embedded submanifold with boundary, the inverse of the codomain restricted inclusion is \(C^\infty\).
Target Context
- The reader will have a description and a proof of the proposition that for any \(C^\infty\) map between any \(C^\infty\) manifolds with boundary, the restriction of the map on any embedded submanifold with boundary domain and any embedded submanifold with boundary codomain is \(C^\infty\).
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\): \(\in \{\text{ the } C^\infty \text{ manifolds with boundary }\}\)
\(M'_2\): \(\in \{\text{ the } C^\infty \text{ manifolds with boundary }\}\)
\(M_1\): \(\in \{\text{ the embedded submanifolds with boundary of } M'_1\}\)
\(M_2\): \(\in \{\text{ the embedded submanifolds with boundary of } M'_2\}\)
\(\iota_1\): \(: M_1 \to M'_1\), \(= \text{ the inclusion }\)
\(\iota_2\): \(: M_2 \to M'_2\), \(= \text{ the inclusion }\)
\(f'\): \(: M'_1 \to M'_2\), \(\in \{\text{ the } C^\infty \text{ maps }\}\), such that \(f' (\iota_1 (M_1)) \subseteq \iota_2 (M_2)\)
\(f\): \( = f' \vert_{M_1}: M_1 \to M_2\)
//
Statements:
\(f \in \{\text{ the } C^\infty \text{ maps }\}\)
//
2: Proof
Whole Strategy: Step 1: see that \(f'' := f' \circ \iota_1: M_1 \to M'_2\) is \(C^\infty\); Step 2: take the codomain restriction of \(f''\), \(f''': M_1 \to f'' (M_1) \subseteq M'_2\), the codomain restriction of \(\iota_2\), \({\iota_2}': M_2 \to \iota_2 (M_2) \subseteq M'_2\), and its inverse, \({\iota_2}'^{-1}: \iota_2 (M_2) \to M_2\), and see that \(f = {\iota_2}'^{-1} \circ f'''\) and \(f\) is \(C^\infty\).
Step 1:
\(\iota_1\) is \(C^\infty\), by the definition of embedded submanifold with boundary of \(C^\infty\) manifold with boundary
\(f'' := f' \circ \iota_1: M_1 \to M'_2\) is \(C^\infty\), by the proposition that for any maps between any arbitrary subsets of any \(C^\infty\) manifolds with boundary \(C^k\) at corresponding points, where \(k\) includes \(\infty\), the composition is \(C^k\) at the point.
Step 2:
Let \(f''' :M_1 \to f'' (M_1) \subseteq M'_2\) be the codomain restriction of \(f''\).
\(f'''\) is \(C^\infty\), by the proposition that for any map between any arbitrary subsets of any \(C^\infty\) manifolds with boundary \(C^k\) at any point, where \(k\) includes \(\infty\), the restriction or expansion on any codomain that contains the range is \(C^k\) at the point.
Let \({\iota_2}': M_2 \to \iota_2 (M_2) \subseteq M'_2\) be the codomain restriction of \(\iota_2\).
Let its inverse be \({\iota_2}'^{-1}: \iota_2 (M_2) \to M_2\), which is valid and \(C^\infty\), by the proposition that for any \(C^\infty\) manifold with boundary and any embedded submanifold with boundary, the inverse of the codomain restricted inclusion is \(C^\infty\).
\(f'' (M_1) \subseteq \iota_2 (M_2)\), because \(f'' (M_1) = f' \circ \iota_1 (M_1) = f' (\iota_1 (M_1)) \subseteq \iota_2 (M_2)\).
So, \({\iota_2}'^{-1} \circ f''': M_1 \to M_2\) is valid, and \(= f\), because \({\iota_2}'^{-1} \circ f''' = {\iota_2}'^{-1} \circ f' \circ \iota_1\).
\({\iota_2}'^{-1} \circ f'''\) is \(C^\infty\), by the proposition that for any maps between any arbitrary subsets of any \(C^\infty\) manifolds with boundary \(C^k\) at corresponding points, where \(k\) includes \(\infty\), the composition is \(C^k\) at the point.
So, \(f\) is \(C^\infty\).
