第1スペース（空間）から第2スペース（空間）の中へのコンティニュアスマップ（連続写像）および第2スペース（空間）から第3スペース（空間）の中へのコンティニュアスマップ（連続写像）に対して、もしも、第2マップ（写像）および第1マップ（写像）の後に第2マップ（写像）を行なうコンポジション（合成）がホモトピーイクイバレンス（同値写像）たちである場合、第1マップ（写像）はホモトピーイクイバレンス（同値写像）であることの記述/証明
話題
About: トポロジカルスペース（空間）
この記事の目次
開始コンテキスト
- 読者は、ホモトピーイクイバレンス（同値写像）の定義を知っている。
- 読者は、任意のトポロジカルスペース（空間）たちの任意のサブスペース（部分空間）たちの間の任意のマップ（写像）たちで任意の対応するポイントたちでコンティニュアス（連続）であるものに対して、コンポジション（合成）は当該ポイントにおいてコンティニュアス（連続）であるという命題を認めている。
- 読者は、任意の第1トポロジカルスペース（空間）から任意の第2トポロジカルスペース（空間）の中への任意のホモトピックマップ（写像）たちおよび任意の第2トポロジカルスペース（空間）から任意の第3トポロジカルスペース（空間）の中への任意のホモトピックマップ（写像）たちに対して、当該ホモトピックマップ（写像）たちのコンポジション（合成）たちはホモトピックであるという命題を認めている。
- 読者は、任意のトポロジカルスペース（空間）たち間の全てのコンティニュアス（連続）マップ（写像）たちのセット（集合）上において、ホモトピックであることはイクイバレンスリレーション（同値関係）であるという命題を認めている。
ターゲットコンテキスト
- 読者は、任意の第1トポロジカルスペース（空間）から任意の第2トポロジカルスペース（空間）の中への任意のコンティニュアスマップ（連続写像）および当該第2スペース（空間）から任意の第3トポロジカルスペース（空間）の中への任意のコンティニュアスマップ（連続写像）に対して、もしも、第2マップ（写像）および第1マップ（写像）の後に第2マップ（写像）を行なうコンポジション（合成）が何らかのホモトピーイクイバレンス（同値写像）たちである場合、第1マップ（写像）はあるホモトピーイクイバレンス（同値写像）であるという命題の記述および証明を得る。
オリエンテーション
本サイトにてこれまで議論された定義たちの一覧があります。
本サイトにてこれまで議論された命題たちの一覧があります。
本体
1: 構造化された記述
ここに'構造化された記述'のルールたちがある。
エンティティ（実体）たち:
\(T_1\): \(\in \{\text{ 全てのトポロジカルスペース（空間）たち }\}\)
\(T_2\): \(\in \{\text{ 全てのトポロジカルスペース（空間）たち }\}\)
\(T_3\): \(\in \{\text{ 全てのトポロジカルスペース（空間）たち }\}\)
\(f_1\): \(: T_1 \to T_2\), \(\in \{\text{ 全てのコンティニュアスマップ（連続写像）たち }\}\)
\(f_2\): \(: T_2 \to T_3\), \(\in \{\text{ 全てのコンティニュアスマップ（連続写像）たち }\}\)
//
ステートメント（言明）たち:
\(f_2 \in \{\text{ 全てのホモトピーイクイバレンス（同値写像）たち }\} \land f_2 \circ f_1 \in \{\text{ 全てのホモトピーイクイバレンス（同値写像）たち }\}\)
\(\implies\)
\(f_1 \in \{\text{ 全てのホモトピーイクイバレンス（同値写像）たち }\}\)
//
2: 注
\(f_1\)は、コンティニュアス（連続）であると事前仮定されている必要がある、本命題に対して、なぜなら、"証明"は、\(f_1\)はコンティニュアス（連続）であることを証明しない、それは、\(f_1\)があるホモトピーイクイバレンス（同値写像）であるためのある必要要件である。
3: Proof
Whole Strategy: Step 1: take \(\widetilde{f_3}: T_3 \to T_2\) such that \(\widetilde{f_3} \circ f_2 \simeq id_{T_2}\) and \(f_2 \circ \widetilde{f_3} \simeq id_{T_3}\) and \(\widetilde{\widetilde{f_3}}: T_3 \to T_1\) such that \(\widetilde{\widetilde{f_3}} \circ f_2 \circ f_1 \simeq id_{T_1}\) and \(f_2 \circ f_1 \circ \widetilde{\widetilde{f_3}} \simeq id_{T_3}\); Step 2: see that \(\widetilde{\widetilde{f_3}} \circ f_2 \circ f_1 \simeq id_{T_1}\) and \(f_1 \circ \widetilde{\widetilde{f_3}} \circ f_2 \simeq id_{T_2}\).
Step 1:
There is a continuous \(\widetilde{f_3}: T_3 \to T_2\) such that \(\widetilde{f_3} \circ f_2 \simeq id_{T_2}\) and \(f_2 \circ \widetilde{f_3} \simeq id_{T_3}\), by Note for the definition of homotopy equivalence.
There is a continuous \(\widetilde{\widetilde{f_3}}: T_3 \to T_1\) such that \(\widetilde{\widetilde{f_3}} \circ f_2 \circ f_1 \simeq id_{T_1}\) and \(f_2 \circ f_1 \circ \widetilde{\widetilde{f_3}} \simeq id_{T_3}\), likewise.
Step 2:
Let us take \(\widetilde{\widetilde{f_3}} \circ f_2: T_2 \to T_1\).
\(\widetilde{\widetilde{f_3}} \circ f_2\) 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.
\(\widetilde{\widetilde{f_3}} \circ f_2 \circ f_1 \simeq id_{T_1}\), which has been seen above.
\(f_1 \circ \widetilde{\widetilde{f_3}} \circ f_2 = id_{T_2} \circ f_1 \circ \widetilde{\widetilde{f_3}} \circ f_2 \simeq \widetilde{f_3} \circ f_2 \circ f_1 \circ \widetilde{\widetilde{f_3}} \circ f_2\), because \(id_{T_2} \simeq \widetilde{f_3} \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, \(= \widetilde{f_3} \circ (f_2 \circ f_1 \circ \widetilde{\widetilde{f_3}}) \circ f_2 \simeq \widetilde{f_3} \circ id_{T_3} \circ f_2\), because \(f_2 \circ f_1 \circ \widetilde{\widetilde{f_3}} \simeq id_{T_3}\), as before, \(= \widetilde{f_3} \circ f_2 \simeq id_{T_2}\).
By the proposition that on the set of the continuous maps between any topological spaces, being homotopic is an equivalence relation, \(f_1 \circ \widetilde{\widetilde{f_3}} \circ f_2 \simeq id_{T_2}\).
So, \(f_1\) is a homotopy equivalence.
