description/proof of that for \(C^\infty\) manifold with boundary and embedded submanifold with boundary, around each point on submanifold with boundary, there is trivializing open subset for manifold with boundary whose intersection with submanifold with boundary is chart domain
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^\infty\) trivializing open subset and \(C^\infty\) local trivialization.
- The reader admits the proposition that for any \(C^\infty\) manifold with boundary and its any chart, the restriction of the chart on any open subset domain is a chart.
- The reader admits the proposition that any open subset of any \(C^\infty\) trivializing open subset is a \(C^\infty\) trivializing open subset.
Target Context
- The reader will have a description and a proof of the proposition that for any \(C^\infty\) manifold with boundary and its any embedded submanifold with boundary, around each point on the submanifold with boundary, there is a trivializing open subset for the manifold with boundary whose intersection with the submanifold with boundary is a chart domain for the submanifold with boundary.
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'\): \(\in \{\text{ the } C^\infty \text{ manifolds with boundary }\}\)
\(M\): \(\in \{\text{ the embedded submanifolds with boundary of } M'\}\)
\(m\): \(\in M\)
//
Statements:
\(\exists U'_m \in \{\text{ the trivializing open subsets of } M' \text{ around } m\} (U'_m \cap M \in \{\text{ the chart domains for } M\})\)
//
2: Note
The point is that \(M'\) can be with a nonempty boundary: when \(M'\) is without boundary, the slice charts theorem can be used to have \(U'_m\) as an adopted chart domain; this proposition says that even when \(M'\) has a nonempty boundary, a \(U'_m\), which is not necessarily any chart domain, can be chosen.
3: Proof
Whole Strategy: Step 1: take any trivializing open subset around \(m\) for \(M'\), \(V'_m\); Step 2: take any open neighborhood of \(m\) on \(M\), \(V_m\), whose inclusion is contained in \(V'_m\), and take any chart domain contained in \(V_m\), \(W_m\); Step 3: let \(W_m = W'_m \cap M\), take \(U'_m := V'_m \cap W'_m\) and \(U_m := U'_m \cap M\), and see that \(U'_m\) is a trivializing open subset for \(M'\) and \(U_m\) is a chart domain for \(M\).
Step 1:
Let us take any trivializing open subset around \(m\) for \(M'\), \(V'_m \subseteq M'\).
Step 2:
Let \(\iota: M \to M'\) be the inclusion.
As \(\iota\) is continuous, there is an open neighborhood of \(m\) on \(M\), \(V_m \subseteq M\), such that \(\iota (V_m) \subseteq V'_m\).
There is a chart domain contained in \(V_m\), \(W_m \subseteq M\), such that \(W_m \subseteq V_m\), because while there is a chart domain around \(m\), the intersection of the chart domain and \(V_m\) is a chart domain, by the proposition that for any \(C^\infty\) manifold with boundary and its any chart, the restriction of the chart on any open subset domain is a chart, and the intersection can be \(W_m\).
Step 3:
As \(M\) has the subspace topology of \(M'\), \(W_m = W'_m \cap M\) where \(W'_m \subseteq M'\) is an open neighborhood of \(m\) on \(M'\).
Let us take \(U'_m := V'_m \cap W'_m\) and \(U_m := U'_m \cap M\).
As \(U'_m\) is an open subset of \(V'_m\), \(U'_m\) is a trivializing open subset for \(M'\), by the proposition that any open subset of any \(C^\infty\) trivializing open subset is a \(C^\infty\) trivializing open subset.
As \(U_m = U'_m \cap M = V'_m \cap W'_m \cap M = V'_m \cap M \cap W'_m \cap M = V'_m \cap M \cap W_m\) is an open subset of \(W_m\) (\(W_m\) is a topological subspace of \(M\) and \(V'_m \cap M\) is open on \(M\)), \(U_m\) is a chart domain, by the proposition that for any \(C^\infty\) manifold with boundary and its any chart, the restriction of the chart on any open subset domain is a chart.
