774: Formalization of Local Slice Condition for Embedded Submanifold or Local Slice Condition for Embedded Submanifold with Boundary

<The previous article in this series | The table of contents of this series | The next article in this series>

description/proof of formalization of local slice condition for embedded submanifold or local slice condition for embedded submanifold with boundary

---

Topics

About: $C^{\mathrm{\infty }}$ manifold

---

The table of contents of this article

• Starting Context
• Target Context
• Orientation
• Main Body
• 1: Structured Description
• 2: Natural Language Description
• 3: Note
• 4: Proof

---

Starting Context

• The reader knows a definition of embedded submanifold with boundary of $C^{\mathrm{\infty }}$ manifold with boundary.
• The reader knows a definition of slicing map on Euclidean set.
• The reader knows a definition of slicing-and-halving map on Euclidean set.
• The reader knows a definition of projection between Euclidean sets.

---

Target Context

• The reader will have a description and a proof of 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.

---

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^{\prime }$: $\in \{\text{ the }{d}^{\prime }\text{ -dimensional }{C}^{\mathrm{\infty }}\text{ manifolds }\}$
$S$: $\subseteq M^{\prime }$
$J$: $\subseteq \{1,...,d^{\prime }\}$ such that $|J|=d$
$k$: $\in J$
$s$: $\in S$
${\lambda }_{J,r^{\prime }}$: $:Pow({\mathbb{R}}^{d^{\prime }})\to Pow({\mathbb{R}}^{d^{\prime }})$, $=\text{ the slicing map }$, where $r^{\prime }\in {\mathbb{R}}^{d^{\prime }}$ is any
${\lambda }_{J,r^{\prime },k}$: $:Pow({\mathbb{R}}^{d^{\prime }})\to Pow({\mathbb{R}}^{d^{\prime }})$, $=\text{ the slicing-and-halving map }$, where $r^{\prime }\in {\mathbb{R}}^{d^{\prime }}$ is any
${\pi }_J$: $:{\mathbb{R}}^{d^{\prime }}\to {\mathbb{R}}^d$, $=\text{ the projection }$
//

Statements:
(
$S$ satisfies the local slice condition for embedded submanifold at $s$
$⟺$
$\mathrm{\exists }(U_s^{\prime }\subseteq M^{\prime },{\varphi }_s^{\prime })\in \{\text{ the charts around }s\text{ of }{M}^{\prime }\}({\varphi }_s^{\prime }(U_s^{\prime }\cap S)={\lambda }_{J,{\varphi }_s^{\prime }(s)}({\varphi }_s^{\prime }(U_s^{\prime })))$
$⟹$
(
$(U_s=U_s^{\prime }\cap S,{\varphi }_s={\pi }_J\circ {\varphi }_s^{\prime }{|}_{U_s})$ is the corresponding adopting chart
$\wedge$
${\varphi }_s(U_s)={\pi }_J\circ {\varphi }_s^{\prime }(U_s)={\pi }_J\circ {\lambda }_{J,{\varphi }_s^{\prime }(s)}({\varphi }_s^{\prime }(U_s^{\prime }))$
)
)
$\wedge$
(
$S$ satisfies the local slice condition for embedded submanifold with boundary at $s$
$⟺$
$\mathrm{\exists }(U_s^{\prime }\subseteq M^{\prime },{\varphi }_s^{\prime })\in \{\text{ the charts around }s\text{ of }{M}^{\prime }\}({\varphi }_s^{\prime }(U_s^{\prime }\cap S)={\lambda }_{J,{\varphi }_s^{\prime }(s)}({\varphi }_s^{\prime }(U_s^{\prime }))\vee ({\varphi }_s^{\prime }(s{)}^k=0\wedge {\varphi }_s^{\prime }(U_s^{\prime }\cap S)={\lambda }_{J,{\varphi }_s^{\prime }(s),k}({\varphi }_s^{\prime }(U_s^{\prime }))))$
$⟹$
(
$(U_s=U_s^{\prime }\cap S,{\varphi }_s={\pi }_J\circ {\varphi }_s^{\prime }{|}_{U_s})$ is the corresponding adopting chart
$\wedge$
${\varphi }_s(U_s)={\pi }_J\circ {\varphi }_s^{\prime }(U_s)={\pi }_J\circ {\lambda }_{J,{\varphi }_s^{\prime }(s)}({\varphi }_s^{\prime }(U_s^{\prime }))\text{ or }{\pi }_J\circ {\lambda }_{J,{\varphi }_s^{\prime }(s),k}({\varphi }_s^{\prime }(U_s^{\prime }))$
)
)
//

