# Homotopy between loop and composite with constant loop

## Statement

### Existential version

Suppose $x_0$ is a point in a topological space $X$ and $f$ is a loop based at $x_0$, i.e., $f$ is a continuous map from $[0,1]$ to $X$ such that $f(0) = f(1) = x_0$. Suppose $e$ is the constant loop based at $x_0$, i.e., the loop that stays at $x_0$ throughout.

Denote by $*$ the composition of loops by concatenation. Then, $f$ is homotopic to the loops $e * f$ and $f * e$.

This statement is essentially the identity element part of the proof that the Fundamental group (?) of a based topological space is indeed a group.

### Constructive/explicit version

For a loop $f$ based at $x_0$, the loop $e * f$ is given by:

$\! (e * f)(t) = \lbrace\begin{array}{rl} x_0, & 0 \le t \le 1/2\\ f(2t - 1), & 1/2 < t \le 1 \\\end{array}$

The homotopy between $f$ and $e * f$ is given by:

$\! F_\ell(t,s) = \lbrace\begin{array}{rl} x_0, & 0 \le t \le s/2 \\ f\left(\frac{2t - s}{2 - s}\right), & s/2 < t \le 1 \\\end{array}$

The loop $f * e$ is given by:

$\! (f * e)(t) = \lbrace\begin{array}{rl} f(2t), & 0 \le t \le 1/2\\ x_0, & 1/2 < t \le 1 \\\end{array}$

The homotopy between $f$ and $f * e$ is given by:

$\! F_r(t,s) = \lbrace\begin{array}{rl} f\left(\frac{2t}{2 - s}\right), & 0 \le t \le (2 - s)/2 \\ x_0 , & (2 - s)/2 < t \le 1\\\end{array}$

### Graphical version

Here is a pictorial description of the homotopy between $f$ and $e * f$:

Here is a pictorial description of the homotopy between $f$ and $f * e$: