I’ve been reading some algebraic topology lately. It is horrendously abstract, at least for me at my current stage. Nonetheless, I’ve managed to make a little progress. On that, I’ll say that the path lifting lemma, a beautiful fundamental result in the field, makes more sense to me now at the formal level, where as perceived by me right now, the difficulty lies largely in the formalisms.

**Path lifting lemma:** *Let be a covering projection and be a path such that for some and ,*

*Then there exists a unique path such that*

How to prove this at a high level? First, we use the Lebesgue number lemma on an open cover of by evenly covered open sets to partition into intervals of length , with the Lebesgue number, to induce pieces of the path in which all lie in some open set of the cover. Because every open set is evenly covered, we for each piece have a uniquely determined continuous map (by the homeomorphism of the covering map plus boundary condition). Glue them together to get the lifted path, via the gluing lemma.

Let be our cover of by evenly covered open sets. Let be a Lebesgue number for , with such that .

Let be restricted to . At , we have that consists of disjoint sets each of which is homeomorphic to , and we pick the one that contains , letting denote the associated map for that, to , so that , with .

We continue like this for up to , using the value imposed on the boundary, which we have by induction to determine the homeomorphism associated with the covering projection that keeps the path continuous, which we call . With this, we have

.

A continuous path is obtained by applying to the gluing lemma to these. That

is satisfied because it is satisfied on sets the union of which is the entire domain, namely .

A canonical example of path lifting is that of lifting a path on the unit circle to a path on the real line. To every point on the unit circle is associated its preimage under the map . It is not hard to verify that this is in fact a covering space. By the path lifting lemma, there is some unique path on the real line that projects to our path on the circle that ends at some integer multiple of , call it , and that path is homotopic to the direct path from to via the linear homotopy. Application of the projection onto that homotopy yields that our path on the circle, which we call , is homotopic to the path where one winds around the circle times counterclockwise, which we call .

Homotopy between and is unique. If on the other hand, were homotopic to for , they we could lift the homotopy onto the real line, thereby yielding a contradiction as there the endpoints would not be the same.

This requires a **homotopy lifting lemma**. The proof of that is similar to that of path lifting, but it is more complicated, since there is an additional homotopy parameter, by convention, within , alongside the path parameter. Again, we use the Lebesgue number lemma, but this time on grid , and again for each grid component there is a unique way to select the local homeomorphism such that there is agreement with its neighboring components, with the parameter space in common here an edge common to two adjacent grid components.

With that every path on the circle is uniquely equivalent by homotopy to some unique , we have that its fundamental group is , since clearly, , where here, is the path concatenation operation.