A description/proof of that for covering map, lift of reverse of path is reverse of lift of path
Topics
About: topological space
The table of contents of this article
Starting Context
- The reader knows a definition of covering map.
- The reader knows a definition of lift of continuous map with respect to covering map.
- The reader admits the proposition that for any covering map, there is the unique lift of any path for each point in the covering map preimage of the path image of any point on the path domain.
Target Context
- The reader will have a description and a proof of the proposition that for any covering map, the lift of the reverse of any path is the reverse of the lift of the path.
Orientation
There is a list of definitions discussed so far in this site.
There is a list of propositions discussed so far in this site.
Main Body
1: Description
For any connected and locally path-connected topological spaces, \(T_1, T_2\), any covering map, \(\pi: T_1 \to T_2\), which means that \(\pi\) is continuous and surjective and around any point, \(p \in T_2\), there is a neighborhood, \(N_p \subseteq T_2\), that is evenly covered by \(\pi\), any closed interval, \(T_3 := [r_1, r_2]\), and any path, \(f: T_3 \to T_2\), for any point, \(p_0 \in T_3\), and each point, \(p'_0 \in \pi^{-1} (f (p_0))\), the lift of the reverse of \(f\), \(\widetilde{\overline{f}}: T_3 \to T_1\), such that \(\widetilde{\overline{f}} (r_2 - (p_0 - r_1)) = p'_0\), is the reverse of the lift of \(f\), \(\overline{\widetilde{f}}\), such that \(\widetilde{f} (p_0) = p'_0\), which is \(\widetilde{\overline{f}} = \overline{\widetilde{f}}\).
2: Proof
There is the unique lift of \(f\), \(\widetilde{f}\), such that \(\widetilde{f} (p_0) = p'_0\), by the proposition that for any covering map, there is the unique lift of any path for each point in the covering map preimage of the path image of any point on the path domain.
For any path, \(f': [r_1, r_2] \to T\) where \(T\) is any topological space, \(\overline{f'} (r) = f' (r_2 - (r - r_1))\) and \(\overline{f'} (r_2 - (r - r_1)) = f' (r)\), by the definition of reverse of path.
\(\overline{\widetilde{f}} (r_2 - (r - r_1)) = \widetilde{f} (r)\). \(\overline{\widetilde{f}} (r_2 - (p_0 - r_1)) = \widetilde{f} (p_0) = p'_0\). \(\pi \circ \overline{\widetilde{f}} (r) = \pi \circ \widetilde{f} (r_2 - (r - r_1)) = f (r_2 - (r - r_1)) = \overline{f} (r)\). As \(\overline{f} (r_2 - (p_0 - r_1)) = f (p_0)\), there is the unique lift of \(\overline{f}\) such that \(\widetilde{\overline{f}} (r_2 - (p_0 - r_1)) = p'_0\), by the proposition that for any covering map, there is the unique lift of any path for each point in the covering map preimage of the path image of any point on the path domain, and \(\overline{\widetilde{f}}\) has to be it, so, \(\widetilde{\overline{f}} = \overline{\widetilde{f}}\).