---

2: Natural Language Description

For any $d^{\prime }$-dimensional $C^{\mathrm{\infty }}$ manifold, $M^{\prime }$, any subset, $S\subseteq M^{\prime }$, any subset, $J\subseteq \{1,...,d^{\prime }\}$, such that $|J|=d$, any $k\in J$, any point, $s\in S$, the slicing map, ${\lambda }_{J,r^{\prime }}:Pow({\mathbb{R}}^{d^{\prime }})\to Pow({\mathbb{R}}^{d^{\prime }})$, where $r^{\prime }\in {\mathbb{R}}^{d^{\prime }}$ is any, the slicing-and-halving map, ${\lambda }_{J,r^{\prime },k}:Pow({\mathbb{R}}^{d^{\prime }})\to Pow({\mathbb{R}}^{d^{\prime }})$, where $r^{\prime }\in {\mathbb{R}}^{d^{\prime }}$ is any, and the projection, ${\pi }_J:{\mathbb{R}}^{d^{\prime }}\to {\mathbb{R}}^d$, $S$ satisfies the local slice condition for embedded submanifold at $s$ if and only if there is a chart around $s$, $(U_s^{\prime }\subseteq M^{\prime },{\varphi }_s^{\prime })$, such that ${\varphi }_s^{\prime }(U_s^{\prime }\cap S)={\lambda }_{J,{\varphi }_s^{\prime }(s)}({\varphi }_s^{\prime }(U_s^{\prime }))$, and if so, the corresponding adopting chart is $(U_s=U_s^{\prime }\cap S,{\varphi }_s={\pi }_J\circ {\varphi }_s^{\prime }{|}_{U_s})$ and ${\varphi }_s(U_s)={\pi }_J\circ {\varphi }_s^{\prime }(U_s)={\pi }_J\circ {\lambda }_{J,{\varphi }_s^{\prime }(s)}({\varphi }_s^{\prime }(U_s^{\prime }))$; $S$ satisfies the local slice condition for embedded submanifold with boundary at $s$ if and only if there is a chart around $s$, $(U_s^{\prime }\subseteq M^{\prime },{\varphi }_s^{\prime })$, such that ${\varphi }_s^{\prime }(U_s^{\prime }\cap S)={\lambda }_{J,{\varphi }_s^{\prime }(s)}({\varphi }_s^{\prime }(U_s^{\prime }))$ or ${\varphi }_s^{\prime }(s{)}^k=0\wedge {\varphi }_s^{\prime }(U_s^{\prime }\cap S)={\lambda }_{J,{\varphi }_s^{\prime }(s),k}({\varphi }_s^{\prime }(U_s^{\prime }))$, and if so, the corresponding adopting chart is $(U_s=U_s^{\prime }\cap S,{\varphi }_s={\pi }_J\circ {\varphi }_s^{\prime }{|}_{U_s})$ and ${\varphi }_s(U_s)={\pi }_J\circ {\varphi }_s^{\prime }(U_s)={\pi }_J\circ {\lambda }_{J,{\varphi }_s^{\prime }(s)}({\varphi }_s^{\prime }(U_s^{\prime }))\text{ or }{\pi }_J\circ {\lambda }_{J,{\varphi }_s^{\prime }(s),k}({\varphi }_s^{\prime }(U_s^{\prime }))$.

