\(C^\infty\)マニフォールド（多様体）、バウンダリー（境界）付き、たちの恣意的なサブセット（部分集合）たち間のローカルディフェオモーフィズム、ドメイン（定義域）ポイントのオープンネイバーフッド（開近傍）、ポイントイメージ（像）のオープンネイバーフッド（開近傍）に対して、ディフェオモーフィズムはネイバーフッド（近傍）たち内に包含されるように選ぶことができることの記述/証明
話題
About: \(C^\infty\)マニフォールド（多様体）
この記事の目次
開始コンテキスト
- 読者は、\(C^\infty\)マニフォールド（多様体）、バウンダリー（境界）付き、たちの任意のサブセット（部分集合）たち間のマップ（写像）でポイントにおいてローカルにディフェオモーフィックであるものの定義を知っている。
- 読者は、任意の\(C^\infty\)マニフォールド（多様体）、バウンダリー（境界）付き、たちの任意のサブセット（部分集合）たち間の任意のマップ（写像）で任意のポイントにおいてローカルにディフェオモーフィックであるものは当該ポイントにおいて\(C^\infty\)であるという命題を認めている。
- 読者は、任意の\(C^\infty\)マニフォールド（多様体）、バウンダリー（境界）付き、たちの任意のサブセット（部分集合）たち間の任意のマップ（写像）で任意のポイントにおいて\(C^k\)であるもの、ここで、\(k\)は\(\infty\)を含む、に対して、当該ポイントを包含する任意のドメイン（定義域）についてのリストリクション（制限）は当該ポイントにおいて\(C^k\)であるという命題を認めている。
- 読者は、任意の\(C^\infty\)マニフォールド（多様体）、バウンダリー（境界）付き、たちの任意のサブセット（部分集合）たち間の任意のマップ（写像）で任意のポイントにおいて\(C^k\)であるもの、ここで、\(k\)は\(\infty\)を含む、に対して、レンジ（値域）を包含する任意のコドメイン（余域）についてのリストリクション（制限）またはエクスパンション（拡張）は当該ポイントにおいて\(C^k\)であるという命題を認めている。
- 読者は、任意のトポロジカルスペース（空間）およびそれをベーススペース（空間）としてオープン（開）である任意のトポロジカルサブスペース（部分空間）に対して、サブスペース（部分空間）の任意のサブセット（部分集合）はサブスペース（部分空間）上でオープン（開）である、もしも、それがベーススペース（空間）でオープン（開）である場合、そしてその場合に限って、という命題を認めている。
ターゲットコンテキスト
- 読者は、任意の\(C^\infty\)マニフォールド（多様体）、バウンダリー（境界）付き、たちの恣意的なサブセット（部分集合）たち間の任意のローカルディフェオモーフィズム、任意のドメイン（定義域）ポイントの任意のオープンネイバーフッド（開近傍）、当該ポイントイメージ（像）の任意のオープンネイバーフッド（開近傍）に対して、あるディフェオモーフィズムは当該ネイバーフッド（近傍）たち内に包含されるように選ぶことができるという命題の記述および証明を得る。
オリエンテーション
本サイトにてこれまで議論された定義たちの一覧があります。
本サイトにてこれまで議論された命題たちの一覧があります。
本体
1: 構造化された記述
ここに'構造化された記述'のルールたちがある。
エンティティ（実体）たち:
\(M_1\): \(\in \{\text{ 全ての } C^\infty \text{ マニフォールド（多様体）、バウンダリー（境界）付き、たち }\}\)
\(M_2\): \(\in \{\text{ 全ての } C^\infty \text{ マニフォールド（多様体）、バウンダリー（境界）付き、たち }\}\)
\(S_1\): \(\subseteq M_1\)
\(S_2\): \(\subseteq M_2\)
\(f\): \(: S_1 \to S_2\), \(\in \{\text{ 全てのローカルディフェオモーフィズムたち }\}\)
\(s\): \(\in S_1\)
\(U'_s\): \(\in \{s \text{ の } S_1 \text{ 上の全てのオープンネイバーフッド（開近傍）たち }\}\)
\(U'_{f (s)}\): \(\in \{f (s) \text{ の } S_2 \text{ 上の全てのオープンネイバーフッド（開近傍）たち }\}\)
//
ステートメント（言明）たち:
\(\exists U_s \in \{s \text{ の } S_1 \text{ 上の全てのオープンネイバーフッド（開近傍）たち }\}, \exists U_{f (s)} \in \{f (s) \text{ の } S_2 \text{ 上の全てのオープンネイバーフッド（開近傍）たち }\} (U_s \subseteq U'_s \land U_{f (s)} \subseteq U'_{f (s)} \land f \vert_{U_s}: U_s \to U_{f (s)} \in \{\text{ 全てのディフェオモーフィズムたち }\})\)
//
2: 注
本命題は明らかとして受け入れられがちであるが、私たちはそれを念の為に証明しよう、一度。
典型的には、\(S_1 = M_1\)および\(S_2 = M_2\)、しかし、他のケースたちも除外しない。
3: 証明
全体戦略: ステップ1: 以下を満たす、\(s\)のあるオープンネイバーフッド（開近傍）\(U''_s \subseteq M_1\)および\(f (s)\)のあるオープンネイバーフッド（開近傍）\(U''_{f (s)} \subseteq M_2\)、つまり、\(f \vert_{U''_s \cap S_1}: U''_s \cap S_1 \to U''_{f (s)} \cap S_2\)はディフェオモーフィズムである、を取る; ステップ2: \(s\)の以下を満たすあるオープンネイバーフッド（開近傍）\(U'''_s \subseteq S_1\)、つまり、\(f (U'''_s) \subseteq U'_{f (s)}\)、を取る; ステップ3: \(U_s := U'_s \cap U''_s \cap U'''_s\)および\(U_{f (s)} := f (U_s)\)を取り、\(U_s \subseteq S_1\)は\(s\)のオープンネイバーフッド（開近傍）であり、\(U_{f (s)} \subseteq S_2\)は\(f (s)\)のオープンネイバーフッド（開近傍）であり、\(U_s \subseteq U'_s\)、\(U_{f (s)} \subseteq U'_{f (s)}\)、\(f \vert_{U_s}: U_s \to U_{f (s)}\)はディフェオモーフィズムであることを見る。
ステップ1:
以下を満たす、\(s\)のあるオープンネイバーフッド（開近傍）\(U''_s \subseteq M_1\)および\(f (s)\)のあるオープンネイバーフッド（開近傍）\(U''_{f (s)} \subseteq M_2\)、つまり、\(f \vert_{U''_s \cap S_1}: U''_s \cap S_1 \to U''_{f (s)} \cap S_2\)はディフェオモーフィズムである、を取ろう、それは可能である、なぜなら、\(f\)はローカルディフェオモーフィズムである。
ステップ2:
\(s\)の以下を満たすあるオープンネイバーフッド（開近傍）\(U'''_s \subseteq S_1\)、つまり、\(f (U'''_s) \subseteq U'_{f (s)}\)、を取ろう、それは可能である、なぜなら、\(f\)はコンティニュアス（連続）である、任意の\(C^\infty\)マニフォールド（多様体）、バウンダリー（境界）付き、たちの任意のサブセット（部分集合）たち間の任意のマップ（写像）で任意のポイントにおいてローカルにディフェオモーフィックであるものは当該ポイントにおいて\(C^\infty\)であるという命題によって: \(C^\infty\)であることはコンティニュアス（連続）であることを含意する、\(C^\infty\)マニフォールド（多様体）、バウンダリー（境界）付き、たちの任意のサブセット（部分集合）たち間のマップ（写像）でポイントにおいて\(C^k\)なもの、ここで、\(k\)は\(0\)を除外し\(\infty\)を含む、の定義に対する"注"内で言及されているとおり。
ステップ3:
\(U_s := U'_s \cap U''_s \cap U'''_s\)および\(U_{f (s)} := f (U_s)\)を取ろう。
\(U_s \subseteq S_1\)は\(s\)のオープンネイバーフッド（開近傍）である、なぜなら、\(s \in U_s\)、そして、\(U_s\)は\(S_1\)のオープンサブセット（開部分集合）である、なぜなら、\(U_s = U'_s \cap U''_s \cap U'''_s \cap S_1 = U'_s \cap (U''_s \cap S_1) \cap U'''_s\)、しかし、\(U''_s \cap S_1\)は\(S_1\)上でオープン（開）である、サブスペース（部分空間）トポロジーの定義によって、そして、\(U'_s\)および\(U'''_s\)は\(S_1\)上でオープン（開）である。
\(U_{f (s)} \subseteq S_2\)は\(f (s)\)のオープンネイバーフッド（開近傍）である、なぜなら、\(f (s) \in U_{f (s)}\)、なぜなら、\(s \in U_s\)であるから、\(f (s) \in f (U_s) = U_{f (s)}\)、\(U_{f (s)}\)は\(S_2\)のサブセット（部分集合）である、なぜなら、\(U_s \subseteq U'''_s\)であるから、\(f (U_s) \subseteq f (U'''_s) \subseteq U'_{f (s)} \subseteq S_2\)、そして、それは\(S_2\)上でオープン（開）である、なぜなら、\(U_s := U'_s \cap U''_s \cap U'''_s\)は\(U''_s \cap S_1\)上でオープン（開）である、なぜなら、\(= U''_s \cap S_1 \cap (U'_s \cap U'''_s) = (U''_s \cap S_1) \cap U''''_s \cap S_1\)、ここで、\(U''''_s \subseteq M_1\)は\(s\)の\(M_1\)上のオープンネイバーフッド（開近傍）である、\(= (U''_s \cap S_1) \cap U''''_s\)、したがって、\(f (U_s)\)は\(U''_{f (s)} \cap S_2\)上でオープン（開）である、なぜなら、\(f \vert_{U''_s \cap S_1}: U''_s \cap S_1 \to U''_{f (s)} \cap S_2\)はディフェオモーフィズムである、しかし、\(U''_{f (s)} \cap S_2\)は\(S_2\)上でオープン（開）であるから、\(f (U_s)\)は\(S_2\)上でオープン（開）である、任意のトポロジカルスペース（空間）およびそれをベーススペース（空間）としてオープン（開）である任意のトポロジカルサブスペース（部分空間）に対して、サブスペース（部分空間）の任意のサブセット（部分集合）はサブスペース（部分空間）上でオープン（開）である、もしも、それがベーススペース（空間）でオープン（開）である場合、そしてその場合に限って、という命題によって。
\(U_s \subseteq U'_s\)。
\(U_{f (s)} \subseteq U'_{f (s)}\)、なぜなら、\(U_s \subseteq U'''_s\)、そして、\(f (U_s) \subseteq f (U'''_s) \subseteq U'_{f (s)}\)。
\(f \vert_{U_s}: U_s \to U_{f (s)}\)はディフェオモーフィズムである、なぜなら、それはバイジェクション（全単射）である、バイジェクティブ（全単射）\(f \vert_{U''_s \cap S_1}: U''_s \cap S_1 \to U''_{f (s)} \cap S_2\)のリストリクション（制限）として、そして、それは\(C^\infty\)である、任意の\(C^\infty\)マニフォールド（多様体）、バウンダリー（境界）付き、たちの任意のサブセット（部分集合）たち間の任意のマップ（写像）で任意のポイントにおいて\(C^k\)であるもの、ここで、\(k\)は\(\infty\)を含む、に対して、当該ポイントを包含する任意のドメイン（定義域）についてのリストリクション（制限）は当該ポイントにおいて\(C^k\)であるという命題および任意の\(C^\infty\)マニフォールド（多様体）、バウンダリー（境界）付き、たちの任意のサブセット（部分集合）たち間の任意のマップ（写像）で任意のポイントにおいて\(C^k\)であるもの、ここで、\(k\)は\(\infty\)を含む、に対して、レンジ（値域）を包含する任意のコドメイン（余域）についてのリストリクション（制限）またはエクスパンション（拡張）は当該ポイントにおいて\(C^k\)であるという命題によって、そして、そのインバース（逆）は\(C^\infty\)である、同様に。
