ディフェオモーフィズムの後の\(C^\infty\)エンベディング（埋め込み）または\(C^\infty\)エンベディング（埋め込み）後のディフェオモーフィズムというコンポジション（合成）は\(C^\infty\)エンベディング（埋め込み）であることの記述/証明
話題
About: \(C^\infty\)マニフォールド（多様体）
この記事の目次
開始コンテキスト
- 読者は、バウンダリー（境界）付き\(C^\infty\)マニフォールド（多様体）たちの任意のサブセット（部分集合）たち間のディフェオモーフィズムの定義を知っている。
- 読者は、\(C^\infty\)エンベディング（埋め込み）の定義を知っている。
- 読者は、インジェクション（単射）たちの任意のファイナイト（有限）コンポジション（合成）はインジェクション（単射）であるという命題を認めている。
- 読者は、任意の\(C^\infty\)マニフォールド（多様体）、バウンダリー（境界）付き、たちの任意のサブセット（部分集合）たち間の任意のマップ（写像）たちで対応するポイントたちにおいて\(C^k\)であるものたち、ここで、\(k\)は\(\infty\)を含む、に対して、コンポジション（合成）はポイントにおいて\(C^k\)であるという命題を認めている。
- 読者は、任意のトポロジカルスペース（空間）たちの任意のサブスペース（部分空間）たちの間の任意のマップ（写像）たちで任意の対応するポイントたちでコンティニュアス（連続）であるものに対して、コンポジション（合成）は当該ポイントにおいてコンティニュアス（連続）であるという命題を認めている。
- 読者は、任意のコンティヌアス（連続）マップ（写像）の、ドメイン（定義域）およびコドメイン（余域）についてのリストリクション（制限）はコンティヌアス（連続）であるという命題を認めている。
ターゲットコンテキスト
- 読者は、任意のディフェオモーフィズムの後の任意の\(C^\infty\)エンベディング（埋め込み）または任意の\(C^\infty\)エンベディング（埋め込み）後の任意のディフェオモーフィズムというコンポジション（合成）は\(C^\infty\)エンベディング（埋め込み）であるという命題の記述および証明を得る。
オリエンテーション
本サイトにてこれまで議論された定義たちの一覧があります。
本サイトにてこれまで議論された命題たちの一覧があります。
本体
1: 構造化された記述
ここに'構造化された記述'のルールたちがある。
エンティティ（実体）たち:
\(M_1\): \(\in \{\text{ 全ての } C^\infty \text{ マニフォールド（多様体）、バウンダリー（境界）付き、たち }\}\)
\(M_2\): \(\in \{\text{ 全ての } C^\infty \text{ マニフォールド（多様体）、バウンダリー（境界）付き、たち }\}\)
\(M_3\): \(\in \{\text{ 全ての } C^\infty \text{ マニフォールド（多様体）、バウンダリー（境界）付き、たち }\}\)
\(f_1\): \(: M_1 \to M_2\), \(\in \{\text{ 全てのディフェオモーフィズムたち }\}\)
\(f_2\): \(: M_2 \to M_3\), \(\in \{\text{ 全て } C^\infty \text{ エンベディング（埋め込み）たち }\}\)
\(f_2 \circ f_1\): \(: M_1 \to M_3\)
\(f'_1\): \(: M_1 \to M_2\), \(\in \{\text{ 全ての } C^\infty \text{ エンベディング（埋め込み）たち }\}\)
\(f'_2\): \(: M_2 \to M_3\), \(\in \{\text{ 全てのディフェオモーフィズムたち }\}\)
\(f'_2 \circ f'_1\): \(: M_1 \to M_3\)
//
ステートメント（言明）たち:
\(f_2 \circ f_1 \in \{\text{ 全ての } C^\infty \text{ エンベディング（埋め込み）たち }\}\)
\(\land\)
\(f'_2 \circ f'_1 \in \{\text{ 全ての } C^\infty \text{ エンベディング（埋め込み）たち }\}\)
//
2: 証明
全体戦略: ステップ1: \(f_2 \circ f_1\)はインジェクティブ（単射）であることを見る; ステップ2: \(f_2 \circ f_1\)は\(C^\infty\)であることを見る; ステップ3: \(f_2 \circ f_1\)は\(C^\infty\)イマージョンであることを見る; ステップ4: \(f_2 \circ f_1\)のコドメイン（余域）リストリクション（制限）はホメオモーフィック（位相同形写像）であることを見る; ステップ5: \(f'_2 \circ f'_1\)はインジェクティブ（単射）であることを見る; ステップ6: \(f'_2 \circ f'_1\)は\(C^\infty\)であることを見る; ステップ7: \(f'_2 \circ f'_1\)は\(C^\infty\)イマージョンであることを見る; ステップ8: \(f'_2 \circ f'_1\)のコドメイン（余域）リストリクション（制限）はホメオモーフィック（位相同形写像）であることを見る。
ステップ1:
\(f_2 \circ f_1\)はインジェクティブ（単射）である、インジェクション（単射）たちの任意のファイナイト（有限）コンポジション（合成）はインジェクション（単射）であるという命題によって: 任意のディフェオモーフィズムまたは任意の\(C^\infty\)エンベディング（埋め込み）はインジェクティブ（単射）である。
ステップ2:
\(f_2 \circ f_1\)は\(C^\infty\)である、任意の\(C^\infty\)マニフォールド（多様体）、バウンダリー（境界）付き、たちの任意のサブセット（部分集合）たち間の任意のマップ（写像）たちで対応するポイントたちにおいて\(C^k\)であるものたち、ここで、\(k\)は\(\infty\)を含む、に対して、コンポジション（合成）はポイントにおいて\(C^k\)であるという命題によって。
ステップ3:
\(f_2 \circ f_1\)は\(C^\infty\)イマージョンであることを見よう。
各\(p \in M_1\)に対して、\(d_p (f_2 \circ f_1) = d_{f_1 (p)} f_2 \circ d_p f_1\)。
\(d_p f_1\) is injective (in fact, bijective) because \(f_1\) is a diffeomorphism and \(d_{f_1 (p)} f_2\) is injective because \(f_2\) is a \(C^\infty\) embedding. \(d_p f_1\)はインジェクティブ（単射）である（実のところ、バイジェクティブ（全単射））、なぜなら、\(f_1\)はディフェオモーフィズムであり、\(d_{f_1 (p)} f_2\)はインジェクティブ（単射）である、なぜなら、\(f_2\)は\(C^\infty\)エンベディング（埋め込み）である。
したがって、\(d_p (f_2 \circ f_1)\)はインジェクティブ（単射）である、インジェクション（単射）たちの任意のファイナイト（有限）コンポジション（合成）はインジェクション（単射）であるという命題によって。
したがって、\(f_2 \circ f_1\)は\(C^\infty\)イマージョンである。
ステップ4:
\(f_2 \circ f_1\)のコドメイン（余域）リストリクション（制限）\(\overline{f_2 \circ f_1}: M_1 \to f_2 \circ f_1 (M_1) \subseteq M_3\)はホメオモーフィズム（位相同形写像）であることを見よう。
\(f_2 \circ f_1\)はコンティニュアス（連続）である、任意のトポロジカルスペース（空間）たちの任意のサブスペース（部分空間）たちの間の任意のマップ（写像）たちで任意の対応するポイントたちでコンティニュアス（連続）であるものに対して、コンポジション（合成）は当該ポイントにおいてコンティニュアス（連続）であるという命題によって。
\(\overline{f_2 \circ f_1}\)はコンティニュアス（連続）である、任意のコンティヌアス（連続）マップ（写像）の、ドメイン（定義域）およびコドメイン（余域）についてのリストリクション（制限）はコンティヌアス（連続）であるという命題によって。
\(\overline{f_2 \circ f_1}\)はバイジェクション（全単射）（\(f_2 \circ f_1\)はインジェクティブ（単射）であり、サージェクティブ（全射）となるようにコドメイン（余域）はリストリクテッド（制限された）である）であるから、インバース（逆）\(\overline{f_2 \circ f_1}^{-1}: f_2 \circ f_1 (M_1) \subseteq M_3 \to M_1\)がある。
\(\overline{f_2 \circ f_1} = \overline{f_2} \circ f_1\)、ここで、\(\overline{f_2}: M_2 \to f_2 (M_2) \subseteq M_3\)は\(f_2\)のコドメイン（余域）リストリクション（制限）。
したがって、\(\overline{f_2 \circ f_1}^{-1} = f_1^{-1} \circ \overline{f_2}^{-1}\)、しかし、\(\overline{f_2}^{-1}\)はコンティニュアス（連続）である、なぜなら、\(f_2\)は\(C^\infty\)エンベディング（埋め込み）であり、\(f_1^{-1}\)はコンティニュアス（連続）である、なぜなら、\(f_1\)はディフェオモーフィズムである、したがって、\(\overline{f_2 \circ f_1}^{-1}\)はコンティニュアス（連続）である。
ステップ5:
\(f'_2 \circ f'_1\)はインジェクティブ（単射）である、インジェクション（単射）たちの任意のファイナイト（有限）コンポジション（合成）はインジェクション（単射）であるという命題によって: 任意の\(C^\infty\)エンベディング（埋め込み）または任意のディフェオモーフィズムはインジェクティブ（単射）である。
ステップ6:
\(f'_2 \circ f'_1\)は\(C^\infty\)である、任意の\(C^\infty\)マニフォールド（多様体）、バウンダリー（境界）付き、たちの任意のサブセット（部分集合）たち間の任意のマップ（写像）たちで対応するポイントたちにおいて\(C^k\)であるものたち、ここで、\(k\)は\(\infty\)を含む、に対して、コンポジション（合成）はポイントにおいて\(C^k\)であるという命題によって。
ステップ7:
\(f'_2 \circ f'_1\)は\(C^\infty\)イマージョンであることを見よう。
各\(p \in M_1\)に対して、\(d_p (f'_2 \circ f'_1) = d_{f'_1 (p)} f'_2 \circ d_p f'_1\)。
\(d_p f'_1\)はインジェクティブ（単射）である、なぜなら、\(f'_1\)は\(C^\infty\)エンベディング（埋め込み）である、そして、\(d_{f'_1 (p)} f'_2\)はインジェクティブ（単射）（実のところ、バイジェクティブ（全単射））である、なぜなら、\(f'_2\)はディフェオモーフィズムである。
したがって、\(d_p (f'_2 \circ f'_1)\)はインジェクティブ（単射）である、インジェクション（単射）たちの任意のファイナイト（有限）コンポジション（合成）はインジェクション（単射）であるという命題によって。
したがって、\(f'_2 \circ f'_1\)は\(C^\infty\)イマージョンである。
ステップ8:
\(f'_2 \circ f'_1\)のコドメイン（余域）リストリクション（制限）\(\overline{f'_2 \circ f'_1}: M_1 \to f'_2 \circ f'_1 (M_1) \subseteq M_3\)はホメオモーフィズム（位相同形写像）であることを見よう。
\(f'_2 \circ f'_1\)はコンティニュアス（連続）である、任意のトポロジカルスペース（空間）たちの任意のサブスペース（部分空間）たちの間の任意のマップ（写像）たちで任意の対応するポイントたちでコンティニュアス（連続）であるものに対して、コンポジション（合成）は当該ポイントにおいてコンティニュアス（連続）であるという命題によって。
\(\overline{f'_2 \circ f'_1}\)はコンティニュアス（連続）である、任意のコンティヌアス（連続）マップ（写像）の、ドメイン（定義域）およびコドメイン（余域）についてのリストリクション（制限）はコンティヌアス（連続）であるという命題によって。
\(\overline{f'_2 \circ f'_1}\)はバイジェクション（全単射）である（\(f'_2 \circ f'_1\)はインジェクティブ（単射）であり、サージェクティブ（全射）となるようにコドメイン（余域）はリストリクテッド（制限された）である）ので、インバース（逆）\(\overline{f'_2 \circ f'_1}^{-1}: f'_2 \circ f'_1 (M_1) \subseteq M_3 \to M_1\)がある。
\(\overline{f'_2 \circ f'_1} = \overline{f'_2} \circ \overline{f'_1}\)である、ここで、\(\overline{f'_1}: M_1 \to f'_1 (M_1) \subseteq M_2\)は\(f'_1\)のコドメイン（余域）リストリクション（制限）であり、\(\overline{f'_2}: f'_1 (M_1) \subseteq M_2 \to f'_2 \circ f'_1 (M_1) \subseteq M_3\)は\(f'_2\)のドメイン（定義域）およびコドメイン（余域）リストリクション（制限）である。
したがって、\(\overline{f'_2 \circ f'_1}^{-1} = \overline{f'_1}^{-1} \circ \overline{f'_2}^{-1}\)、しかし、\(\overline{f'_2}^{-1}\)はコンティニュアス（連続）である、なぜなら、\(f'_2\)はディフェオモーフィズムである、任意のコンティヌアス（連続）マップ（写像）の、ドメイン（定義域）およびコドメイン（余域）についてのリストリクション（制限）はコンティヌアス（連続）であるという命題によって、そして、\(\overline{f'_1}^{-1}\)はコンティニュアス（連続）である、なぜなら、\(f'_1\)は\(C^\infty\)エンベディング（埋め込み）である。したがって、\(\overline{f_2 \circ f_1}^{-1}\)はコンティニュアス（連続）である。
