Existence of the universal cover: a path-connected, locally path-connected, semilocally simply-connected space has a simply-connected covering space

Read-back of Hatcher.exists_simplyConnected_cover.

universe u

theorem exists_simplyConnected_cover {X : Type u} [TopologicalSpace X] [PathConnectedSpace X]
    [LocallyPathConnectedSpace X] (hX : IsSemilocallySimplyConnected X) :
    ∃ C : CoveringSpace X, SimplyConnectedSpace C.E

Setting and binders

• X : Type u — a type in an explicitly named universe u (not Type*). This matters because CoveringSpace X (below) forces the total space to live in the same universe u.
• [TopologicalSpace X] — an arbitrary topology.
• [PathConnectedSpace X] — Mathlib: nonempty : Nonempty X and joined : ∀ x y, Joined x y (Joined x y := Nonempty (Path x y)). So $X$ is nonempty and any two points are joined by a continuous path.
• [LocallyPathConnectedSpace X] — Mathlib: ∀ x, (𝓝 x).HasBasis (fun s => s ∈ 𝓝 x ∧ IsPathConnected s) id. For every $x$ and every neighbourhood $N$ of $x$, there is a (not necessarily open) neighbourhood $s\subseteq N$ of $x$ that is path-connected (IsPathConnected s := ∃ a ∈ s, ∀ b ∈ s, JoinedIn s a b, i.e. nonempty and any two points joined by a path inside $s$). This is the standard "locally path-connected".
• hX : IsSemilocallySimplyConnected X — the bundle's definition: ∀ x : X, ∃ U ∈ nhds x, ∀ γ : Path x x, (∀ t, γ t ∈ U) → γ.Homotopic (Path.refl x). Every $x$ has a neighbourhood $U$ (U ∈ nhds x: contains an open set containing $x$; $U$ itself need not be open) such that every loop $\gamma:[0,1]\to X$ based at $x$ with image in $U$ is homotopic rel endpoints, in $X$ (Path.Homotopic = HomotopyRel … {0,1}), to the constant loop Path.refl x. I.e. $\pi_1(U,x)\to\pi_1(X,x)$ is trivial.

The conclusion uses the bundle's CoveringSpace X (declared in a section where X : Type u):

structure CoveringSpace where
    E : Type u
  [topE : TopologicalSpace E]
    p : E → X
  isCoveringMap : IsCoveringMap p

So a CoveringSpace X is a quadruple: a type E in the same universe u as X, a topology on E (registered as an instance via attribute [instance] CoveringSpace.topE), a function p : E → X, and a proof that p is a covering map in Mathlib's sense — every $x\in X$ has an open neighbourhood $U$ with $p^{-1}(U)$ open and a homeomorphism $p^{-1}(U)\simeq_t U\times p^{-1}(x)$ over $U$, with $p^{-1}(x)$ discrete. Surjectivity of p is not part of CoveringSpace (Mathlib allows empty fibres).

SimplyConnectedSpace C.E — Mathlib: Nonempty (FundamentalGroupoid C.E ≌ Discrete Unit), equivalently $E$ is nonempty, path-connected, and any two paths in $E$ with the same endpoints are homotopic rel endpoints (in particular $\pi_1(E,e)=1$ for every $e$).

Hypotheses

1. $X$ is a nonempty, path-connected topological space.
2. $X$ is locally path-connected.
3. $X$ is semilocally simply connected (every point has a neighbourhood in which loops at that point are null-homotopic in $X$).

Conclusion

In words: there exists a topological space $E$ (in the same universe as $X$) and a covering map $p:E\to X$ such that $E$ is simply connected. This is the existence of a universal cover.

Remarks

• Match with Hatcher Prop. 1.36 (existence half). Hatcher: "Suppose $X$ is path-connected, locally path-connected, and semilocally simply-connected. Then $X$ has a simply-connected covering space." The hypotheses and conclusion coincide with the Lean statement. Hatcher's Prop. 1.36 continues with the classification of connected covers by subgroups; that part is not in this statement — only the existence of one simply-connected cover is asserted.
• No uniqueness / universality is claimed. The statement does not say the cover is unique up to isomorphism, nor that it covers every other connected cover (the "universal" property). IsIsomorphic / IsPointedIsomorphic from the bundle are not mentioned.
• Surjectivity of p follows but is not stated. SimplyConnectedSpace C.E forces $E\ne\emptyset$; a Mathlib covering map is open and the set of points with empty fibre is open, so $p(E)$ is clopen and nonempty in the connected space $X$, hence $p$ is onto. So the missing surjectivity in CoveringSpace does not weaken the theorem here. In particular the "cheap" witness with $E=\emptyset$ (which is a Mathlib covering map of anything, IsCoveringMapOn.of_isEmpty) is ruled out because the empty space is not simply connected.
• Trivialisation check. One could try E := X, p := id (the identity is a covering map). That witness works only if $X$ is already simply connected, so the theorem is not trivially satisfiable in general (e.g. $X=S^1$ needs $E=\mathbb R$). The statement is non-trivial and non-vacuous: the hypotheses are met by every connected manifold and CW complex.
• Universe constraint. Because CoveringSpace X fixes E : Type u, the theorem asserts existence of a universal cover in the same universe as $X$. Hatcher's construction ($E$ = homotopy classes of paths from a basepoint, a quotient of a subtype of Path-like data in Type u) lives in Type u, so this is not a real restriction, but a reader should note that a proof cannot escape to a higher universe.
• LocallyPathConnectedSpace neighbourhoods need not be open, and U in IsSemilocallySimplyConnected need not be open either; both are equivalent to their open-neighbourhood versions, so there is no discrepancy with textbook definitions.
• Homotopies in IsSemilocallySimplyConnected are taken in $X$, not in $U$, exactly as Hatcher's "inclusion-induced map $\pi_1(U,x)\to\pi_1(X,x)$ is trivial"; the stronger "locally simply connected" is not what is assumed, so the hypothesis is the correct (weaker) one.
• The topology on E is bundled as a structure field topE, not a separate typeclass parameter; SimplyConnectedSpace C.E uses that instance.
• Nothing is said about the fibres' cardinality, deck transformations, or IsNormalCover, even though those definitions exist in the bundle.