description/proof of that for \(C^\infty\) manifold, subset, and point on subset, if chart satisfies local slice condition for embedded submanifold or local slice condition for embedded submanifold with boundary, its sub-open-neighborhood does so
Topics
About: \(C^\infty\) manifold
The table of contents of this article
- Starting Context
- Target Context
- Orientation
- Main Body
- 1: Structured Description
- 2: Natural Language Description
- 3: Proof
Starting Context
Target Context
- The reader will have a description and a proof of the proposition that for any \(C^\infty\) manifold, any subset, and any point on the subset, if a chart satisfies the local slice condition for embedded submanifold or the local slice condition for embedded submanifold with boundary, its any sub-open-neighborhood does so.
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 } d' \text{ -dimensional } C^\infty \text{ manifolds } \}\)
\(S\): \(\subseteq M'\)
\(J\): \(\subseteq \{1, ..., d'\}\) such that \(\vert J \vert = d\)
\(k\): \(\in J\)
\(s\): \(\in S\)
\(\lambda_{J, r}\): \(: Pow (\mathbb{R}^{d'}) \to Pow (\mathbb{R}^{d'})\), \(= \text{ the slicing map }\), where \(r \in \mathbb{R}^{d'}\) is any
\(\lambda_{J, r, k}\): \(: Pow (\mathbb{R}^{d'}) \to Pow (\mathbb{R}^{d'})\), \(= \text{ the slicing-and-halving map }\), where \(r \in \mathbb{R}^{d'}\) is any
\(\pi_J\): \(: \mathbb{R}^{d'} \to \mathbb{R}^d\), \(= \text{ the projection }\)
\((U'_s \subseteq M', \phi'_s)\): \(\in \{\text{ the charts around } s \text{ of } M'\}\)
\(V'_s\): \(\in \{\text{ the open neighborhoods of } s \text{ on } M'\}\), such that \(V'_s \subseteq U'_s\)
//
Statements:
\((U'_s \subseteq M', \phi'_s)\) satisfies the local slice condition for embedded submanifold or the local slice condition for embedded submanifold with boundary
\(\implies\)
\((V'_s \subseteq M', \phi'_s \vert_{V'_s})\) satisfies the local slice condition for embedded submanifold or the local slice condition for embedded submanifold with boundary
//
2: Natural Language Description
For any \(d'\)-dimensional \(C^\infty\) manifold, \(M'\), any subset, \(S \subseteq M'\), any subset, \(J \subseteq \{1, ..., d'\}\), such that \(\vert J \vert = d\), any \(k \in J\), any point, \(s \in S\), the slicing map, \(\lambda_{J, r}: Pow (\mathbb{R}^{d'}) \to Pow (\mathbb{R}^{d'})\), where \(r \in \mathbb{R}^{d'}\) is any, the slicing-and-halving map, \(\lambda_{J, r, k}: Pow (\mathbb{R}^{d'}) \to Pow (\mathbb{R}^{d'})\), where \(r \in \mathbb{R}^{d'}\) is any, the projection, \(\pi_J: \mathbb{R}^{d'} \to \mathbb{R}^d\), any chart around \(s\), \((U'_s \subseteq M', \phi'_s)\), and any open neighborhood of \(s\), \(V'_s \subseteq M'\), such that \(V'_s \subseteq U'_s\), if \((U'_s \subseteq M', \phi'_s)\) satisfies the local slice condition for embedded submanifold or the local slice condition for embedded submanifold with boundary, \((V'_s \subseteq M', \phi'_s \vert_{V'_s})\) satisfies the local slice condition for embedded submanifold or the local slice condition for embedded submanifold with boundary.
3: Proof
Whole Strategy: Step 1: suppose that \((U'_s \subseteq M', \phi'_s)\) satisfies the local slice condition for embedded submanifold and get the formalization, \(\phi'_s (U'_s \cap S) = \lambda_{J, \phi'_s (s)} (\phi'_s (U'_s))\); Step 2: see that \(\phi'_s (V'_s \cap S) = \lambda_{J, \phi'_s (s)} (\phi'_s (V'_s))\) is satisfied; Step 3: suppose that \((U'_s \subseteq M', \phi'_s)\) satisfies the local slice condition for embedded submanifold with boundary and get the formalization, \(\phi'_s (U'_s \cap S) = \lambda_{J, \phi'_s (s)} (\phi'_s (U'_s)) \lor (\phi'_s (s)^k = 0 \land \phi'_s (U'_s \cap S) = \lambda_{J, \phi'_s (s), k} (\phi'_s (U'_s)))\); Step 4: see that \(\phi'_s (V'_s \cap S) = \lambda_{J, \phi'_s (s)} (\phi'_s (V'_s)) \lor (\phi'_s (s)^k = 0 \land \phi'_s (V'_s \cap S) = \lambda_{J, \phi'_s (s), k} (\phi'_s (V'_s)))\) is satisfied.
Step 1:
Let us suppose that \((U'_s \subseteq M', \phi'_s)\) satisfies the local slice condition for embedded submanifold.
By the proposition that a formalization of the local slice condition for embedded submanifold or the local slice condition for embedded submanifold with boundary is valid, \(\phi'_s (U'_s \cap S) = \lambda_{J, \phi'_s (s)} (\phi'_s (U'_s))\).
Step 2:
By the proposition that a formalization of the local slice condition for embedded submanifold or the local slice condition for embedded submanifold with boundary is valid, all what we need to see is that \(\phi'_s (V'_s \cap S) = \lambda_{J, \phi'_s (s)} (\phi'_s (V'_s))\) is satisfied.
Let \(p \in \phi'_s (V'_s \cap S)\) be any and see that \(p \in \lambda_{J, \phi'_s (s)} (\phi'_s (V'_s))\).
\(p \in \phi'_s (V'_s)\), because \(p \in \phi'_s (V'_s \cap S) \subseteq \phi'_s (V'_s)\).
\(p \in \phi'_s (V'_s \cap S) \subseteq \phi'_s (U'_s \cap S) = \lambda_{J, \phi'_s (s)} (\phi'_s (U'_s))\), which implies that for each \(j \in \{1, ..., d'\} \setminus J\), \(p^j = \phi'_s (s)^j\). But that implies that \(p \in \lambda_{J, \phi'_s (s)} (\phi'_s (V'_s))\).
Let \(p \in \lambda_{J, \phi'_s (s)} (\phi'_s (V'_s))\) be any and see that \(p \in \phi'_s (V'_s \cap S)\).
There is a \(p' \in V'_s\) such that \(p = \phi'_s (p')\).
\(p \in \lambda_{J, \phi'_s (s)} (\phi'_s (V'_s)) \subseteq \lambda_{J, \phi'_s (s)} (\phi'_s (U'_s)) = \phi'_s (U'_s \cap S)\). So, there is a \(p'' \in U'_s \cap S\) such that \(p = \phi'_s (p'')\).
As \(\phi'_s\) is injective, \(p' = p'' \in V'_s \cap U'_s \cap S = V'_s \cap S\). So, \(p = \phi'_s (p') \in \phi'_s (V'_s \cap S)\).
So, \(\phi'_s (V'_s \cap S) = \lambda_{J, \phi'_s (s)} (\phi'_s (V'_s))\).
Step 3:
Let us suppose that \((U'_s \subseteq M', \phi'_s)\) satisfies the local slice condition for embedded submanifold with boundary.
By the proposition that a formalization of the local slice condition for embedded submanifold or the local slice condition for embedded submanifold with boundary is valid, \(\phi'_s (U'_s \cap S) = \lambda_{J, \phi'_s (s)} (\phi'_s (U'_s)) \lor (\phi'_s (s)^k = 0 \land \phi'_s (U'_s \cap S) = \lambda_{J, \phi'_s (s), k} (\phi'_s (U'_s)))\).
Step 4:
By the proposition that a formalization of the local slice condition for embedded submanifold or the local slice condition for embedded submanifold with boundary is valid, all what we need to see is that \(\phi'_s (V'_s \cap S) = \lambda_{J, \phi'_s (s)} (\phi'_s (V'_s)) \lor (\phi'_s (s)^k = 0 \land \phi'_s (V'_s \cap S) = \lambda_{J, \phi'_s (s), k} (\phi'_s (V'_s)))\) is satisfied.
When \(\phi'_s (U'_s \cap S) = \lambda_{J, \phi'_s (s)} (\phi'_s (U'_s))\), \(\phi'_s (V'_s \cap S) = \lambda_{J, \phi'_s (s)} (\phi'_s (V'_s))\), as before.
Let us suppose that \(\phi'_s (s)^k = 0 \land \phi'_s (U'_s \cap S) = \lambda_{J, \phi'_s (s), k} (\phi'_s (U'_s))\) and see that \(\phi'_s (s)^k = 0 \land \phi'_s (V'_s \cap S) = \lambda_{J, \phi'_s (s), k} (\phi'_s (V'_s))\).
\(\phi'_s (s)^k = 0\), obviously.
Let \(p \in \phi'_s (V'_s \cap S)\) be any and see that \(p \in \lambda_{J, \phi'_s (s), k} (\phi'_s (V'_s))\).
\(p \in \phi'_s (V'_s)\), because \(p \in \phi'_s (V'_s \cap S) \subseteq \phi'_s (V'_s)\).
\(p \in \phi'_s (V'_s \cap S) \subseteq \phi'_s (U'_s \cap S) = \lambda_{J, \phi'_s (s), k} (\phi'_s (U'_s))\), which implies that for each \(j \in \{1, ..., d'\} \setminus J\), \(p^j = \phi'_s (s)^j\) and \(\phi'_s (s)^k \le p^k\). But that implies that \(p \in \lambda_{J, \phi'_s (s), k} (\phi'_s (V'_s))\).
Let \(p \in \lambda_{J, \phi'_s (s), k} (\phi'_s (V'_s))\) be any and see that \(p \in \phi'_s (V'_s \cap S)\).
There is a \(p' \in V'_s\) such that \(p = \phi'_s (p')\).
\(p \in \lambda_{J, \phi'_s (s), k} (\phi'_s (V'_s)) \subseteq \lambda_{J, \phi'_s (s), k} (\phi'_s (U'_s)) = \phi'_s (U'_s \cap S)\). So, there is a \(p'' \in U'_s \cap S\) such that \(p = \phi'_s (p'')\).
As \(\phi'_s\) is injective, \(p' = p'' \in V'_s \cap U'_s \cap S = V'_s \cap S\). So, \(p = \phi'_s (p') \in \phi'_s (V'_s \cap S)\).
So, \(\phi'_s (s)^k = 0 \land \phi'_s (V'_s \cap S) = \phi'_s (V'_s \cap S) = \lambda_{J, \phi'_s (s), k} (\phi'_s (V'_s))\).
