Theorem 1.38 (classification of covering spaces): path-connected covering spaces $\leftrightarrow$ subgroups of $\pi_1(X,x_0)$, up to conjugacy when basepoints are ignored

Read-back of Hatcher.classification_of_covering_spaces.

Setting and binders

• X : Type u, [TopologicalSpace X] — a topological space in a fixed universe u.
• [PathConnectedSpace X] — Mathlib's class: Nonempty X and any two points are joined by a continuous path Path x y (I → X, continuous, with prescribed endpoints).
• [LocallyPathConnectedSpace X] — for every x, the filter 𝓝 x has a basis of sets s with s ∈ 𝓝 x and IsPathConnected s (nonempty, any two points joined by a path inside s).
• hX : IsSemilocallySimplyConnected X — the bundle's definition: for every x there is a neighbourhood U ∈ 𝓝 x (not necessarily open) such that every loop γ : Path x x with ∀ t, γ t ∈ U is Path.Homotopic (homotopic rel endpoints, in X) to the constant loop Path.refl x. Equivalently, $\pi_1(U,x)\to\pi_1(X,x)$ is trivial. This is Hatcher's definition.
• x₀ : X — explicit basepoint.

Types from the bundle.

• CoveringSpace X: a structure with E : Type u (same universe as X), [topE : TopologicalSpace E], p : E → X, isCoveringMap : IsCoveringMap p. Mathlib's IsCoveringMap p: for every x : X, IsEvenlyCovered p x (p⁻¹{x}), i.e. the fibre p⁻¹{x} is discrete and there exist an open U ∋ x with p⁻¹(U) open and a homeomorphism p⁻¹(U) ≃ₜ U × p⁻¹{x} whose first component is p. Surjectivity is not required; fibres may be empty and E may be empty.
• PointedCover X x₀: a CoveringSpace X together with e₀ : E and p_e₀ : p e₀ = x₀.
• C.subgroup (for C : PointedCover X x₀) $= \operatorname{range}(\texttt{FundamentalGroup.mapOfEq}\,\langle C.p, \_\rangle\, C.p\_e₀)$. By mapOfEq_apply, the homomorphism sends a loop class [γ] at e₀ to [p ∘ γ] re-indexed as a loop at x₀ using p e₀ = x₀. So $C.\texttt{subgroup} = p_*\pi_1(E,e_0)\le \pi_1(X,x_0)$.
• coverSubgroup C.p C.isCoveringMap.continuous h for any e and h : C.p e = x₀ — the same thing, $p_*\pi_1(E,e)$, for an arbitrary point e of the fibre over x₀.
• IsPointedIsomorphic C₁ C₂ (for pointed covers): $\exists f : E_1\simeq_t E_2$ (Mathlib Homeomorph: bijection, continuous both ways) with $\forall e,\ p_2(f e) = p_1 e$ and $f(e_0^{(1)}) = e_0^{(2)}$.
• IsIsomorphic C₁ C₂ (for unpointed covers): $\exists f : E_1\simeq_t E_2$ with $\forall e,\ p_2(f e) = p_1 e$ — a homeomorphism over X, no basepoint condition.
• FundamentalGroup X x₀ is Mathlib's End (FundamentalGroupoid.mk x₀), homotopy classes of loops at x₀, with multiplication p * q = q.trans p (traverse q first, then p; reversed relative to Hatcher's concatenation order).
• H.map (MulAut.conj g).toMonoidHom: MulAut.conj g is h ↦ g * h * g⁻¹ (MulAut.conj_apply, definitional), Subgroup.map φ H has carrier φ '' H. So this is $\{g*h*g^{-1} : h\in H\} = gHg^{-1}$ in Mathlib's product, which equals $g^{-1}Hg$ in Hatcher's concatenation-order product. Wherever it appears below, g is existentially quantified over the whole group, so the convention does not alter the meaning.

Hypotheses

