# Homotopy between constant loop and composite of loop with inverse

## Statement

### Existential version

Suppose $x_0$ is a point in a topological space $X$. Suppose $f$ is a loop based at $x_0$, i.e., $f$ is a continuous map from the closed unit interval $[0,1]$ to $X$ such that $f(0) = f(1) = x_0$. Denote by $f^{-1}$ the loop defined as $f^{-1}(t) = f(1 - t)$. Denote by $e$ the constant loop at the point $x_0$.

Denote by $*$ the composition of loops by concatenation. Then, the loops $f * f^{-1}$ and $f^{-1} * f$ are both homotopic to $e$.

Note that since $(f^{-1})^{-1} = f$, it suffices to show that $f * f^{-1}$ is homotopic to $e$.

This is the inverses part of the proof that the Fundamental group (?) of a based topological space is indeed a group.

### Constructive/explicit version

We note that $f^{-1}(t) = f(1 - t)$, so we have:

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

The map $e$ to which we want to homotope this is:

$\! e(t) = x_0, 0 \le t \le 1$

The homotopy is given by:

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

### Graphical version

Here is a pictorial description of the homotopy:

### Uniform version

Suppose $(X,x_0)$ is a based topological space. Let $L = \Omega(X,x_0)$ be the loop space. Consider the following two maps from $L$ to itself:

$A: L \to L, \qquad A(f) = f * f^{-1}$

and:

$E:L \to L, \qquad E(f) = e$

Then, the maps $A$ and $E$ are homotopic maps.