Proposition 1.36: every subgroup $H\le\pi_1(X,x_0)$ is $p_*\pi_1(X_H,\tilde x_0)$ for some covering space

Read-back of Hatcher.exists_cover_of_subgroup.

Setting and binders

• X : Type u — a type in a fixed (arbitrary) universe u.
• [TopologicalSpace X] — a topology on X.
• [PathConnectedSpace X] — Mathlib's class: X is nonempty and any two points x y : X are Joined, i.e. there exists a continuous path Path x y (a continuous map from the unit interval I = [0,1] with γ 0 = x, γ 1 = y). So this instance silently supplies Nonempty X.
• [LocallyPathConnectedSpace X] — Mathlib's class: for every x, the neighbourhood filter 𝓝 x has a basis consisting of sets s with s ∈ 𝓝 x and IsPathConnected s (nonempty, and any two of its points joined by a path inside s). This is the standard "locally path-connected" (neighbourhoods in the basis need not be open).
• hX : IsSemilocallySimplyConnected X — the bundle's definition:

$$\forall x \in X,\ \exists U \in \mathcal N(x),\ \forall \gamma : \mathrm{Path}\,x\,x,\ \big(\forall t,\ \gamma(t) \in U\big) \to \gamma \simeq \mathrm{refl}_x .$$

Here U ∈ nhds x means U contains an open set containing x (not necessarily open itself); γ.Homotopic (Path.refl x) is Nonempty (γ.Homotopy (refl x)), a homotopy of paths relative to endpoints (Mathlib's Path.Homotopy is ContinuousMap.HomotopyRel … {0,1}), taking place in all of X. So: every point has a neighbourhood U such that every loop at x lying in U is null-homotopic in X, i.e. $\pi_1(U,x)\to\pi_1(X,x)$ is trivial. This is Hatcher's definition of semilocally simply-connected.

• x₀ : X — a basepoint, explicit.
• H : Subgroup (FundamentalGroup X x₀) — an arbitrary subgroup of $\pi_1(X,x_0)$. Mathlib's FundamentalGroup X x₀ is End (FundamentalGroupoid.mk x₀), the group of homotopy classes (rel endpoints) of loops at x₀; its multiplication is p * q = q.trans p (i.e. p * q traverses q first, then p; the opposite of Hatcher's concatenation-order convention). This does not affect which subsets are subgroups.

Hypotheses

Exactly the instance hypotheses above plus hX. Nothing else: no Hausdorffness, no compactness, no second-countability, no assumption on H (it may be ⊥, ⊤, non-normal, infinite index, etc.).

Conclusion

$$\exists\, C : \texttt{PointedCover } X\ x_0,\quad \texttt{PathConnectedSpace } C.E\ \wedge\ C.\texttt{subgroup} = H .$$

Unpacking PointedCover X x₀ (from the bundle): a structure consisting of

• E : Type u — a total space in the same universe u as X;
• [topE : TopologicalSpace E] — a topology on E (made an instance);
• p : E → X — a function;
• isCoveringMap : IsCoveringMap p — Mathlib's covering-map predicate: for every x : X, IsEvenlyCovered p x (p⁻¹{x}), i.e. the fibre p⁻¹{x} (as a subtype) carries the discrete topology and there is a set U ⊆ X with x ∈ U, U open, p⁻¹(U) open, and a homeomorphism Hom : p⁻¹(U) ≃ₜ U × p⁻¹{x} whose first coordinate is p. Mathlib's docstring explicitly notes: p is not assumed surjective; fibres may be empty; E may be empty. IsCoveringMap.continuous derives Continuous p.
• e₀ : E — a point of E;
• p_e₀ : p e₀ = x₀ — it lies over x₀.

PathConnectedSpace C.E — the total space E is nonempty and path-connected.

C.subgroup is coverSubgroup C.p C.isCoveringMap.continuous C.p_e₀, which is (coverHom …).range, where coverHom p hp he = FundamentalGroup.mapOfEq ⟨p, hp⟩ he. By Mathlib's mapOfEq_apply, mapOfEq f h [γ] = ([f ∘ γ]).cast h.symm h.symm: push the loop γ at e₀ forward to the loop p ∘ γ at p e₀, and re-index the endpoints to x₀ via the equality p e₀ = x₀. So coverHom is exactly the induced homomorphism $p_* : \pi_1(E,e_0)\to\pi_1(X,x_0)$ and C.subgroup is its image

$$C.\texttt{subgroup} = p_*\big(\pi_1(E,e_0)\big) = \{[p\circ\gamma] : \gamma \text{ a loop at } e_0\}\ \le\ \pi_1(X,x_0).$$

So the theorem asserts, in words: for a path-connected, locally path-connected, semilocally simply-connected space $X$ with basepoint $x_0$ and any subgroup $H\le\pi_1(X,x_0)$, there exists a covering map $p:E\to X$ with $E$ path-connected (and living in universe u) and a point $e_0\in p^{-1}(x_0)$ such that $p_*\pi_1(E,e_0)=H$.

This is the existence half of Hatcher, Proposition 1.36 (and the surjectivity half of Theorem 1.38).

Remarks

1. Not vacuous, not trivial. The hypotheses are satisfiable (e.g. $X=S^1$, or any connected manifold or CW complex), and the conclusion for H = ⊥ is existence of a simply-connected (universal) cover, for H = ⊤ it is satisfied by E = X, p = id. The conjunct PathConnectedSpace C.E is what makes the statement non-trivial for intermediate H: without it one could not obviously cheat either (a disconnected E with e₀ in a component E' has C.subgroup = p_*\pi_1(E',e_0), so nothing is gained), but the theorem does not rely on that; it demands path-connectedness outright, as the textbook does.
2. Universe. E : Type u is forced to share X's universe. Since the statement is existential, this restriction only makes it (formally) stronger than "there exists a covering in some universe"; Hatcher's construction ($E$ = a quotient of the set of paths in $X$ from $x_0$) lives in Type u anyway, so nothing is lost.
3. Surjectivity of p. Not stated, but automatic here: E is nonempty, X is connected, and for a covering map in Mathlib's sense the set of x with nonempty fibre is open and so is its complement (fibres over an evenly-covered U are all homeomorphic to p⁻¹{x}); hence p is onto.
4. Basepoint dependence. The subgroup is attached to the pair (E, e₀); the theorem only asserts that some basepoint in the fibre works, exactly as in Hatcher ("for a suitably chosen basepoint").
5. No uniqueness. Nothing about uniqueness up to isomorphism is asserted here; that is isPointedIsomorphic_iff.
6. Semilocal simple connectivity is stated via arbitrary (not necessarily open) neighbourhoods U ∈ 𝓝 x. Since any such U contains an open neighbourhood, and loops in the smaller set are loops in U, this is equivalent to the open-neighbourhood version. Only loops based at x are constrained, matching Hatcher's $\pi_1(U,x)\to\pi_1(X,x)$ trivial.
7. Group-law convention. Mathlib's product on FundamentalGroup is reversed relative to Hatcher's; the set of subgroups is identical, so H ranges over exactly the textbook's subgroups.
8. Nothing a textbook would include is missing except the customary remark that $E$ is then also locally path-connected (which is not stated but is not part of Hatcher's Prop. 1.36 either).