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