Let and be a topological spaces,
be a covering of with ,
and be a continuous map.
A lift of is any function so that , topology
i.e. the following diagram commutes in :
Lifts fill a fundamental role in Homotopy theory MOC,
in particular they allow for the computation of the Fundamental group.
Their usefulness follows from the main theorem below.
i.e. the image of is a subset of the image2 of , where is the Fundamental group functor.
Furthermore if exists it is unique.
Construction of lift
A lift of is constructed as follows:
For each , by path-connectedness there exists a path from to .
Then define a path in , which by Second lemma Lifts of paths has a unique lift with .
Then let .
The proof involves four lemmas, each relying on the previous:
Uniqueness may be proven immediately,
then we prove the special cases of lifts of paths and lifts of homotopies of paths,
and then the requirement given for the fundamental group.
The reverse direction is obvious.
For the forward direction, consider the set
Let , , and be an evenly covered open neighbourhood of .
Let be the sheets over containing and respectively.
Then is an open neighbourhood of , and
Now if , then and consequently
Thus is the union of all obtained from with and is thus open.
Now if , then and consequently for all .
Thus is the union of all obtained from with and is thus open.
Therefore is clopen and inhabited (),
so since is connected, .
Hence .
Uniqueness follows from First lemma Uniqueness, but is also self-evident in the following argument.
For each , let be an evenly covered open neighbourhood of .
Then is an open cover of ,
and is an open cover of .
Using a Lebesgue number may be evenly subdivided with
so that where for all .
Now consider a lift .
Clearly ,
where is the sheet over containing .
Thus if is set, is unique and well-defined.
First, notice that if a lift of with exists,
it is necessarily unique (by First lemma Uniqueness)
and a homotopy from to :
Clearly and for all ,
and since and are discrete,
both and must be constant for all ,
so and we let .
By construction is a homotopy from to ,
but is a lift of with for each ,
thus by uniqueness in particular for ,
and hence is the desired homotopy.
For existence we use a similar construction to above:
Using a Lebesgue number argument may be subdivided into a grid with
so that for each square with ,
its image is contained entirely within an evenly covered open set in ,
i.e. .
Now consider a lift .
If the bottom left corner is set,
then clearly , where is the sheet over containing .
Then by Second lemma Lifts of paths the edges automatically agree,
thus by starting with we obtain a well-defined, unique lift of .
Fourth lemma: Condition for the existence of a lift
It remains to show that is independent from the choice of path .
To this end let be a path from to .
Then is a continuous loop with basepoint .
Since is guaranteed a lift by Second lemma Lifts of paths,
it follows ,
and thus there exists a continuous loop with basepoint such that .
Let , , and ,
so and thus .
Then if and are the lifts of and respectively with ,
then is the lift of .
Hence by Third lemma Lifts of homotopies of paths, ,
and in particular .
Hence is the same regardless of the selected path .