---

3: Note

The motivation for this proposition is that while the local slice condition for embedded submanifold or the local slice condition for embedded submanifold with boundary is usually described in natural languages, such a description is not handy for checking the conformance to the condition or the consequences of the condition.

Proof is not any proof for the proposition '$S$ is an embedded submanifold without or with boundary if and only if $S$ satisfies the local slice condition' but a proof for the formalizations to be valid.

The reason why we need to specify ${\varphi }_s^{\prime }(s{)}^k=0$ for the with-boundary case is that otherwise, ${\pi }_J\circ {\varphi }_s^{\prime }(U_s^{\prime }\cap S)$ would not be any open subset of ${\mathbb{H}}^d$; that specification is not any big deal because it is just about translating the chart map if it was that ${\varphi }_s^{\prime }(s{)}^k\ne 0$; in fact, a usual practice is that ${\varphi }_s^{\prime }$ is chosen such that ${\varphi }_s^{\prime }(s)=0$.

---

4: Proof

Whole Strategy: Step 1: see that the local slice condition for embedded submanifold at $s$ equals the formalization; Step 2: see that the adopting chart satisfies the consequences; Step 3: see that the local slice condition for embedded submanifold with boundary at $s$ equals the formalization; Step 4: see that the adopting chart satisfies the consequences.

Step 1:

Let us suppose that $S$ satisfies the local slice condition for embedded submanifold at $s$.

There is a chart around $s$, $(U_s^{\prime }\subseteq M^{\prime },{\varphi }_s^{\prime })$, such that ${\varphi }_s^{\prime }(U_s^{\prime }\cap S)=\{r\in {\varphi }_s^{\prime }(U_s^{\prime })|\mathrm{\forall }j\in \{1,...,d^{\prime }\}\setminus J(r^j=c^j)\}$ for some constant, $c^j\in \mathbb{R}$ s.

As $s\in U_s^{\prime }\cap S$, ${\varphi }_s^{\prime }(s)\in {\varphi }_s^{\prime }(U_s^{\prime }\cap S)=\{r\in {\varphi }_s^{\prime }(U_s^{\prime })|\mathrm{\forall }j\in \{1,...,d^{\prime }\}\setminus J(r^j=c^j)\}$, which implies that $\mathrm{\forall }j\in \{1,...,d^{\prime }\}\setminus J({\varphi }_s^{\prime }(s{)}^j=c^j)$, which means that $\{r\in {\varphi }_s^{\prime }(U_s^{\prime })|\mathrm{\forall }j\in \{1,...,d^{\prime }\}\setminus J(r^j=c^j)\}=\{r\in {\varphi }_s^{\prime }(U_s^{\prime })|\mathrm{\forall }j\in \{1,...,d^{\prime }\}\setminus J(r^j={\varphi }_s^{\prime }(s{)}^j)\}={\lambda }_{J,{\varphi }_s^{\prime }(s)}({\varphi }_s^{\prime }(U_s^{\prime }))$.

So, ${\varphi }_s^{\prime }(U_s^{\prime }\cap S)={\lambda }_{J,{\varphi }_s^{\prime }(s)}({\varphi }_s^{\prime }(U_s^{\prime })))$.

Let us suppose that $S$ satisfies that $\mathrm{\exists }(U_s^{\prime }\subseteq M^{\prime },{\varphi }_s^{\prime })\in \{\text{ the charts around }s\text{ of }{M}^{\prime }\}({\varphi }_s^{\prime }(U_s^{\prime }\cap S)={\lambda }_{J,{\varphi }_s^{\prime }(s)}({\varphi }_s^{\prime }(U_s^{\prime })))$.

