Proposition (induced map by covering map is injective):
Let be a covering space, and let . Then the induced map
is injective.
Proof: Suppose that are loops at such that . Then there exists a homotopy from to , which are both loops at . This homotopy lifts uniquely to a homotopy such that . Moreover fixes the basepoint, because the maps and are continuous and hence map connected sets to connected sets, and the preimage of a point under a covering map bears the discrete topology. By uniqueness of path lifting, will be equal to , so that .
Proof: Suppose that lifts , so that . Then so that, since maps to , we indeed have .
Conversely, suppose that . Then we define a lift of as follows: For each , choose a path so that and by path-connectedness of . By path lifting, lifts uniquely to a path . Then set . We have to show that this definition does not depend on the choice of . Indeed, let be another path like . Then is a loop at that induces an equivalence class . This in turn induces an equivalence class ; indeed, , since both are composition with the map . By the assumption, there exists a loop in such that . Moreover, is a path in that may be lifted to a path in . Since we may lift homotopies, we may lift a homotopy between and to a homotopy between and , which, similarly to the proof of injectivity of , leaves the endpoints fixed. Hence, is a loop, and in particular restricted to yields, when direction is reversed, a lift of that connects to . We conclude well-definedness.
It remains to prove continuity. Hence, let be arbitrary; we shall prove continuity at . Pick an evenly covered neighbourhood about . Let be the open set mapping homeomorphically to which contains . Let be any open neighbourhood of . Set to be the image of (which is open) under , so that is itself open. By continuity of , there exists an open neihbourhood of that is mapped by into . By strong local connectedness, choose to be connected. Recall that maps from connected domains lift uniquely; this shows that on , we have . Hence, maps into .
Finally, connectedness of implies that is unique.