Path lifting property (a) for covering spaces

Declaration Hatcher.path_lifting_property. This theorem uses none of the custom definitions from the accompanying bundle (circleCover, omegaLoop, omegaLoopN, omegaClass do not occur in it); every notion it uses is from Mathlib or Lean core, and the non-universal ones are unfolded below.

Data and hypotheses. Let $E$ and $X$ be arbitrary topological spaces (no separation, connectedness, path-connectedness, local path-connectedness, or nonemptiness assumption is placed on either). Let $p : E \to X$ be a function, and assume

which in Mathlib means literally the following: for every point $x \in X$, the point $x$ is evenly covered by $p$ with fibre $p^{-1}(\{x\})$, i.e.

• the fibre $p^{-1}(\{x\}) \subseteq E$, with its subspace topology, is a discrete space (its topology is the discrete one), and
• there exists a subset $U \subseteq X$ with $x \in U$, $U$ open in $X$, $p^{-1}(U)$ open in $E$, and a homeomorphism $H : p^{-1}(U) \to U \times p^{-1}(\{x\})$ (the product carrying the product topology, $U$ and $p^{-1}(U)$ the subspace topologies) such that for every $y \in p^{-1}(U)$ the first coordinate of $H(y)$ is $p(y)$.

Note what this does and does not say: $p$ is not assumed surjective, so fibres $p^{-1}(\{x\})$ may be empty (the empty space is discrete, and $U \times \varnothing = \varnothing$ is homeomorphic to $p^{-1}(U) = \varnothing$, so points outside the image of $p$ can satisfy the condition); the fibres over different points are not required to be homeomorphic to one another; and no separate continuity hypothesis on $p$ is stated — the only hypothesis on $p$ is the evenly-covered condition just spelled out.

Let $I = [0,1] = \{ t \in \mathbb{R} : 0 \le t \le 1 \}$ with the subspace topology from $\mathbb{R}$, and let

be a continuous map (an element of $C(I,X)$, Mathlib's type of continuous maps, whose elements are equal exactly when their underlying functions agree pointwise). Let $e_0 \in E$ be a point, and assume

where $0$ denotes the left endpoint $0 \in [0,1]$. (Since $e_0$ is a point of $E$, the hypotheses force $E \neq \varnothing$; since $f(0) \in X$, also $X \neq \varnothing$.)

Conclusion. There exists a unique continuous map $f' : I \to E$ (unique as an element of $C(I,E)$) such that both

and

The "exists unique" here is Lean's $\exists!$, which unfolds to: there is a continuous $f' : I \to E$ with $p \circ f' = f$ and $f'(0) = e_0$, and for every continuous $g : I \to E$ with $p \circ g = f$ and $g(0) = e_0$ one has $g = f'$ (pointwise equality on all of $[0,1]$). Thus the uniqueness clause ranges over all continuous maps $[0,1] \to E$ satisfying both the lifting equation and the initial condition; it says nothing about non-continuous functions, about maps agreeing with $f$ only on part of $[0,1]$, or about maps with a different starting point.

Degenerate cases silently included. The statement is asserted for every covering map $p$ in the above sense, including ones with empty fibres over some points of $X$ (e.g. $p$ not surjective) — the theorem then still claims a continuous lift of $f$ exists through $e_0$, with $p(f'(t)) = f(t)$ for every $t \in [0,1]$, including any $t$ for which $f(t)$ might lie outside the image of $p$. It is also asserted for constant paths $f$, for $E = X$ with $p = \mathrm{id}$, and for arbitrary (e.g. non-Hausdorff, disconnected) $E$ and $X$. No hypothesis in the statement is impossible to satisfy: the identity map of any nonempty space, together with the constant path and $e_0 = f(0)$, satisfies all of them.