${\lambda }_{J,{\varphi }_s^{\prime }(s)}({\varphi }_s^{\prime }(U_s^{\prime }))=\{r\in {\varphi }_s^{\prime }(U_s^{\prime }))|\mathrm{\forall }j\in \{1,...,d^{\prime }\}\setminus J(r^j={\varphi }_s^{\prime }(s{)}^j)\}$. As $c^j:={\varphi }_s^{\prime }(s{)}^j$ s are constants, $S$ satisfies the local slice condition for embedded submanifold at $s$.

Step 2:

Let us suppose that $S$ satisfies the local slice condition for embedded submanifold at $s$.

The corresponding adopting chart is $(U_s=U_s^{\prime }\cap S,{\varphi }_s={\pi }_J\circ {\varphi }_s^{\prime }{|}_{U_s})$ (we do not intend to prove here that it is indeed a chart for the embedded submanifold, which is something proved in the proposition '$S$ is an embedded submanifold if and only if $S$ satisfies the local slice condition').

${\varphi }_s(U_s)={\pi }_J\circ {\varphi }_s^{\prime }{|}_{U_s}(U_s)={\pi }_J\circ {\varphi }_s^{\prime }(U_s)={\pi }_J\circ {\varphi }_s^{\prime }(U_s^{\prime }\cap S)={\pi }_J\circ {\lambda }_{J,{\varphi }_s^{\prime }(s)}({\varphi }_s^{\prime }(U_s^{\prime }))$.

Step 3:

Let us suppose that $S$ satisfies the local slice condition for embedded submanifold with boundary at $s$.

There is a chart around $s$, $(U_s^{\prime }\subseteq M^{\prime },{\varphi }_s^{\prime })$, such that ${\varphi }_s^{\prime }(U_s^{\prime }\cap S)=\{r\in {\varphi }_s^{\prime }(U_s^{\prime })|\mathrm{\forall }j\in \{1,...,d^{\prime }\}\setminus J(r^j=c^j)\}$ or ${\varphi }_s^{\prime }(s{)}^k=0\wedge {\varphi }_s^{\prime }(U_s^{\prime }\cap S)=\{r\in {\varphi }_s^{\prime }(U_s^{\prime })|\mathrm{\forall }j\in \{1,...,d^{\prime }\}\setminus J(r^j=c^j)\wedge 0\le r^k\}$ for some constant, $c^j\in \mathbb{R}$ s.

As $s\in U_s^{\prime }\cap S$, ${\varphi }_s^{\prime }(s)\in {\varphi }_s^{\prime }(U_s^{\prime }\cap S)=\{r\in {\varphi }_s^{\prime }(U_s^{\prime })|\mathrm{\forall }j\in \{1,...,d^{\prime }\}\setminus J(r^j=c^j)\}\text{ or }\{r\in {\varphi }_s^{\prime }(U_s^{\prime })|\mathrm{\forall }j\in \{1,...,d^{\prime }\}\setminus J(r^j=c^j)\wedge 0\le r^k\}$, which implies that $\mathrm{\forall }j\in \{1,...,d^{\prime }\}\setminus J({\varphi }_s^{\prime }(s{)}^j=c^j)$, which means that $\{r\in {\varphi }_s^{\prime }(U_s^{\prime })|\mathrm{\forall }j\in \{1,...,d^{\prime }\}\setminus J(r^j=c^j)\}=\{r\in {\varphi }_s^{\prime }(U_s^{\prime })|\mathrm{\forall }j\in \{1,...,d^{\prime }\}\setminus J(r^j={\varphi }_s^{\prime }(s{)}^j)\}={\lambda }_{J,{\varphi }_s^{\prime }(s)}({\varphi }_s^{\prime }(U_s^{\prime })))$ and $\{r\in {\varphi }_s^{\prime }(U_s^{\prime })|\mathrm{\forall }j\in \{1,...,d^{\prime }\}\setminus J(r^j=c^j)\wedge {\varphi }_s^{\prime }(s{)}^k\le r^k\}=\{r\in {\varphi }_s^{\prime }(U_s^{\prime })|\mathrm{\forall }j\in \{1,...,d^{\prime }\}\setminus J(r^j={\varphi }_s^{\prime }(s{)}^j)\wedge {\varphi }_s^{\prime }(s{)}^k\le r^k\}={\lambda }_{J,{\varphi }_s^{\prime }(s),k}({\varphi }_s^{\prime }(U_s^{\prime })))$.

