Homotopy between composites of homotopic loops

From Topospaces

Statement

Existential version

Suppose is a topological space, is a point in , and are loops based at with the property that is homotopic to (as a loop based at ) and is homotopic to (again, as a loop based at ). Then, is homotopic to .

Constructive/explicit version

More explicitly, suppose is a homotopy from to . In other words, is a continuous map (where is the circle, viewed as with endpoints identified, and is the closed unit interval) having the following properties:

  • (here is the chosen basepoint of the circle from which we're mapping). This says that the loop always remains based on .

Similarly, suppose is a continuous map having the following properties:

  • (here is the chosen basepoint of the circle). This says that the loop always remains based on .

Then, we can consider the following homotopy from to :

We can think of as .

Graphical version

The pictures below describe the explicit construction. Note that the geometric shapes shown in these pictures can be thought of as the sources of the respective maps to , with the additional caveat that the boundary vertical lines map to the point . (The same pictures, without the collapse of boundaries, work to establish the homotopy between composites of homotopic paths).

The homotopy between and is a map from a filled unit square, where the restrictions of the map to the bottom and top sides of the square are and respectively. The left and right sides map to the point :

The homotopy between and is a map from a filled unit square, where the restrictions of the map to the bottom and top sides of the square are and respectively. The left and right sides map to the point :

These homotopies are composed by concatenation, as shown below. Both and need to be scaled by a factor of for the concatenated homotopy to fit in a unit square: