description/proof of that for map between embedded submanifolds with boundary of \(C^\infty\) manifolds with boundary, \(C^k\)-ness does not change when domain or codomain is regarded to be subset
Topics
About: \(C^\infty\) manifold
The table of contents of this article
Starting Context
- The reader knows a definition of embedded submanifold with boundary of \(C^\infty\) manifold with boundary.
- The reader knows a definition of \(C^k\) map between arbitrary subsets of \(C^\infty\) manifolds with boundary, where \(k\) includes \(\infty\).
- 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\).
- 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.
Target Context
- The reader will have a description and a proof of the proposition that for any map between any embedded submanifolds with boundary of any \(C^\infty\) manifolds with boundary, \(C^k\)-ness does not change when the domain or the codomain is regarded to be the subset.
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\}\)
\(\iota_1\): \(: M_1 \to M'_1\), \(= \text{ the inclusion }\)
\(M_2\): \(\in \{\text{ the embedded submanifolds with boundary of } M'_2\}\)
\(\iota_2\): \(: M_2 \to M'_2\), \(= \text{ the inclusion }\)
\(f_1\): \(: M_1 \to M_2\)
\(f_2\): \(: M_1 \to \iota_2 (M_2) \subseteq M'_2\), \(= f_1\) with the codomain replaced
\(f_3\): \(: \iota_1 (M_1) \subseteq M'_1 \to M_2\), \(= f_1\) with the domain replaced
\(f_4\): \(: \iota_1 (M_1) \subseteq M'_1 \to \iota_2 (M_2) \subseteq M'_2\), \(= f_1\) with the domain and the codomain replaced
//
Statements:
\(f_1 \in \{\text{ the } C^k \text{ maps }\}\)
\(\iff\)
\(f_2 \in \{\text{ the } C^k \text{ maps }\}\)
\(\iff\)
\(f_3 \in \{\text{ the } C^k \text{ maps }\}\)
\(\iff\)
\(f_4 \in \{\text{ the } C^k \text{ maps }\}\)
//
2: Note
This proposition is not so trivial: for example, \(C^k\)-ness of \(f_1\) is judged with respect to the atlas of \(M_1\) and the atlas of \(M_2\) while \(C^k\)-ness of \(f_4\) is judged with respect to the atlas of \(M'_1\) and the atlas of \(M'_2\).
This proposition requires \(M_1\) and \(M_2\) to be embedded, not more generally immersed.
3: Proof
Whole Strategy: let \(\iota'_j: M_j \to \iota_j (M_j) \subseteq M'_j\) be the codomain restriction of \(\iota_j\), and for from \(f_j\) to \(f_k\), express \(f_k\) with \(f_j\) and \(\iota'_1, \iota'_2\), and use 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\); Step 1: express \(f_2, f_3, f_4\) with \(f_1\) and \(\iota'_1, \iota'_2\), express \(f_1, f_3, f_4\) with \(f_2\) and \(\iota'_1, \iota'_2\), express \(f_1, f_2, f_4\) with \(f_3\) and \(\iota'_1, \iota'_2\), and express \(f_1, f_2, f_3\) with \(f_4\) and \(\iota'_1, \iota'_2\); Step 2: see that \({\iota'_1}^{-1}\) and \({\iota'_2}^{-1}\) are \(C^\infty\); Step 3: conclude the proposition.
Step 1:
Let \(\iota'_1: M_1 \to \iota_1 (M_1) \subseteq M'_1\) be the codomain restriction of \(\iota_1\).
\(\iota'_1\) 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\).
\(\iota'_2\) 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 us express \(f_2, f_3, f_4\) with \(f_1\) and \(\iota'_1\) and \(\iota'_2\).
\(f_2 = \iota'_2 \circ f_1\).
\(f_3 = f_1 \circ {\iota'_1}^{-1}\).
\(f_4 = \iota'_2 \circ f_1 \circ {\iota'_1}^{-1}\).
Let us express \(f_1, f_3, f_4\) with \(f_2\) and \(\iota'_1\) and \(\iota'_2\).
\(f_1 = {\iota'_2}^{-1} \circ f_2\).
\(f_3 = {\iota'_2}^{-1} \circ f_2 \circ {\iota'_1}^{-1}\).
\(f_4 = f_2 \circ {\iota'_1}^{-1}\).
Let us express \(f_1, f_2, f_4\) with \(f_3\) and \(\iota'_1\) and \(\iota'_2\).
\(f_1 = f_3 \circ \iota'_1\).
\(f_2 = \iota'_2 \circ f_3 \circ \iota'_1\).
\(f_4 = \iota'_2 \circ f_3\).
Let us express \(f_1, f_2, f_3\) with \(f_4\) and \(\iota'_1\) and \(\iota'_2\).
\(f_1 = {\iota'_2}^{-1} f_4 \circ \iota'_1\).
\(f_2 = f_4 \circ \iota'_1\).
\(f_3 = {\iota'_2}^{-1} \circ f_4\).
Step 2:
\({\iota'_1}^{-1}\) and \({\iota'_2}^{-1}\) are \(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\).
Step 3:
Let us suppose \(f_1\) is \(C^k\).
\(f_2, f_3, f_4\) are \(C^k\), 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.
Let us suppose \(f_2\) is \(C^k\).
\(f_1, f_3, f_4\) are \(C^k\), likewise.
Let us suppose \(f_3\) is \(C^k\).
\(f_1, f_2, f_4\) are \(C^k\), likewise.
Let us suppose \(f_4\) is \(C^k\).
\(f_1, f_2, f_3\) are \(C^k\), likewise.