Exactly the four listed above: X path-connected, locally path-connected, semilocally simply-connected, plus a basepoint. No Hausdorff, no compactness, no CW structure. (Hatcher's Theorem 1.38 has precisely these hypotheses.)

Conclusion

A conjunction of three statements, (1) ∧ ((2) ∧ (3)).

(1) Existence (surjectivity onto subgroups).

$$\forall H\le\pi_1(X,x_0),\ \exists C : \texttt{PointedCover } X\ x_0,\quad E_C \text{ is path-connected}\ \wedge\ p_*\pi_1(E_C,e_0)=H.$$

Identical to exists_cover_of_subgroup: every subgroup is realised as $p_*\pi_1(E,e_0)$ for some path-connected pointed covering with total space in Type u.

(2) Pointed isomorphism ⇔ equal subgroups.

$$\forall C_1\,C_2 : \texttt{PointedCover } X\ x_0,\ \ E_1 \text{ path-conn.}\to E_2 \text{ path-conn.}\to\Big(\texttt{IsPointedIsomorphic } C_1\ C_2 \iff (p_1)_*\pi_1(E_1,e_0^{(1)}) = (p_2)_*\pi_1(E_2,e_0^{(2)})\Big).$$

Identical to isPointedIsomorphic_iff with the two path-connectedness assumptions written as implications: for path-connected pointed covers, there is a homeomorphism over X carrying basepoint to basepoint iff the two image subgroups coincide.

(3) Unpointed isomorphism ⇔ conjugate subgroups.

$$\forall C_1\,C_2 : \texttt{CoveringSpace } X,\ \ E_1 \text{ path-conn.}\to E_2 \text{ path-conn.}\to\Big(\texttt{IsIsomorphic } C_1\ C_2 \iff \exists\, e_1\in E_1,\ e_2\in E_2,\ (h_1 : p_1 e_1 = x_0),\ (h_2 : p_2 e_2 = x_0),\ g\in\pi_1(X,x_0):\ \ g\,\big[(p_1)_*\pi_1(E_1,e_1)\big]\,g^{-1} = (p_2)_*\pi_1(E_2,e_2)\Big).$$

In words: two path-connected (unpointed) covering spaces of X are isomorphic over X iff there exist basepoints $e_1, e_2$ in the fibres over $x_0$ whose image subgroups are conjugate in $\pi_1(X,x_0)$. Note the quantifier: some choice of basepoints, not every choice. (By coverSubgroup_conj, the set of subgroups obtained as $e_i$ varies in the fibre is a full conjugacy class, so "for some $e_1,e_2$ conjugate" is equivalent to "for all $e_1,e_2$ conjugate"; but that equivalence is not part of this statement.)

Remarks

Relation to Hatcher's Theorem 1.38 ("bijection" formulation). Hatcher states: (i) $(\tilde X,\tilde x_0)\mapsto p_*\pi_1(\tilde X,\tilde x_0)$ is a bijection from basepoint-preserving isomorphism classes of path-connected pointed covers to subgroups of $\pi_1(X,x_0)$; (ii) forgetting basepoints, a bijection from isomorphism classes of path-connected covers to conjugacy classes of subgroups. The Lean theorem never forms quotient sets or an Equiv; instead it gives the ingredients:

• Well-definedness of (i) on isomorphism classes: the "⇒" of (2).
• Injectivity of (i): the "⇐" of (2).
• Surjectivity of (i): (1).
• Well-definedness of (ii) (isomorphic covers have conjugate subgroups, for some/any basepoints): "⇒" of (3) (together with coverSubgroup_conj for the "any" version).
• Injectivity of (ii): "⇐" of (3).
• Surjectivity of (ii): not stated separately, but follows immediately from (1) by forgetting the basepoint (a subgroup $H$ in a given conjugacy class is realised as $p_*\pi_1(E,e_0)$, and the conjugacy class of that is the class of $H$). A reader checking against the textbook should be aware this is a one-line consequence, not an explicit conjunct.

So the three parts are logically equivalent to Hatcher's two bijections restricted to covers with E : Type u, with the (i)/(ii) correspondence spelled out as "iff" conditions rather than as a bijection between quotient sets. Nothing weaker is asserted at the level of content, but the theorem is not literally a Bijective or Equiv statement.

Universe restriction. Every cover quantified over has total space E : Type u, the same universe as X. Hence "all covering spaces" in (2) and (3) means "all covering spaces whose total space lives in Type u", and (1) produces one in Type u. For path-connected covers this loses nothing up to isomorphism: with e₀ fixed, each point of E is the endpoint of a unique lift of some path in X from x₀, so $|E|\le|\{\text{paths in }X\}|$, and any such cover is homeomorphic over X to one in Type u. But the theorem as stated does not say anything about a cover E : Type v, v ≠ u.

Non-vacuity, non-triviality. The hypotheses are satisfiable (circle, torus, any connected manifold). None of (1)–(3) is trivially true: (1) for H = ⊥ is existence of a universal cover; (2) "⇐" is Hatcher's Prop. 1.37; (3) "⇐" is the unpointed classification. The only automatically true pieces are the "⇒" directions of (2) and (3), which are standard functoriality (in (3), given the iso f take any e₁, e₂ := f e₁, g := 1).

Surjectivity of p not stated. IsCoveringMap does not force surjectivity, but in (1)–(3) every relevant E is path-connected hence nonempty, X is connected, and fibre cardinality is locally constant for a covering map, so every pᵢ is in fact onto X. Consequently the existential over e₁, e₂ in (3) is never blocked by empty fibres. The theorem does not mention this; it is a consequence, not an assumption.

Hypothesis hX is used only for (1). Parts (2) and (3) hold for any path-connected, locally path-connected X. Bundling them under the stronger hypotheses matches Hatcher's Theorem 1.38 but makes (2),(3) formally weaker than the standalone isPointedIsomorphic_iff / coverSubgroup_conj.

Isomorphism notion. Both IsIsomorphic and IsPointedIsomorphic demand a Homeomorph (continuous inverse included) with $p_2\circ f = p_1$. This is the standard notion of isomorphism of covering spaces over X. The direction C₁ → C₂ is fixed in the definition; symmetry follows via Homeomorph.symm but is not asserted.

Which conjugate. In (3), the Lean condition is $g\,H_1\,g^{-1}=H_2$ with Mathlib's product, i.e. $g^{-1}H_1g = H_2$ in Hatcher's convention. Because g ranges over the whole group, "$H_1$ and $H_2$ are conjugate" is what is asserted either way.

Absent from the formal statement, present in textbooks: (a) the explicit bijection/quotient-set language; (b) surjectivity onto conjugacy classes as a separate clause; (c) uniqueness of the basepoint-preserving isomorphism; (d) the remark that the total spaces are themselves locally path-connected; (e) the normal-cover/deck-group refinement (Prop. 1.39/1.40), which is not part of Theorem 1.38 either. None of these absences weakens the assertions actually made; (a) and (b) are recoverable from (1)–(3) plus coverSubgroup_conj.

Degenerate instantiations. If $\pi_1(X,x_0)=1$ (e.g. X contractible): (1) is only about H = ⊤, satisfied by E = X; (2) and (3) say every two path-connected covers of X are (pointed-)isomorphic — correct. If E₁ = E₂ as covers, (3)'s right side is witnessed by any e₁, e₂ := e₁, g := 1. No instantiation makes the theorem vacuous.