Necessity of semilocal simple connectivity: a space with a simply-connected covering space is semilocally simply-connected

Read-back of Hatcher.isSemilocallySimplyConnected_of_cover.

theorem isSemilocallySimplyConnected_of_cover {E X : Type*} [TopologicalSpace E]
    [TopologicalSpace X] [SimplyConnectedSpace E] {p : E → X} (hp : IsCoveringMap p)
    (hsurj : Function.Surjective p) : IsSemilocallySimplyConnected X

Setting and binders

• E X : Type* — two types, independent universes.
• [TopologicalSpace E] [TopologicalSpace X] — arbitrary topologies. No connectedness, path-connectedness, or local path-connectedness is assumed on $X$.
• [SimplyConnectedSpace E] — Mathlib's class with single field equiv_unit : Nonempty (FundamentalGroupoid E ≌ Discrete Unit): the fundamental groupoid of $E$ is equivalent (as a category) to the one-object, one-morphism category. Mathlib proves this is equivalent to: $E$ is nonempty and for all $x,y\in E$ the set of homotopy-rel-endpoints classes of paths from $x$ to $y$ is a singleton (simply_connected_iff_unique_homotopic), equivalently $E$ is path-connected and any two paths with the same endpoints are homotopic rel endpoints (simply_connected_iff_paths_homotopic'). In particular SimplyConnectedSpace E provides an instance PathConnectedSpace E (so $E\ne\emptyset$) and every loop in $E$ is null-homotopic.
• {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)\simeq_t U\times p^{-1}(x)$ commuting with the projection to $U$. Mathlib does not build surjectivity into IsCoveringMap — fibres may be empty.
• hsurj : Function.Surjective p — ∀ x : X, ∃ e : E, p e = x. This is the explicit surjectivity that Mathlib's covering-map notion lacks.

The conclusion uses the bundle's definition:

• IsSemilocallySimplyConnected X : Prop := ∀ x : X, ∃ U ∈ nhds x, ∀ γ : Path x x, (∀ t, γ t ∈ U) → γ.Homotopic (Path.refl x).

  Unpacked:

  • U ∈ nhds x — $U$ is a neighbourhood of $x$ in Mathlib's sense: there is an open $V$ with $x\in V\subseteq U$. $U$ itself need not be open.
  • γ : Path x x — a continuous map $\gamma:[0,1]\to X$ (unitInterval) with $\gamma(0)=\gamma(1)=x$, i.e. a loop based at $x$.
  • ∀ t, γ t ∈ U — the loop lies entirely inside $U$.
  • γ.Homotopic (Path.refl x) — Path.Homotopic p₀ p₁ := Nonempty (p₀.Homotopy p₁), and Path.Homotopy is ContinuousMap.HomotopyRel _ _ {0, 1}: a homotopy $[0,1]\times[0,1]\to X$ in $X$ (not required to stay in $U$) fixing both endpoints, from $\gamma$ to the constant loop at $x$.

  So IsSemilocallySimplyConnected X says: every $x\in X$ has a neighbourhood $U$ such that every loop at $x$ contained in $U$ is null-homotopic (rel basepoint) in $X$; equivalently, the inclusion-induced map $\pi_1(U,x)\to\pi_1(X,x)$ is trivial.

Hypotheses

1. $E$ is simply connected (hence nonempty and path-connected, with trivial $\pi_1$ at every point).
2. $p:E\to X$ is a covering map (Mathlib sense).
3. $p$ is surjective.

Conclusion

$X$ is semilocally simply connected in the bundle's sense:

Remarks

• Match with Hatcher. Hatcher (§1.3, discussion before Prop. 1.36) states: "if $X$ has a simply-connected covering space then $X$ is semilocally simply-connected", with his definition "each point $x\in X$ has a neighborhood $U$ such that the inclusion-induced map $\pi_1(U,x)\to\pi_1(X,x)$ is trivial." The bundle's IsSemilocallySimplyConnected is literally this (loops at $x$ inside $U$ are trivial in $\pi_1(X,x)$). Some texts instead require $\pi_1(U,y)\to\pi_1(X,y)$ trivial for all $y\in U$; the Lean definition only asks it at the given basepoint $x$, matching Hatcher's wording rather than that stronger variant.
• Why hsurj is present. In Hatcher, covering spaces are surjective by convention (or implicitly via connectedness). In Mathlib a covering map can have empty fibres, and over a point with empty fibre the conclusion could fail (there is no lift to exploit). Hence the explicit surjectivity hypothesis is a genuine, needed hypothesis and not a stylistic addition. It also forces $X\neq\emptyset$ (since $E\ne\emptyset$); conversely, if $X$ were empty, $E$ would be empty too, contradicting SimplyConnectedSpace E, so the empty case does not arise.
• No connectedness of $X$ is required, and the statement is still true as stated. For $x\in X$ take the evenly covered open $U$ and a point $e\in p^{-1}(x)$ (exists by hsurj); a loop $\gamma$ in $U$ at $x$ lifts to the slice $U\times\{e\}$ as a loop $\tilde\gamma$ at $e$; $\tilde\gamma$ is null-homotopic since $E$ is simply connected; pushing the homotopy down by $p$ null-homotopes $\gamma$. So the statement is neither vacuous nor over-hypothesised; it is somewhat more general than the textbook context (which has $X$ path-connected and locally path-connected).
• The neighbourhood $U$ is not required to be open, but since nhds-membership implies $U$ contains an open neighbourhood, and shrinking $U$ only weakens the loop condition, this is equivalent to the open version.
• Homotopies live in $X$, not $U$, exactly as in the textbook notion ("trivial in $\pi_1(X,x)$"). If the homotopy were required inside $U$ this would be "locally simply connected", a strictly stronger property; that is not what is stated.
• Nothing about local path-connectedness is asserted or assumed; the conclusion is only the semilocal simple-connectivity property.
• Universes. $E$ and $X$ in independent universes; the conclusion is a Prop, so no universe constraint.
• Vacuity check. SimplyConnectedSpace E is satisfiable (e.g. $E=\mathbb R$), and $p:\mathbb R\to S^1$ is a surjective covering; the conclusion for $S^1$ is a true, non-trivial statement. Nothing collapses.