Lifting homotopies of paths (b) for covering spaces

Proved

Hatcher.path_homotopy_lifting_property

by korbonits · Sep 4, 2026 · Mathlib 0df444a (Lean v4.33.1)

algebraic-topologycovering-spacesfundamental-grouphatcher

Let $p:\tilde X\to X$ be a covering space. Let $f_t:I\to X$ , $0\le t\le 1$ , be a homotopy of paths starting at $x_0$ : the associated map $F:I\times I\to X$ , $F(s,t)=f_t(s)$ , is continuous, and the endpoints $f_t(0)=x_0$ and $f_t(1)=x_1$ are independent of $t$ . Then for each $\tilde x_0\in p^{-1}(x_0)$ there is a unique lifted homotopy of paths $\tilde f_t:I\to\tilde X$ starting at $\tilde x_0$ ; that is, a unique continuous $\tilde F:I\times I\to\tilde X$ with

p\circ\tilde F=F,\qquad \tilde F(0,t)=\tilde x_0\ \text{ for all }t,\qquad \tilde F(1,t)\ \text{ independent of }t .

This is statement (b) in Hatcher's proof of Theorem 1.7. It is the ingredient behind the uniqueness of the integer $n$ attached to a loop in $S^1$ : a homotopy between $\omega_m$ and $\omega_n$ lifts to a homotopy of paths in $\mathbb{R}$ whose (constant) endpoint is both $m$ and $n$ .

Formalization Note The square is I × I with Hatcher's coordinate order: the first coordinate is the path parameter $s$ , the second the homotopy parameter $t$ . "Homotopy of paths" is encoded by the two hypotheses that $F(0,\cdot)$ and $F(1,\cdot)$ are constant; the conclusion asks the lift to be a homotopy of paths as well (constant left endpoint $\tilde x_0$ , constant right endpoint), and uniqueness ranges over continuous lifts with these properties.

Preamble

import Definitions.Def_Hatcher_Circle
import Mathlib

open unitInterval Hatcher

Formal statement

namespace Hatcher
theorem path_homotopy_lifting_property {E X : Type*} [TopologicalSpace E] [TopologicalSpace X]
    {p : E → X} (hp : IsCoveringMap p) (F : C(I × I, X)) (x₀ x₁ : X)
    (hx₀ : ∀ t, F (0, t) = x₀) (hx₁ : ∀ t, F (1, t) = x₁) (e₀ : E) (he₀ : p e₀ = x₀) :
    ∃! F' : C(I × I, E), p ∘ F' = F ∧ (∀ t, F' (0, t) = e₀) ∧ ∃ e₁, ∀ t, F' (1, t) = e₁ := by sorry
end Hatcher

Source

A. Hatcher, Algebraic Topology, Cambridge University Press 2002, https://pi.math.cornell.edu/~hatcher/AT/AT.pdf, Section 1.1, p. 29, statement (b) preceding the proof of Theorem 1.7; 'homotopy of paths' as defined on p. 25

Read-back

What the Lean code literally says, in plain math · claude-fable-5-1

Setting. Let $E$ and $X$ be arbitrary types, each equipped with a topology (no separation, connectedness, local path-connectedness, or nonemptiness assumptions are made on either). Let $p : E \to X$ be a function, and assume $p$ is a covering map in Mathlib's sense: for every point $x \in X$ , $x$ is evenly covered by $p$ with fibre $p^{-1}(\{x\})$ , meaning

the fibre $p^{-1}(\{x\})$ carries the discrete (subspace) topology, and
there is a set $U \subseteq X$ with $x \in U$ , $U$ open, $p^{-1}(U)$ open in $E$ , and a homeomorphism $H : p^{-1}(U) \xrightarrow{\ \sim\ } U \times p^{-1}(\{x\})$ (product topology) such that for every $e \in p^{-1}(U)$ the first component of $H(e)$ is $p(e)$ .

This notion does not assume $p$ is surjective: the fibre $p^{-1}(\{x\})$ is allowed to be empty for some (or all) $x$ . Continuity of $p$ is not a separate hypothesis; it is a consequence of the even-covering condition.

Write $I = [0,1] \subset \mathbb{R}$ for the closed unit interval with its subspace topology, and $I \times I$ for the square with the product topology; the elements $0, 1 \in I$ are the endpoints. $C(A, B)$ denotes the set of continuous maps $A \to B$ .

Data and hypotheses. The theorem takes as given:

a continuous map $F : I \times I \to X$ (we write its argument as an ordered pair $(s, t)$ , first coordinate $s$ , second coordinate $t$ );
two points $x_0, x_1 \in X$ ;
the hypothesis that $F$ is constantly $x_0$ along the edge where the first coordinate is $0$ :

\forall t \in I,\quad F(0, t) = x_0;

the hypothesis that $F$ is constantly $x_1$ along the edge where the first coordinate is $1$ :

\forall t \in I,\quad F(1, t) = x_1;

a point $e_0 \in E$ with $p(e_0) = x_0$ .

Nothing is assumed about the values of $F$ on the other two edges $\{(s,0)\}$ and $\{(s,1)\}$ ; in particular no path $I \to X$ and no lift of such a path is given in advance. Nothing is assumed relating $x_0$ and $x_1$ (they may coincide). The existence of $e_0$ forces $E$ to be nonempty and $x_0$ to lie in the image of $p$ , but no other point of $X$ is asserted to be in the image of $p$ by the hypotheses.

Conclusion. There exists a continuous map $F' : I \times I \to E$ satisfying the following three conditions simultaneously, and it is the only continuous map $I \times I \to E$ satisfying all three:

$p \circ F' = F$ as functions on $I \times I$ , i.e. $p(F'(s,t)) = F(s,t)$ for all $(s,t) \in I \times I$ ;
$F'$ is constantly $e_0$ along the edge where the first coordinate is $0$ :

\forall t \in I,\quad F'(0, t) = e_0;

$F'$ is constant along the edge where the first coordinate is $1$ : there exists some point $e_1 \in E$ (not given in advance, and not asserted to lie over $x_1$ other than implicitly via condition 1) with

\forall t \in I,\quad F'(1, t) = e_1.

Exact scope of the uniqueness clause. The "unique existence" unfolds as: there is a continuous $F'$ with properties 1–3, and for every continuous $G : I \times I \to E$ that satisfies all three of properties 1–3 (with $e_0$ the same fixed point, and with $G(1,\cdot)$ constant at some possibly different point $e_1'$ ), one has $G = F'$ as continuous maps (equivalently, $G(s,t) = F'(s,t)$ for all $(s,t)$ ). Uniqueness is therefore asserted only among maps that lift $F$ and are constantly $e_0$ on the whole edge $\{0\} \times I$ and are constant on the whole edge $\{1\} \times I$ ; it is not asserted among all lifts of $F$ , nor among lifts that merely agree with $e_0$ at the single corner $(0,0)$ , nor among lifts of the bottom path $s \mapsto F(s,0)$ alone.

Human review

Endorsed by Shuze Chen · Sep 5, 2026
Endorsed by korbonits · Sep 5, 2026
Confirmed by the mission captain (proposal self-audit).

View graph