Proposition 1.34 (unique lifting): two lifts agreeing at one point agree everywhere

Read-back of Hatcher.unique_lifting.

theorem unique_lifting {E X Y : Type*} [TopologicalSpace E] [TopologicalSpace X]
    [TopologicalSpace Y] [ConnectedSpace Y]
    {p : E → X} (hp : IsCoveringMap p) (f : C(Y, X)) (F₁ F₂ : C(Y, E))
    (h₁ : p ∘ F₁ = f) (h₂ : p ∘ F₂ = f) (y : Y) (hy : F₁ y = F₂ y) : F₁ = F₂

Setting and binders

• E X Y : Type* — three types, independent universes.
• [TopologicalSpace E] [TopologicalSpace X] [TopologicalSpace Y] — arbitrary topologies on all three. No hypotheses at all on $E$ or $X$ beyond what IsCoveringMap supplies.
• [ConnectedSpace Y] — Mathlib's class ConnectedSpace Y extends PreconnectedSpace Y with an extra field toNonempty : Nonempty Y. PreconnectedSpace Y says IsPreconnected (Set.univ : Set Y): there are no two open sets $U,V$ with $U\cup V = Y$, $U\cap Y\neq\emptyset$, $V\cap Y\ne\emptyset$ and $U\cap V\cap Y=\emptyset$. So $Y$ is connected in the usual sense and nonempty. (Path-connectedness is not assumed; only connectedness.)
• {p : E → X}, hp : IsCoveringMap p — Mathlib covering map: for every $x\in X$, the fibre $p^{-1}(x)$ is discrete and there is an open $U\ni x$ with $p^{-1}(U)$ open and a homeomorphism $H:p^{-1}(U)\simeq_t U\times p^{-1}(x)$ with $\pi_1\circ H = p$. Fibres may be empty; $p$ need not be surjective. IsCoveringMap implies p is a local homeomorphism (Mathlib: IsCoveringMap.isLocalHomeomorph).
• f : C(Y, X) — a bundled continuous map $f:Y\to X$.
• F₁ F₂ : C(Y, E) — two bundled continuous maps $\tilde f_1,\tilde f_2 : Y\to E$.
• h₁ : p ∘ F₁ = f, h₂ : p ∘ F₂ = f — equalities of functions $Y\to X$ (the C(·,·) terms are coerced): $p(\tilde f_i(y)) = f(y)$ for all $y$. So both $\tilde f_1,\tilde f_2$ are lifts of $f$ through $p$.
• y : Y, hy : F₁ y = F₂ y — one point at which the two lifts agree.

Hypotheses

1. $Y$ is a nonempty connected topological space.
2. $p:E\to X$ is a covering map (Mathlib sense).
3. $\tilde f_1,\tilde f_2:Y\to E$ are continuous with $p\circ\tilde f_1 = f = p\circ\tilde f_2$.
4. $\tilde f_1(y)=\tilde f_2(y)$ for at least one point $y\in Y$.

Conclusion

F₁ = F₂ — equality in the type C(Y, E) of bundled continuous maps. By extensionality this is equivalent to $\tilde f_1(z)=\tilde f_2(z)$ for all $z\in Y$.

In words: two lifts of the same map $f:Y\to X$ through a covering map $p$ that agree at a single point of the connected space $Y$ agree everywhere.

Remarks

• Match with Hatcher Prop. 1.34 (unique lifting property). Hatcher: "Given a covering space $p:\tilde X\to X$ and a map $f:Y\to X$, if two lifts $\tilde f_1,\tilde f_2:Y\to\tilde X$ of $f$ agree at one point of $Y$ and $Y$ is connected, then $\tilde f_1$ and $\tilde f_2$ agree on all of $Y$." The Lean statement is a faithful transcription: connectedness of $Y$ (not path-connectedness), no assumptions on $\tilde X$ or $X$, agreement at one point.
• The parameter f is redundant. The hypotheses h₁, h₂ together only say $p\circ\tilde f_1 = p\circ\tilde f_2$; f simply names the common composite. The theorem is neither weaker nor stronger than the version without f, since any two lifts of the same f satisfy $p\circ F_1=p\circ F_2$ and conversely one can take f := ⟨p ∘ F₁, …⟩.
• Nonemptiness. ConnectedSpace Y includes Nonempty Y, but this is redundant here because the explicit point y : Y already witnesses nonemptiness. If $Y$ were allowed to be empty the conclusion would hold trivially anyway (there is only one map out of the empty space), so the nonemptiness is not what makes the theorem non-vacuous.
• Connectedness is used essentially. If $Y$ were disconnected (e.g. two points) and $p$ had a fibre with $\ge2$ points, one could choose lifts agreeing on one component and differing on another, so the statement would be false without [ConnectedSpace Y].
• Surjectivity of $p$ is not assumed and not needed. Points of $X$ with empty fibre cannot be in the image of $f$ (since $f = p\circ\tilde f_1$), so they play no role.
• Discreteness of fibres is the key property used (via IsCoveringMap): the set where the two lifts agree and the set where they disagree are both open, using the local trivialisation $p^{-1}(U)\cong U\times p^{-1}(x)$ with discrete fibre. Nothing weaker (e.g. merely a local homeomorphism) is assumed, though the textbook proof would go through with a local homeomorphism plus a Hausdorff-type condition; the Lean statement asks for a full covering map.
• Coercions. p ∘ F₁ is p ∘ ⇑F₁ : Y → X and f on the right is ⇑f. Equality is function equality, not equality in C(Y, X); the two are equivalent.
• Universes. All three types are in independent universes; the conclusion is an equality in C(Y, E), so nothing constrains the universes.
• There is no hidden trivialisation: the hypotheses are jointly satisfiable in non-trivial ways (e.g. $p:\mathbb R\to S^1$, $Y=[0,1]$, two lifts of a path), and the conclusion is the expected non-trivial uniqueness.