# Covering homotopy

for a homotopy $F _ {t}$ of a mapping $F _ {0} : Z \rightarrow Y$, given a mapping $p: X \rightarrow Y$

A homotopy $G _ {t} : Z \rightarrow X$ such that $pG _ {t} = F _ {t}$. In this situation, if the covering mapping $G _ {0}$ for $F _ {0}$ is prescribed in advance, one says that $G _ {t}$ extends $G _ {0}$. The covering homotopy axiom, in its strong version, requires that, for a given mapping $p: X \rightarrow Y$, for any homotopy $F _ {t} : Z \rightarrow Y$ from a paracompactum $Z$ and for any $G _ {0}$ ($pG _ {0} = F _ {0}$), an extension of $G _ {0}$ to a covering homotopy $G _ {t}$ exists. In that case $p$ is said to be a Hurewicz fibration. The most important example is provided by the locally trivial fibre bundles (cf. Locally trivial fibre bundle). If the covering homotopy property is only required to hold in the case that $Z$ is a finite polyhedron, $p$ is called a Serre fibration.

Let $X$ and $Y$ be arcwise connected and let $P _ {A}$ be the path space of $A$ (i.e. the space of continuous mappings $q: [ 0, 1] \rightarrow A$). Consider a continuous mapping

$$\mu : D \rightarrow P _ {X} ,$$

where

$$D = \ \{ {( x, q) } : {x \in X, q \in P _ {Y} , p ( x) = q ( 0) } \} \subset \ X \times P _ {Y} ,$$

and assume that $\mu ( x, q)$ begins at a point $x$ and covers $q$. Then the formula $G _ {t} ( x) = \mu ( G _ {0} ( x), F _ {t} ( x))$ yields an extension of $G _ {0}$ to a covering homotopy $G _ {t}$. In particular, a mapping $M$ satisfying these conditions can be defined naturally for a covering, and also for a smooth vector bundle with a fixed connection. The validity of the covering homotopy axiom in Serre's formulation makes it possible to construct the exact homotopy sequence of a fibration (see Homotopy group).