# Homotopy lifting property

In mathematics, in particular in homotopy theory within algebraic topology, the **homotopy lifting property** (also known as 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 due to the fact that 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 from now on all mappings are continuous functions from a topological space to another. Given a map , and a space , one says that has the * homotopy lifting property*,

^{[1]}

^{[2]}or that has the

*with respect to , if:*

**homotopy lifting property**- For any homotopy , and
- For any map lifting (i.e., so that ),

there exists a homotopy lifting (i.e., so that ) with .

The following diagram visualizes 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. Also compare this to the visualization of the homotopy extension property.

If the map satisfies the homotopy lifting property with respect to *all* spaces *X*, then is called a fibration, or one sometimes simply says that * has the homotopy lifting property*.

Note that this is the definition of *fibration in the sense of Hurewicz*, which is more restrictive than *fibration in the sense of Serre*, for which homotopy lifting only for a CW complex is required.

## Generalization: The 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 * has the homotopy lifting extension property * if:

- For any homotopy , and
- For any lifting of ,

there exists a homotopy which extends (i.e., such that ).

The homotopy lifting property of is obtained by taking , so that above is simply .

The homotopy extension property of is obtained by taking to be a constant map, so that is irrelevant in that every map to *E* is trivially the lift of a constant map to the image point of .

## See also

## Notes

## References

- {{#invoke:citation/CS1|citation

|CitationClass=book }}

- {{#invoke:citation/CS1|citation

|CitationClass=book }}

- {{#invoke:citation/CS1|citation

|CitationClass=book }}

- {{#invoke:citation/CS1|citation

|CitationClass=citation }}.

## External links

- {{#invoke:citation/CS1|citation

|CitationClass=citation }}