Homotopy between loop and composite with constant loop

From Topospaces
Jump to: navigation, search

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:

Homotopyforleftcompositionwithtrivialloop.png

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

Homotopyforrightcompositionwithtrivialloop.png