So, ${\varphi }_s^{\prime }(U_s^{\prime }\cap S)={\lambda }_{J,{\varphi }_s^{\prime }(s)}({\varphi }_s^{\prime }(U_s^{\prime }))\text{ or }{\varphi }_s^{\prime }(s{)}^k=0\wedge {\varphi }_s^{\prime }(U_s^{\prime }\cap S)={\lambda }_{J,{\varphi }_s^{\prime }(s),k}({\varphi }_s^{\prime }(U_s^{\prime }))$.

Let us suppose that $S$ satisfies that $\mathrm{\exists }(U_s^{\prime }\subseteq M^{\prime },{\varphi }_s^{\prime })\in \{\text{ the charts around }s\text{ of }{M}^{\prime }\}({\varphi }_s^{\prime }(U_s^{\prime }\cap S)={\lambda }_{J,{\varphi }_s^{\prime }(s)}({\varphi }_s^{\prime }(U_s^{\prime }))\text{ or }{\varphi }_s^{\prime }(s{)}^k=0\wedge {\varphi }_s^{\prime }(U_s^{\prime }\cap S)={\lambda }_{J,{\varphi }_s^{\prime }(s),k}({\varphi }_s^{\prime }(U_s^{\prime })))$.

${\lambda }_{J,{\varphi }_s^{\prime }(s)}({\varphi }_s^{\prime }(U_s^{\prime })))=\{r\in {\varphi }_s^{\prime }(U_s^{\prime }))|\mathrm{\forall }j\in \{1,...,d^{\prime }\}\setminus J(r^j={\varphi }_s^{\prime }(s{)}^j)\}$ and ${\lambda }_{J,{\varphi }_s^{\prime }(s),k}({\varphi }_s^{\prime }(U_s^{\prime })))=\{r\in {\varphi }_s^{\prime }(U_s^{\prime }))|\mathrm{\forall }j\in \{1,...,d^{\prime }\}\setminus J(r^j={\varphi }_s^{\prime }(s{)}^j)\wedge {\varphi }_s^{\prime }(s{)}^k\le r^k\}$. As $c^j:={\varphi }_s^{\prime }(s{)}^j$ s are constants and that ${\varphi }_s^{\prime }(s{)}^k=0$ makes ${\varphi }_s^{\prime }(s{)}^k\le r^k$ to be $0\le r^k$, $S$ satisfies the local slice condition for embedded submanifold with boundary at $s$.

Step 4:

Let us suppose that $S$ satisfies the local slice condition for embedded submanifold with boundary at $s$.

The corresponding adopting chart is $(U_s=U_s^{\prime }\cap S,{\varphi }_s={\pi }_J\circ {\varphi }_s^{\prime }{|}_{U_s})$ (we do not intend to prove here that it is indeed a chart for the embedded submanifold with boundary, which is something proved in the proposition '$S$ is an embedded submanifold with boundary if and only if $S$ satisfies the local slice condition').

${\varphi }_s(U_s)={\pi }_J\circ {\varphi }_s^{\prime }{|}_{U_s}(U_s)={\pi }_J\circ {\varphi }_s^{\prime }(U_s)={\pi }_J\circ {\varphi }_s^{\prime }(U_s^{\prime }\cap S)={\pi }_J\circ {\lambda }_{J,{\varphi }_s^{\prime }(s)}({\varphi }_s^{\prime }(U_s^{\prime }))\text{ or }{\pi }_J\circ {\lambda }_{J,{\varphi }_s^{\prime }(s),k}({\varphi }_s^{\prime }(U_s^{\prime }))$.

---

References

<The previous article in this series | The table of contents of this series | The next article in this series>