Homotopy between composites of homotopic loops

Statement

Existential version

Suppose $X$ is a topological space, $x_{0}$ is a point in $X$ , and $f_{1}, g_{1}, f_{2}, g_{2}$ are loops based at $x_{0}$ with the property that $f_{1}$ is homotopic to $g_{1}$ (as a loop based at $x_{0}$ ) and $f_{2}$ is homotopic to $g_{2}$ (again, as a loop based at $x_{0}$ ). Then, $f_{1} * f_{2}$ is homotopic to $g_{1} * g_{2}$ .

Constructive/explicit version

More explicitly, suppose $F_{1}$ is a homotopy from $f_{1}$ to $g_{1}$ . In other words, $F_{1} : S^{1} \times I \to X$ is a continuous map (where $S^{1}$ is the circle, viewed as $[0, 1]$ with endpoints identified, and $I = [0, 1]$ is the closed unit interval) having the following properties:

$F_{1} (s, 0) = f_{1} (s)$
$F_{1} (s, 1) = g_{1} (s)$
$F_{1} (0, t) = x_{0}$ (here $0 \sim 1$ is the chosen basepoint of the circle from which we're mapping). This says that the loop always remains based on $x_{0}$ .

Similarly, suppose $F_{2} : S^{1} \times I \to X$ is a continuous map having the following properties:

$F_{2} (s, 0) = f_{2} (s)$
$F_{2} (s, 1) = g_{2} (s)$
$F_{2} (0, t) = x_{0}$ (here $0 \sim 1$ is the chosen basepoint of the circle). This says that the loop always remains based on $x_{0}$ .

Then, we can consider the following homotopy from $f_{1} * f_{2}$ to $g_{1} * g_{2}$ :

$F (s, t) : = {\begin{matrix} F_{1} (2 s, t), & 0 \leq t \leq 1 / 2 \\ F_{2} (2 s - 1, t) & 1 / 2 < t \leq 1 \end{matrix}$

We can think of $F$ as $F_{1} * F_{2}$ .