ホモトピックマップ（写像）たちのコンポジションたちはホモトピックである、ホモトピーをこれとして、ことの記述/証明
話題
About: トポロジカルスペース（空間）
この記事の目次
開始コンテキスト
- 読者は、ホモトピックマップ（写像）たちの定義を知っている。
- 読者は、任意のトポロジカルスペース（空間）から任意のプロダクトトポロジカルスペース（空間）の中への任意のマップ（写像）はコンティニュアス（連続）である、もしも、各コンポーネントマップ（写像）がコンティニュアス（連続）である場合、そしてその場合に限って、という命題を認めている。
- 読者は、任意のトポロジカルスペース（空間）たちの任意のサブスペース（部分空間）たちの間の任意のマップ（写像）たちで任意の対応するポイントたちでコンティニュアス（連続）であるものに対して、コンポジション（合成）は当該ポイントにおいてコンティニュアス（連続）であるという命題を認めている。
ターゲットコンテキスト
- 読者は、任意の第1トポロジカルスペース（空間）から任意の第2トポロジカルスペース（空間）の中への任意のホモトピックマップ（写像）たちおよび当該第2トポロジカルスペース（空間）から任意の第3トポロジカルスペース（空間）の中への任意のホモトピックマップ（写像）たちに対して、当該ホモトピックマップ（写像）たちのコンポジションたちはホモトピックである、これをあるホモトピーとして、という命題の記述および証明を得る。
オリエンテーション
本サイトにてこれまで議論された定義たちの一覧があります。
本サイトにてこれまで議論された命題たちの一覧があります。
本体
1: 構造化された記述
ここに'構造化された記述'のルールたちがある。
エンティティ（実体）たち:
\(T_1\): \(\in \{\text{ 全てのトポロジカルスペース（空間）たち }\}\)
\(T_2\): \(\in \{\text{ 全てのトポロジカルスペース（空間）たち }\}\)
\(T_3\): \(\in \{\text{ 全てのトポロジカルスペース（空間）たち }\}\)
\(f_1\): \(: T_1 \to T_2\), \(\in \{\text{ 全てのコンティニュアスマップ（連続写像）たち }\}\)
\(f'_1\): \(: T_1 \to T_2\), \(\in \{\text{ 全てのコンティニュアスマップ（連続写像）たち }\}\)
\(f_2\): \(: T_2 \to T_3\), \(\in \{\text{ 全てのコンティニュアスマップ（連続写像）たち }\}\)
\(f'_2\): \(: T_2 \to T_3\), \(\in \{\text{ 全てのコンティニュアスマップ（連続写像）たち }\}\)
//
ステートメント（言明）たち:
\(f_1 \simeq f'_1 \text{ 、あるホモトピー } F_1 \text{ を持って } \land f_2 \simeq f'_2 \text{ あるホモトピー } F_2 \text{ を持って }\)
\(\implies\)
\(f_2 \circ f_1 \simeq f'_2 \circ f'_1\)、あるホモトピー\(F: T_1 \times I \to T_3, (t_1, j) \mapsto F_2 (F_1 (t_1, j), j)\)を持って
//
2: Proof
Whole Strategy: Step 1: take any homotopy from \(f_1\) to \(f'_1\), \(F_1\) and any homotopy from \(f_2\) to \(f'_2\), \(F_2\); Step 2: take \(F: T_1 \times I \to T_3, (t_1, j) \mapsto F_2 (F_1 (t_1, j), j)\) and see that \(F\) is a homotopy from \(f_2 \circ f_1\) to \(f'_2 \circ f'_1\).
Step 1:
Let us take any homotopy from \(f_1\) to \(f'_1\), \(F_1: T_1 \times I \to T_2\): \(F_1 (t_1, 0) = f_1 (t_1)\) and \(F_1 (t_1, 1) = f'_1 (t_1)\).
Let us take any homotopy from \(f_2\) to \(f'_2\), \(F_2: T_2 \times I \to T_3\): \(F_2 (t_2, 0) = f_2 (t_2)\) and \(F_2 (t_2, 1) = f'_2 (t_2)\).
Step 2:
Let us take \(F: T_1 \times I \to T_3, (t_1, j) \mapsto F_2 (F_1 (t_1, j), j)\).
\(F': T_1 \times I \to T_2 \times I, (t_1, j) \mapsto (F_1 (t_1, j), j)\) is continuous, by the proposition that any map from any topological space into any product topological space is continuous if and only if each component map is continuous: \(: T_1 \times I \to I, (t_1, j) \mapsto j\) is continuous, because for each open neighborhood of \(j\), \(U_j \subseteq I\), \(T_1 \times U_j\) is mapped into \(U_j\) where \(T_1 \times U_j \subseteq T_1 \times I\) is an open neighborhood of \((t, j)\).
\(F = F_2 \circ F'\) is continuous, by the proposition that for any maps between any arbitrary subspaces of any topological spaces continuous at any corresponding points, the composition is continuous at the point.
For each \(t_1 \in T_1\), \(F (t_1, 0) = F_2 (F_1 (t_1, 0), 0) = F_2 (f_1 (t_1), 0) = f_2 (f_1 (t_1)) = f_2 \circ f_1 (t_1)\) and \(F (t_1, 1) = F_2 (F_1 (t_1, 1), 1) = F_2 (f'_1 (t_1), 1) = f'_2 (f'_1 (t_1)) = f'_2 \circ f'_1 (t_1)\).
So, \(F\) is a homotopy from \(f_2 \circ f_1\) to \(f'_2 \circ f'_1\) and \(f_2 \circ f_1 \simeq f'_2 \circ f'_1\).
