View source for Covering homotopy

<!--
c0269401.png
$#A+1 = 33 n = 0
$#C+1 = 33 : ~/encyclopedia/old_files/data/C026/C.0206940 Covering homotopy
Automatically converted into TeX, above some diagnostics.
Please remove this comment and the {{TEX|auto}} line below,
if TeX found to be correct.
-->

{{TEX|auto}}
{{TEX|done}}

''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|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|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|Homotopy group]]).

====Comments====
Thus, a covering homotopy is a lifting of a given homotopy (a homotopy lifting). The covering homotopy property is dual to the homotopy extension property, which defines the notion of a [[Cofibration|cofibration]].

====References====
<table><TR><TD valign="top">[a1]</TD> <TD valign="top">  E.H. Spanier,   "Algebraic topology" , McGraw-Hill  (1966)  pp. Chapt. 2</TD></TR></table>