ホモトピーイクイバレンス（同値写像）に対して、ホモトピーイクイバレンス（同値写像）にホモトピックなマップ（写像）はホモトピーイクイバレンス（同値写像）であることの記述/証明
話題
About: トポロジカルスペース（空間）
この記事の目次
開始コンテキスト
- 読者は、ホモトピーイクイバレンス（同値写像）の定義を知っている。
- 読者は、ホモトピックマップ（写像）たちの定義を知っている。
- 読者は、任意のトポロジカルスペース（空間）たちの任意のサブスペース（部分空間）たちの間の任意のマップ（写像）たちで任意の対応するポイントたちでコンティニュアス（連続）であるものに対して、コンポジション（合成）は当該ポイントにおいてコンティニュアス（連続）であるという命題を認めている。
- 読者は、任意のトポロジカルスペース（空間）から任意のプロダクトトポロジカルスペース（空間）の中への任意のマップ（写像）はコンティニュアス（連続）である、もしも、各コンポーネントマップ（写像）がコンティニュアス（連続）である場合、そしてその場合に限って、という命題を認めている。
- 読者は、任意の第1トポロジカルスペース（空間）から任意の第2トポロジカルスペース（空間）の中への任意のホモトピックマップ（写像）たちおよび任意の第2トポロジカルスペース（空間）から任意の第3トポロジカルスペース（空間）の中への任意のホモトピックマップ（写像）たちに対して、当該ホモトピックマップ（写像）たちのコンポジション（合成）たちはホモトピックであるという命題を認めている。
- 読者は、任意のトポロジカルスペース（空間）たち間の全てのコンティニュアス（連続）マップ（写像）たちのセット（集合）上において、ホモトピックであることはイクイバレンスリレーション（同値関係）であるという命題を認めている。
ターゲットコンテキスト
- 読者は、任意のホモトピーイクイバレンス（同値写像）に対して、当該ホモトピーイクイバレンス（同値写像）にホモトピックな任意のマップ（写像）はあるホモトピーイクイバレンス（同値写像）であるという命題の記述および証明を得る。
オリエンテーション
本サイトにてこれまで議論された定義たちの一覧があります。
本サイトにてこれまで議論された命題たちの一覧があります。
本体
1: 構造化された記述
ここに'構造化された記述'のルールたちがある。
エンティティ（実体）たち:
\(T_1\): \(\in \{\text{ 全てのトポロジカルスペース（空間）たち }\}\)
\(T_2\): \(\in \{\text{ 全てのトポロジカルスペース（空間）たち }\}\)
\(f_1\): \(: T_1 \to T_2\), \(\in \{ T_1 \text{ から } T_2 \text{ の中への全てのホモトピーイクイバレンス（同値写像）たち }\}\)
\(f'_1\): \(: T_1 \to T_2\), \(\in \{\text{ 全てのコンティニュアスマップ（連続写像）たち }\}\)
//
ステートメント（言明）たち:
\(f_1 \simeq f'_1\)
\(\implies\)
\(f'_1 \in \{T_1 \text{ から } T_2 \text{ の中への全てのホモトピーイクイバレンス（同値写像）たち }\}\)
//
2: Proof
Whole Strategy: Step 1: take any continuous map, \(f_2: T_2 \to T_1\), such that \(f_2 \circ f_1 \simeq id_{T_1}\) and \(f_1 \circ f_2 \simeq id_{T_2}\) and a homotopy from \(f_1\) to \(f'_1\), \(F_1\); Step 2: take any homotopy from \(f_2 \circ f_1\) to \(id_{T_1}\), \(F\), and \(F': T_1 \times I \to T_1, (t_1, j) \mapsto F (f_2 \circ F_1 (t_1, j), j)\), and see that \(F'\) is a homotopy from \(f_2 \circ f_1 \circ f_2 \circ f_1\) to \(f_2 \circ f'_1\) and that \(id_{T_1} \simeq f_2 \circ f'_1\); Step 3: take any homotopy from \(f_1 \circ f_2\) to \(id_{T_2}\), \(F\), and \(F': T_2 \times I \to T_2, (t_2, j) \mapsto F (F_1 (f_2 (t_2), j), j)\), and see that \(F'\) is a homotopy from \(f_1 \circ f_2 \circ f_1 \circ f_2\) to \(f'_1 \circ f_2\) and that \(id_{T_2} \simeq f'_1 \circ f_2\); Step 4: conclude the proposition.
Step 1:
There is a continuous map, \(f_2: T_2 \to T_1\), such that \(f_2 \circ f_1 \simeq id_{T_1}\) and \(f_1 \circ f_2 \simeq id_{T_2}\), by Note for the definition of homotopy equivalence.
There is a homotopy from \(f_1\) to \(f'_1\), \(F_1: T_1 \times I \to T_2\): for each \(t_1 \in T_1\), \(F_1 (t_1, 0) = f_1 (t_1)\) and \(F_1 (t_1, 1) = f'_1 (t_1)\).
Step 2:
Let \(F: T_1 \times I \to T_1\) be any homotopy from \(f_2 \circ f_1\) to \(id_{T_1}\): for each \(t_1 \in T_1\), \(F (t_1, 0) = f_2 \circ f_1 (t_1)\) and \(F (t_1, 1) = id_{T_1} (t_1)\).
Let us take \(F': T_1 \times I \to T_1, (t_1, j) \mapsto F (f_2 \circ F_1 (t_1, j), j)\).
\(F'': T_1 \times I \to T_1 \times I, (t_1, j) \mapsto (f_2 \circ F_1 (t_1, j), j)\) 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 and 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 \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 (f_2 \circ F_1 (t_1, 0), 0) = F (f_2 \circ f_1 (t_1), 0) = f_2 \circ f_1 (f_2 \circ f_1 (t_1)) = f_2 \circ f_1 \circ f_2 \circ f_1 (t_1)\) and \(F' (t_1, 1) = F (f_2 \circ F_1 (t_1, 1), 1) = F (f_2 \circ f'_1 (t_1), 1) = id_{T_1} (f_2 \circ f'_1 (t_1)) = f_2 \circ f'_1 (t_1)\).
So, \(f_2 \circ f_1 \circ f_2 \circ f_1 \simeq f_2 \circ f'_1\).
But as \(id_{T_1} \simeq f_2 \circ f_1\), \(id_{T_1} \circ f_2 \circ f_1 \simeq f_2 \circ f_1 \circ f_2 \circ f_1\), by the proposition that for any homotopic maps from any 1st topological space into any 2nd topological space and any homotopic maps from the 2nd topological space into any 3rd topological space, the compositions of the homotopic maps are homotopic with a homotopy as this, but the left hand side is \(f_2 \circ f_1\), so, \(f_2 \circ f_1 \simeq f_2 \circ f_1 \circ f_2 \circ f_1\).
So, \(id_{T_1} \simeq f_2 \circ f_1 \simeq f_2 \circ f_1 \circ f_2 \circ f_1 \simeq f_2 \circ f'_1\).
By the proposition that on the set of the continuous maps between any topological spaces, being homotopic is an equivalence relation, \(id_{T_1} \simeq f_2 \circ f'_1\).
Step 3:
Let \(F: T_2 \times I \to T_2\) be any homotopy from \(f_1 \circ f_2\) to \(id_{T_2}\): for each \(t_2 \in T_2\), \(F (t_2, 0) = f_1 \circ f_2 (t_2)\) and \(F (t_2, 1) = id_{T_2} (t_2)\).
Let us take \(F': T_2 \times I \to T_2, (t_2, j) \mapsto F (F_1 (f_2 (t_2), j), j)\).
\(F'': T_2 \times I \to T_2 \times I, (t_2, j) \mapsto (F_1 (f_2 (t_2), j), j)\) is continuous, by the proposition that the product map of any finite number of continuous maps is continuous by the product topologies, 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, and 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 \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_2 \in T_2\), \(F' (t_2, 0) = F (F_1 (f_2 (t_2), 0), 0) = F (f_1 (f_2 (t_2)), 0) = f_1 \circ f_2 (f_1 (f_2 (t_2))) = f_1 \circ f_2 \circ f_1 \circ f_2 (t_2)\) and \(F' (t_2, 1) = F (F_1 (f_2 (t_2), 1), 1) = F (f'_1 (f_2 (t_2)), 1) = id_{T_2} (f'_1 (f_2 (t_2))) = f'_1 (f_2 (t_2)) = f'_1 \circ f_2 (t_2)\).
So, \(f_1 \circ f_2 \circ f_1 \circ f_2 \simeq f'_1 \circ f_2\).
But as \(id_{T_2} \simeq f_1 \circ f_2\), \(id_{T_2} \circ f_1 \circ f_2 \simeq f_1 \circ f_2 \circ f_1 \circ f_2\), by the proposition that for any homotopic maps from any 1st topological space into any 2nd topological space and any homotopic maps from the 2nd topological space into any 3rd topological space, the compositions of the homotopic maps are homotopic with a homotopy as this, but the left hand side is \(f_1 \circ f_2\), so, \(f_1 \circ f_2 \simeq f_1 \circ f_2 \circ f_1 \circ f_2\).
So, \(id_{T_2} \simeq f_1 \circ f_2 \simeq f_1 \circ f_2 \circ f_1 \circ f_2 \simeq f'_1 \circ f_2\).
By the proposition that on the set of the continuous maps between any topological spaces, being homotopic is an equivalence relation, \(id_{T_2} \simeq f'_1 \circ f_2\).
Step 4:
By Step 2 and Step 3, \(f'_1\) is a homotopy equivalence, by Note for the definition of homotopy equivalence.
