In mathematics, in particular in homotopy theory within algebraic topology, the homotopy lifting property (also known as an instance of the right lifting property or the covering homotopy axiom) is a technical condition on a continuous function from a topological space E to another one, B. It is designed to support the picture of E "above" B by allowing a homotopy taking place in B to be moved "upstairs" to E. For example, a covering map has a property of unique local lifting of paths to a given sheet; the uniqueness is because the fibers of a covering map are discrete spaces. The homotopy lifting property will hold in many situations, such as the projection in a vector bundle, fiber bundle or fibration, where there need be no unique way of lifting.

Formal definition

Assume all maps are continuous functions between topological spaces. Given a map, and a space Y,, one says that (Y, \pi) has the homotopy lifting property, or that \pi, has the homotopy lifting property with respect to Y, if: there exists a homotopy lifting f_\bullet (i.e., so that ) which also satisfies. The following diagram depicts this situation: The outer square (without the dotted arrow) commutes if and only if the hypotheses of the lifting property are true. A lifting corresponds to a dotted arrow making the diagram commute. This diagram is dual to that of the homotopy extension property; this duality is loosely referred to as Eckmann–Hilton duality. If the map \pi satisfies the homotopy lifting property with respect to all spaces Y, then \pi is called a fibration, or one sometimes simply says that \pi has the homotopy lifting property. A weaker notion of fibration is Serre fibration, for which homotopy lifting is only required for all CW complexes Y.

Generalization: homotopy lifting extension property

There is a common generalization of the homotopy lifting property and the homotopy extension property. Given a pair of spaces, for simplicity we denote. Given additionally a map, one says that (X, Y, \pi) has the homotopy lifting extension property if: The homotopy lifting property of (X, \pi) is obtained by taking, so that T above is simply. The homotopy extension property of (X, Y) is obtained by taking \pi to be a constant map, so that \pi is irrelevant in that every map to E is trivially the lift of a constant map to the image point of \pi.