Homotopy lifting property (c) for covering spaces

Read-back of Hatcher.homotopy_lifting_property.

The statement is universally quantified over three arbitrary topological spaces $E$, $X$, $Y$ (each may live in its own universe; no separation, connectedness, local connectedness, compactness, or nonemptiness assumptions are made on any of them), together with an arbitrary function $p : E \to X$ and the following data and hypotheses:

• Hypothesis on $p$. $p$ is a covering map in Mathlib's sense: for every point $x \in X$, the point $x$ is "evenly covered" by $p$ with fibre $p^{-1}(\{x\})$. Unfolded, this means that for every $x \in X$: the subspace $p^{-1}(\{x\}) \subseteq E$ carries the discrete topology, and there exists an open set $U \subseteq X$ with $x \in U$ such that $p^{-1}(U)$ is open in $E$ and there is a homeomorphism

whose first coordinate agrees with $p$, i.e. $\operatorname{pr}_1(H(e)) = p(e)$ for all $e \in p^{-1}(U)$. Note what this does not include: $p$ is not assumed surjective (a fibre $p^{-1}(\{x\})$ may be empty, in which case the condition just says $x$ has an open neighbourhood disjoint from $p(E)$); the fibres over different points need not be homeomorphic to one another; continuity of $p$ is not a separate hypothesis (it is a consequence of the definition). The covering-map hypothesis is the only assumption on $p$.

• The map $F$. $F$ is a continuous map $F : Y \times I \to X$, where $I = [0,1] \subseteq \mathbb{R}$ is the closed unit interval with its subspace topology and $Y \times I$ carries the product topology. The order of the coordinates is fixed: the first coordinate is the point $y \in Y$, the second is the parameter $t \in [0,1]$, so $F$ is evaluated as $F(y,t)$.

• The map $F_0$. $F_0$ is a continuous map $F_0 : Y \to E$.

• Compatibility hypothesis. For every $y \in Y$,

Conclusion. There exists a unique continuous map $F' : Y \times I \to E$ such that both of the following hold:

1. $p \circ F' = F$ as functions $Y \times I \to X$, i.e. $p\big(F'(y,t)\big) = F(y,t)$ for all $y \in Y$ and all $t \in [0,1]$; and
2. $F'(y, 0) = F_0(y)$ for every $y \in Y$.

The uniqueness clause ranges exactly over continuous maps $Y \times I \to E$: it asserts that if $G : Y \times I \to E$ is any continuous map satisfying $p \circ G = F$ and $G(y,0) = F_0(y)$ for all $y$, then $G = F'$ (equality of continuous maps, i.e. $G(y,t) = F'(y,t)$ for all $(y,t)$). Nothing is asserted about non-continuous functions $Y \times I \to E$ satisfying the two conditions, and no property of $F'$ beyond continuity and conditions 1–2 is claimed (in particular nothing about how $F'$ depends on the data).

Degenerate cases silently included. If $Y$ is empty, the hypotheses hold vacuously and the conclusion asserts the existence and uniqueness of the (unique) map from the empty space, so the statement is trivially true in that case. If $E$ is empty, then $p$ is automatically a covering map for any $X$, and the existence of $F_0 : Y \to E$ forces $Y$ to be empty. If $X$ is a single point, or $p$ is a homeomorphism, the statement is still asserted with the same content. No hypothesis excludes $p$ from having empty fibres over points of $X$ that are hit by $F$; the theorem asserts the conclusion for all such situations regardless.

This declaration does not use any of the custom definitions from the bundle (circleCover, omegaLoopN, omegaLoop, omegaClass); it refers only to Mathlib notions.