Proposition 1.33 (lifting criterion): $f$ lifts iff $f_*\pi_1(Y,y_0)\subseteq p_*\pi_1(\tilde X,\tilde x_0)$

Read-back of Hatcher.lifting_criterion.

theorem lifting_criterion {E X Y : Type*} [TopologicalSpace E] [TopologicalSpace X]
    [TopologicalSpace Y] [PathConnectedSpace Y] [LocallyPathConnectedSpace Y]
    {p : E → X} (hp : IsCoveringMap p) {e₀ : E} {x₀ : X} (he : p e₀ = x₀)
    (f : C(Y, X)) {y₀ : Y} (hf : f y₀ = x₀) :
    (∃ F : C(Y, E), p ∘ F = f ∧ F y₀ = e₀) ↔
      (FundamentalGroup.mapOfEq f hf).range ≤ coverSubgroup p hp.continuous he

Setting and binders

• E X Y : Type* — three types in three independent universes.
• [TopologicalSpace E] [TopologicalSpace X] [TopologicalSpace Y] — arbitrary topologies. No connectedness or local connectedness is assumed on $E$ or $X$.
• [PathConnectedSpace Y] — $Y$ is nonempty and any two points of $Y$ are joined by a continuous path (Joined x y := Nonempty (Path x y)).
• [LocallyPathConnectedSpace Y] — Mathlib's class: ∀ y, (𝓝 y).HasBasis (fun s => s ∈ 𝓝 y ∧ IsPathConnected s) id. Unfolded: for every $y\in Y$ and every neighbourhood $N$ of $y$ there is a set $s\subseteq N$ which is itself a neighbourhood of $y$ (contains an open set containing $y$; $s$ need not be open) and is path-connected. IsPathConnected s := ∃ x ∈ s, ∀ y ∈ s, JoinedIn s x y, where JoinedIn s x y := ∃ γ : Path x y, ∀ t, γ t ∈ s — so $s$ is nonempty and any two points of $s$ are joined by a path inside $s$. This is Hatcher's "locally path-connected".
• {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 $p^{-1}(U)\cong U\times p^{-1}(x)$ over $U$. Fibres may be empty (no surjectivity). hp.continuous : Continuous p.
• {e₀ : E} {x₀ : X}, he : p e₀ = x₀ — basepoints, $p(e_0)=x_0$.
• f : C(Y, X) — a bundled continuous map $f : Y\to X$ (ContinuousMap). It is coerced to a function where needed.
• {y₀ : Y}, hf : f y₀ = x₀ — basepoint of $Y$ mapped to $x_0$.

Definitions from the bundle / Mathlib appearing in the conclusion:

• FundamentalGroup.mapOfEq f hf : FundamentalGroup Y y₀ →* FundamentalGroup X x₀ is $f_*:\pi_1(Y,y_0)\to\pi_1(X,x_0)$ (push-forward of loop classes along $f$, then transport along the equality $f(y_0)=x_0$).
• (…).range : Subgroup (FundamentalGroup X x₀) — the image subgroup $f_*\pi_1(Y,y_0)$.
• coverSubgroup p hp.continuous he = (FundamentalGroup.mapOfEq ⟨p, hp.continuous⟩ he).range — the image subgroup $p_*\pi_1(E,e_0)\le\pi_1(X,x_0)$.
• ≤ on Subgroup is inclusion of underlying sets.

Hypotheses

1. $Y$ is a nonempty, path-connected, locally path-connected space.
2. $p:E\to X$ is a covering map (Mathlib sense); $p(e_0)=x_0$.
3. $f:Y\to X$ is continuous with $f(y_0)=x_0$.

Conclusion

An if-and-only-if:

Left side. ∃ F : C(Y, E), p ∘ F = f ∧ F y₀ = e₀: there exists a continuous map $\tilde f : Y\to E$ with $p\circ\tilde f = f$ (equality of functions $Y\to X$, i.e. $p(\tilde f(y)) = f(y)$ for all $y$) and $\tilde f(y_0)=e_0$. That is, a lift of $f$ through $p$ sending $y_0$ to $e_0$ exists.

Right side. (mapOfEq f hf).range ≤ coverSubgroup p hp.continuous he:

So the theorem asserts: a based lift $\tilde f:(Y,y_0)\to(E,e_0)$ of $f$ exists iff $f_*\pi_1(Y,y_0)\subseteq p_*\pi_1(E,e_0)$.

Remarks

• Match with Hatcher Prop. 1.33. Hatcher: "Suppose given a covering space $p:(\tilde X,\tilde x_0)\to(X,x_0)$ and a map $f:(Y,y_0)\to(X,x_0)$ with $Y$ path-connected and locally path-connected. Then a lift $\tilde f:(Y,y_0)\to(\tilde X,\tilde x_0)$ of $f$ exists iff $f_*(\pi_1(Y,y_0))\subset p_*(\pi_1(\tilde X,\tilde x_0))$." The Lean statement has exactly these hypotheses and conclusion. Hatcher makes no connectedness assumption on $\tilde X$ or $X$, and neither does the Lean.
• Direction-by-direction. The forward implication (lift exists ⟹ inclusion) is pure functoriality, $f_* = p_*\circ\tilde f_*$, and needs none of the hypotheses on $Y$. The reverse implication is where path-connectedness (to define the lift via paths from $y_0$) and local path-connectedness (for continuity of the lift) of $Y$ are used. The statement bundles both into one iff, so as stated it requires the $Y$-hypotheses for the whole biconditional.
• Uniqueness is not asserted. The left side is a bare existential; nothing says the lift is unique (that is a separate theorem, unique_lifting).
• Surjectivity of $p$ is not assumed. Mathlib's IsCoveringMap allows empty fibres. This is harmless here: the fibre over $x_0$ contains $e_0$, and the lift constructed in the reverse direction only ever lands in the path-component of $e_0$. Also, nothing forces $E$ to be path-connected; coverSubgroup is just the image of the basepoint component's $\pi_1$.
• Degenerate instances. If $Y$ is a one-point space, both sides are true (constant lift at $e_0$; trivial group is contained in anything), so no contradiction. If $E$ is simply connected the right side says $f_*$ is trivial, recovering "maps from $Y$ lift to the universal cover iff they kill $\pi_1$".
• p ∘ F = f. Here F and f are coerced to functions; the equation is p ∘ ⇑F = ⇑f, i.e. pointwise equality for all y : Y. It is not an equality in C(Y, X), but the two are equivalent by extensionality.
• Neighbourhoods in LocallyPathConnectedSpace need not be open. Mathlib's basis condition allows non-open path-connected neighbourhoods; this is equivalent to the usual definition (Mathlib proves an open-basis version), so no gap versus the textbook.
• Universes. $E, X, Y$ may be in different universes; the conclusion mentions only Props and subgroups, so there is no universe constraint of note.
• Nothing is vacuous: the hypotheses are satisfiable (e.g. $Y$ a manifold, $p$ any covering) and both sides are genuine conditions.