エンベッデッドサブマニフォールド（部分多様体）に対するローカルスライスコンディションまたはエンベッデッドサブマニフォールド（部分多様体）、バウンダリー（境界）付き、に対するローカルスライスコンディションのフォーマライゼーション（定式化）の記述/証明
話題
About: \(C^\infty\)マニフォールド（多様体）
この記事の目次
開始コンテキスト
- 読者は、\(C^\infty\)マニフォールド（多様体）、バウンダリー（境界）付き、のエンベッデッドサブマニフォールド（部分多様体）、バウンダリー（境界）付き、の定義を知っている。
- 読者は、ユークリディアンセット（集合）上のスライシングマップ（写像）の定義を知っている。
- 読者は、ユークリディアンセット（集合）上のスライシングアンドハーフ化マップ（写像）の定義を知っている。
- 読者は、ユークリディアンセット（集合）たち間プロジェクション（射影）の定義を知っている。
ターゲットコンテキスト
- 読者は、エンベッデッドサブマニフォールド（部分多様体）に対するローカルスライスコンディションまたはエンベッデッドサブマニフォールド（部分多様体）、バウンダリー（境界）付き、に対するローカルスライスコンディションのフォーマライゼーション（定式化）は妥当であるという命題の記述および証明を得る。
オリエンテーション
本サイトにてこれまで議論された定義たちの一覧があります。
本サイトにてこれまで議論された命題たちの一覧があります。
本体
1: 構造化された記述
ここに'構造化された記述'のルールたちがある。
エンティティ（実体）たち:
\(M'\): \(\in \{ \text{ the } d' \text{ ディメンショナル（次元） } C^\infty \text{ マニフォールド（多様体）たち } \}\)
\(S\): \(\subseteq M'\)
\(J\): \(\subseteq \{1, ..., d'\}\)で、\(\vert J \vert = d\)を満たすもの
\(k\): \(\in J\)
\(s\): \(\in S\)
\(\lambda_{J, r'}\): \(: Pow (\mathbb{R}^{d'}) \to Pow (\mathbb{R}^{d'})\), \(= \text{ 当該スライシングマップ（写像） }\)、ここで、\(r' \in \mathbb{R}^{d'}\)は任意のもの
\(\lambda_{J, r', k}\): \(: Pow (\mathbb{R}^{d'}) \to Pow (\mathbb{R}^{d'})\), \(= \text{ 当該スライシングアンドハーフ化マップ（写像） }\)、ここで、\(r' \in \mathbb{R}^{d'}\)は任意のもの
\(\pi_J\): \(: \mathbb{R}^{d'} \to \mathbb{R}^d\), \(= \text{ 当該プロジェクション（射影） }\)
//
ステートメント（言明）たち:
(
\(S\)は、\(s\)において、エンベッデッドサブマニフォールド（部分多様体）に対するローカルスライスコンディションを満たす
\(\iff\)
\(\exists (U'_s \subseteq M', \phi'_s) \in \{s \text{ の周りの } M' \text{ の全てのチャートたち }\} (\phi'_s (U'_s \cap S) = \lambda_{J, \phi'_s (s)} (\phi'_s (U'_s)))\)
\(\implies\)
(
\((U_s = U'_s \cap S, \phi_s = \pi_J \circ \phi'_s \vert_{U_s})\)は、対応するアダプティングチャート
\(\land\)
\(\phi_s (U_s) = \pi_J \circ \phi'_s (U_s) = \pi_J \circ \lambda_{J, \phi'_s (s)} (\phi'_s (U'_s))\)
)
)
\(\land\)
(
\(S\)は、\(s\)において、エンベッデッドサブマニフォールド（部分多様体）、バウンダリー（境界）付き、に対するローカルスライスコンディションを満たす
\(\iff\)
\(\exists (U'_s \subseteq M', \phi'_s) \in \{s \text{ の周りの } M' \text{ の全てのチャートたち }\} (\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))))\)
\(\implies\)
(
\((U_s = U'_s \cap S, \phi_s = \pi_J \circ \phi'_s \vert_{U_s})\)は、対応するアダプティングチャート
\(\land\)
\(\phi_s (U_s) = \pi_J \circ \phi'_s (U_s) = \pi_J \circ \lambda_{J, \phi'_s (s)} (\phi'_s (U'_s)) \text{ or } \pi_J \circ \lambda_{J, \phi'_s (s), k} (\phi'_s (U'_s))\)
)
)
//
2: 自然言語記述
任意の\(d'\)ディメンショナル（次元）\(C^\infty\)マニフォールド（多様体）\(M'\)、任意のサブセット（部分集合）\(S \subseteq M'\)、以下を満たす任意のサブセット（部分集合）\(J \subseteq \{1, ..., d'\}\)、つまり、\(\vert J \vert = d\)、任意の\(k \in J\)、任意のポイント\(s \in S\)、スライシングマップ（写像）\(\lambda_{J, r'}: Pow (\mathbb{R}^{d'}) \to Pow (\mathbb{R}^{d'})\)、ここで、\(r' \in \mathbb{R}^{d'}\)は任意のもの、スライシングアンドハーフ化マップ（写像）\(\lambda_{J, r', k}: Pow (\mathbb{R}^{d'}) \to Pow (\mathbb{R}^{d'})\)、ここで、\(r' \in \mathbb{R}^{d'}\)は任意のもの、プロジェクション（射影）\(\pi_J: \mathbb{R}^{d'} \to \mathbb{R}^d\)に対して、\(S\)は、\(s\)において、エンベッデッドサブマニフォールド（部分多様体）に対するローカルスライスコンディションを満たす、もしも、\(s\)の周りに以下を満たすあるチャート\((U'_s \subseteq M', \phi'_s)\)、つまり、\(\phi'_s (U'_s \cap S) = \lambda_{J, \phi'_s (s)} (\phi'_s (U'_s))\)、がある場合、そしてその場合に限って、そして、もしも、そうである場合、対応するアダプティングチャートは\((U_s = U'_s \cap S, \phi_s = \pi_J \circ \phi'_s \vert_{U_s})\)であり、\(\phi_s (U_s) = \pi_J \circ \phi'_s (U_s) = \pi_J \circ \lambda_{J, \phi'_s (s)} (\phi'_s (U'_s))\); \(S\)は、\(s\)において、エンベッデッドサブマニフォールド（部分多様体）、バウンダリー（境界）付き、に対するローカルスライスコンディションを満たす、もしも、\(s\)の周りに以下を満たすあるチャート\((U'_s \subseteq M', \phi'_s)\)、つまり、\(\phi'_s (U'_s \cap S) = \lambda_{J, \phi'_s (s)} (\phi'_s (U'_s))\)または\(\phi'_s (s)^k = 0 \land \phi'_s (U'_s \cap S) = \lambda_{J, \phi'_s (s), k} (\phi'_s (U'_s))\)、がある場合、そしてその場合に限って、そして、そうである場合、対応するアダプティングチャートは\((U_s = U'_s \cap S, \phi_s = \pi_J \circ \phi'_s \vert_{U_s})\)であり、\(\phi_s (U_s) = \pi_J \circ \phi'_s (U_s) = \pi_J \circ \lambda_{J, \phi'_s (s)} (\phi'_s (U'_s)) \text{ または } \pi_J \circ \lambda_{J, \phi'_s (s), k} (\phi'_s (U'_s))\)。
3: 注
本命題に対するモチベーションは、エンベッデッドサブマニフォールド（部分多様体）に対するローカルスライスコンディションまたはエンベッデッドサブマニフォールド（部分多様体）、バウンダリー（境界）付き、に対するローカルスライスコンディションは通常自然言語たちで記述されるが、そうした記述は、当該コンディションへの整合や当該コンディションの帰結たちをチェックするのに便利でないこと。
"証明"は、'\(S\)はエンベッデッドサブマニフォールド（部分多様体）、バウンダリー（境界）無しまたはバウンダリー（境界）付き、である、もしも、\(S\)はローカルスライスコンディションを満たす場合、そして、その場合に限って'という命題の証明ではなく、当該フォーマライゼーション（定式化）が妥当であることの証明である。
バウンダリー（境界）付きケースに対して\(\phi'_s (s)^k = 0\)を指定する必要がある理由は、そうでなければ、\(\pi_J \circ \phi'_s (U'_s \cap S)\)は\(\mathbb{H}^d\)のオープンサブセット（開部分集合）ではないことになること; その指定は重要事ではない、なぜなら、それは、単に、もしも、\(\phi'_s (s)^k \neq 0\)であったら、当該チャートマップ（写像）を平行移動すればよいだけのこと; 実のところ、大抵の場合、\(\phi'_s\)は、\(\phi'_s (s) = 0\)であるように選ばれる。
4: 証明
全体戦略: ステップ1: \(s\)における、エンベッデッドサブマニフォールド（部分多様体）に対するローカルスライスコンディションは当該フォーマライゼーション（定式化）に等しいことを見る; ステップ2: 当該アダプティングチャートは当該帰結たちを満たすことを見る; ステップ3: \(s\)における、エンベッデッドサブマニフォールド（部分多様体）、バウンダリー（境界）付き、に対するローカルスライスコンディションは当該フォーマライゼーション（定式化）に等しいことを見る; ステップ4: 当該アダプティングチャートは当該帰結たちを満たすことを見る。
ステップ1:
Let us suppose that \(S\)は、\(s\)における、エンベッデッドサブマニフォールド（部分多様体）に対するローカルスライスコンディションを満たすと仮定しよう。
\(s\)の周りに以下を満たすあるチャート\((U'_s \subseteq M', \phi'_s)\)、つまり、\(\phi'_s (U'_s \cap S) = \{r \in \phi'_s (U'_s) \vert \forall j \in \{1, ..., d'\} \setminus J (r^j = c^j)\}\)、何らかのコンスタント\(c^j \in \mathbb{R}\)たちに対して、がある。
\(s \in U'_s \cap S\)であるので、\(\phi'_s (s) \in \phi'_s (U'_s \cap S) = \{r \in \phi'_s (U'_s) \vert \forall j \in \{1, ..., d'\} \setminus J (r^j = c^j)\}\)、それが含意するのは、\(\forall j \in \{1, ..., d'\} \setminus J (\phi'_s (s)^j = c^j)\)、それが意味するのは、\(\{r \in \phi'_s (U'_s) \vert \forall j \in \{1, ..., d'\} \setminus J (r^j = c^j)\} = \{r \in \phi'_s (U'_s) \vert \forall j \in \{1, ..., d'\} \setminus J (r^j = \phi'_s (s)^j)\} = \lambda_{J, \phi'_s (s)} (\phi'_s (U'_s))\)。
したがって、\(\phi'_s (U'_s \cap S) = \lambda_{J, \phi'_s (s)} (\phi'_s (U'_s)))\)。
\(S\)は、\(\exists (U'_s \subseteq M', \phi'_s) \in \{\text{ the charts around } s \text{ of M' }\} (\phi'_s (U'_s \cap S) = \lambda_{J, \phi'_s (s)} (\phi'_s (U'_s)))\)を満たすと仮定しよう。
\(\lambda_{J, \phi'_s (s)} (\phi'_s (U'_s)) = \{r \in \phi'_s (U'_s)) \vert \forall j \in \{1, ..., d'\} \setminus J (r^j = \phi'_s (s)^j)\}\)。\(c^j := \phi'_s (s)^j\)たちはコンスタントたちであるので、\(S\)は、\(s\)における、エンベッデッドサブマニフォールド（部分多様体）に対するローカルスライスコンディションを満たす。
ステップ2:
\(S\)は、\(s\)における、エンベッデッドサブマニフォールド（部分多様体）に対するローカルスライスコンディションを満たすと仮定する。
対応するアダプティングチャートは\((U_s = U'_s \cap S, \phi_s = \pi_J \circ \phi'_s \vert_{U_s})\)（私たちは、それが本当にエンベッデッドサブマニフォールド（部分多様体）に対するチャートであること（それは、'\(S\)はエンベッデッドサブマニフォールド（部分多様体）である、もしも、\(S\)はローカルスライスコンディションを満たす場合、そして、その場合に限って'という命題の中で証明されるものである）をここで証明するつもりはない）。
\(\phi_s (U_s) = \pi_J \circ \phi'_s \vert_{U_s} (U_s) = \pi_J \circ \phi'_s (U_s) = \pi_J \circ \phi'_s (U'_s \cap S) = \pi_J \circ \lambda_{J, \phi'_s (s)} (\phi'_s (U'_s))\)。
ステップ3:
\(S\)は、\(s\)における、エンベッデッドサブマニフォールド（部分多様体）、バウンダリー（境界）付き、に対するローカルスライスコンディションを満たすと仮定しよう。
\(s\)の周りに以下を満たすチャート\((U'_s \subseteq M', \phi'_s)\)、つまり、\(\phi'_s (U'_s \cap S) = \{r \in \phi'_s (U'_s) \vert \forall j \in \{1, ..., d'\} \setminus J (r^j = c^j)\}\)または\(\phi'_s (s)^k = 0 \land \phi'_s (U'_s \cap S) = \{r \in \phi'_s (U'_s) \vert \forall j \in \{1, ..., d'\} \setminus J (r^j = c^j) \land 0 \le r^k\}\)、何らかのコンスタント\(c^j \in \mathbb{R}\)たちに対して、がある。
\(s \in U'_s \cap S\)であるから、\(\phi'_s (s) \in \phi'_s (U'_s \cap S) = \{r \in \phi'_s (U'_s) \vert \forall j \in \{1, ..., d'\} \setminus J (r^j = c^j)\} \text{ または } \{r \in \phi'_s (U'_s) \vert \forall j \in \{1, ..., d'\} \setminus J (r^j = c^j) \land 0 \le r^k\}\)、それが含意するのは、\(\forall j \in \{1, ..., d'\} \setminus J (\phi'_s (s)^j = c^j)\)、それが意味するのは、\(\{r \in \phi'_s (U'_s) \vert \forall j \in \{1, ..., d'\} \setminus J (r^j = c^j)\} = \{r \in \phi'_s (U'_s) \vert \forall j \in \{1, ..., d'\} \setminus J (r^j = \phi'_s (s)^j)\} = \lambda_{J, \phi'_s (s)} (\phi'_s (U'_s)))\)および\(\{r \in \phi'_s (U'_s) \vert \forall j \in \{1, ..., d'\} \setminus J (r^j = c^j) \land \phi'_s (s)^k \le r^k\} = \{r \in \phi'_s (U'_s) \vert \forall j \in \{1, ..., d'\} \setminus J (r^j = \phi'_s (s)^j) \land \phi'_s (s)^k \le r^k\} = \lambda_{J, \phi'_s (s), k} (\phi'_s (U'_s)))\)。
したがって、\(\phi'_s (U'_s \cap S) = \lambda_{J, \phi'_s (s)} (\phi'_s (U'_s)) \text{ または } \phi'_s (s)^k = 0 \land \phi'_s (U'_s \cap S) = \lambda_{J, \phi'_s (s), k} (\phi'_s (U'_s))\)。
\(S\)は、\(\exists (U'_s \subseteq M', \phi'_s) \in \{s \text{ の周りの} M' \text{ の全てのチャートたち }\} (\phi'_s (U'_s \cap S) = \lambda_{J, \phi'_s (s)} (\phi'_s (U'_s)) \text{ または } \phi'_s (s)^k = 0 \land \phi'_s (U'_s \cap S) = \lambda_{J, \phi'_s (s), k} (\phi'_s (U'_s)))\)を満たすと仮定する。
\(\lambda_{J, \phi'_s (s)} (\phi'_s (U'_s))) = \{r \in \phi'_s (U'_s)) \vert \forall j \in \{1, ..., d'\} \setminus J (r^j = \phi'_s (s)^j)\}\)および\(\lambda_{J, \phi'_s (s), k} (\phi'_s (U'_s))) = \{r \in \phi'_s (U'_s)) \vert \forall j \in \{1, ..., d'\} \setminus J (r^j = \phi'_s (s)^j) \land \phi'_s (s)^k \le r^k\}\)。\(c^j := \phi'_s (s)^j\)たちはコンスタントたちであり、\(\phi'_s (s)^k = 0\)は\(\phi'_s (s)^k \le r^k\)を\(0 \le r^k\)であるとするので、\(S\)は、\(s\)における、エンベッデッドサブマニフォールド（部分多様体）、バウンダリー（境界）付き、に対するローカルスライスコンディションを満たす。
ステップ4:
\(S\)は、\(s\)における、エンベッデッドサブマニフォールド（部分多様体）、バウンダリー（境界）付き、に対するローカルスライスコンディションを満たすと仮定しよう。
対応するアダプティングチャートは\((U_s = U'_s \cap S, \phi_s = \pi_J \circ \phi'_s \vert_{U_s})\)である（私たちは、それが本当にエンベッデッドサブマニフォールド（部分多様体）、バウンダリー（境界）付き、に対するチャートであること（それは、'\(S\)はエンベッデッドサブマニフォールド（部分多様体）、バウンダリー（境界）付き、である、もしも、\(S\)はローカルスライスコンディションを満たす場合、そして、その場合に限って'という命題の中で証明されるものである）をここで証明するつもりはない）。
\(\phi_s (U_s) = \pi_J \circ \phi'_s \vert_{U_s} (U_s) = \pi_J \circ \phi'_s (U_s) = \pi_J \circ \phi'_s (U'_s \cap S) = \pi_J \circ \lambda_{J, \phi'_s (s)} (\phi'_s (U'_s)) \text{ または } \pi_J \circ \lambda_{J, \phi'_s (s), k} (\phi'_s (U'_s))\)。
