Proposition 1.37: basepoint-preserving isomorphism iff $p_{1}\pi_1(\tilde X_1,\tilde x_1)=p_{2}\pi_1(\tilde X_2,\tilde x_2)$

Proved

Hatcher.isPointedIsomorphic_iff

by korbonits · Sep 8, 2026 · Mathlib 0df444a (Lean v4.33.1)

algebraic-topologycovering-spacesfundamental-grouphatcher

Throughout, a covering space of $X$ is a space $\tilde X$ with a map $p:\tilde X\to X$ such that each $x\in X$ has an open neighborhood $U$ whose preimage $p^{-1}(U)$ is a disjoint union of open sets each mapped homeomorphically onto $U$ by $p$ (Hatcher, p. 56; Mathlib's IsCoveringMap). Given basepoints $\tilde x_0\in\tilde X$ , $x_0=p(\tilde x_0)$ , we write $p_*:\pi_1(\tilde X,\tilde x_0)\to\pi_1(X,x_0)$ for the induced homomorphism (Hatcher.coverHom) and $H=p_*\big(\pi_1(\tilde X,\tilde x_0)\big)$ for its image (Hatcher.coverSubgroup).

Proposition 1.37. If $X$ is path-connected and locally path-connected, then two path-connected covering spaces $p_1:\tilde X_1\to X$ and $p_2:\tilde X_2\to X$ are isomorphic via an isomorphism $f:\tilde X_1\to\tilde X_2$ taking a basepoint $\tilde x_1\in p_1^{-1}(x_0)$ to a basepoint $\tilde x_2\in p_2^{-1}(x_0)$ iff

p_{1*}\big(\pi_1(\tilde X_1,\tilde x_1)\big)=p_{2*}\big(\pi_1(\tilde X_2,\tilde x_2)\big).

Hatcher's proof applies the lifting criterion to $p_1$ and $p_2$ in both directions and the unique lifting property to see the two lifts are inverse.

Formalization Note An isomorphism of covering spaces is a homeomorphism $f$ with $p_1=p_2\circ f$ (p. 67); the statement is about PointedCover X x₀ structures and their subgroups.

Preamble

import Definitions.Def_Hatcher_Covering
import Mathlib

open Hatcher unitInterval

universe u

Formal statement

namespace Hatcher
theorem isPointedIsomorphic_iff {X : Type u} [TopologicalSpace X] [PathConnectedSpace X]
    [LocallyPathConnectedSpace X] {x₀ : X} (C₁ C₂ : PointedCover X x₀)
    (h₁ : PathConnectedSpace C₁.E) (h₂ : PathConnectedSpace C₂.E) :
    IsPointedIsomorphic C₁ C₂ ↔ C₁.subgroup = C₂.subgroup := by sorry
end Hatcher

Source

A. Hatcher, Algebraic Topology, Cambridge University Press 2002, https://pi.math.cornell.edu/~hatcher/AT/AT.pdf, Section 1.3, p. 67, Proposition 1.37

Read-back

What the Lean code literally says, in plain math · claude-fable-5-1

Read-back of Hatcher.isPointedIsomorphic_iff.

Setting and binders

X : Type u, [TopologicalSpace X] — a topological space in universe u.
[PathConnectedSpace X] — X is nonempty and any two points are joined by a continuous path (Mathlib's class bundles Nonempty X with ∀ x y, Joined x y).
[LocallyPathConnectedSpace X] — every neighbourhood filter 𝓝 x has a basis of path-connected neighbourhoods (s ∈ 𝓝 x ∧ IsPathConnected s).
{x₀ : X} — an implicit basepoint (determined by C₁ C₂).
C₁ C₂ : PointedCover X x₀ — two pointed covering spaces of X over x₀. Each Cᵢ consists of: a total space Cᵢ.E : Type u (same universe as X), a topology on it, a map Cᵢ.p : Cᵢ.E → X, a proof Cᵢ.isCoveringMap : IsCoveringMap Cᵢ.p, a point Cᵢ.e₀ : Cᵢ.E, and Cᵢ.p_e₀ : Cᵢ.p Cᵢ.e₀ = x₀.

IsCoveringMap p (Mathlib) means: for every x : X the fibre p⁻¹{x} is discrete and there is an open U ∋ x with p⁻¹(U) open and a homeomorphism p⁻¹(U) ≃ₜ U × p⁻¹{x} commuting with the projection to U. Surjectivity is not required; empty fibres and empty E are allowed.
h₁ : PathConnectedSpace C₁.E, h₂ : PathConnectedSpace C₂.E — both total spaces are (nonempty and) path-connected. Supplied as explicit hypotheses, not instances.

No semilocal simple connectivity of X is assumed here.

Hypotheses

Just the above. Nothing about E₁, E₂ being locally path-connected (this follows anyway since p is a local homeomorphism onto a locally path-connected space, but it is not stated), no Hausdorff assumption, and no relation between C₁ and C₂ is presupposed.

Conclusion

\texttt{IsPointedIsomorphic } C_1\ C_2 \iff C_1.\texttt{subgroup} = C_2.\texttt{subgroup}.

Left side, unpacked from the bundle:

\exists\, f : E_1 \simeq_t E_2,\quad \big(\forall e\in E_1,\ p_2(f(e)) = p_1(e)\big)\ \wedge\ f(e_0^{(1)}) = e_0^{(2)} .

E₁ ≃ₜ E₂ is Mathlib's Homeomorph: a bijection E₁ → E₂ (an Equiv, with two-sided inverse) such that both it and its inverse are continuous. So the left side says: there is a homeomorphism $f$ of total spaces with $p_2\circ f = p_1$ (a morphism of covering spaces over $X$ ; being a homeomorphism, it is an isomorphism of covers) and which carries the basepoint $e_0^{(1)}$ to $e_0^{(2)}$ . This is exactly a basepoint-preserving isomorphism of covering spaces in Hatcher's sense.

Right side: Cᵢ.subgroup is coverSubgroup Cᵢ.p Cᵢ.isCoveringMap.continuous Cᵢ.p_e₀, the range of coverHom Cᵢ.p _ Cᵢ.p_e₀ = FundamentalGroup.mapOfEq ⟨Cᵢ.p, _⟩ Cᵢ.p_e₀. By mapOfEq_apply, this homomorphism sends the class of a loop γ at e₀ to the class of p ∘ γ, re-typed as a loop at x₀ via p e₀ = x₀. Hence

C_i.\texttt{subgroup} = (p_i)_*\big(\pi_1(E_i, e_0^{(i)})\big)\ \le\ \pi_1(X,x_0),

and the right side is equality of these two subgroups of $\pi_1(X,x_0)$ as Subgroup values (i.e. equality of underlying subsets).

In words: for a path-connected, locally path-connected $X$ and two path-connected pointed covering spaces $(E_1,e_1)\to(X,x_0)$ , $(E_2,e_2)\to(X,x_0)$ , there is a basepoint-preserving isomorphism of coverings if and only if $(p_1)_*\pi_1(E_1,e_1) = (p_2)_*\pi_1(E_2,e_2)$ . This is Hatcher, Proposition 1.37, stated as an equivalence.

Remarks

The forward direction is essentially trivial and needs no hypotheses: if $f$ is a homeomorphism over $X$ carrying basepoints, then $(p_2)_*\circ f_* = (p_1)_*$ with $f_*$ an isomorphism $\pi_1(E_1,e_1)\cong\pi_1(E_2,e_2)$ , so the images coincide. The content is the reverse direction (the lifting criterion applied twice), for which path-connectedness of $E_1,E_2$ and local path-connectedness (inherited from X) are exactly the standard hypotheses. The statement is therefore not vacuous and not a trivialisation.
Universe. Both covers have E : Type u. The theorem says nothing about covers whose total space lives in another universe; because it is a statement about two given covers this is not a weakening in content (any path-connected cover of a Type u space is isomorphic to one in Type u), but a reader should note the PointedCover structure hard-wires E : Type u.
Surjectivity of pᵢ. Not stated, but automatic: Eᵢ is nonempty (contains e₀) and X is connected, so fibre-cardinality being locally constant forces every fibre to be nonempty.
Path-connectedness of X is a hypothesis but is not strictly needed for the equivalence (the lifting criterion only needs the source Eᵢ path-connected and locally path-connected); this matches Hatcher's stated hypotheses and is harmless.
Uniqueness of f (a textbook corollary: the basepoint-preserving isomorphism is unique) is not asserted; only existence appears on the left side.
What "isomorphism" means. IsPointedIsomorphic requires f to be a homeomorphism; it does not merely ask for a continuous bijection over X. It does not ask for a Homeomorph that is a fibrewise map in any further sense; p₂ ∘ f = p₁ is the only compatibility. It is stated with a specific direction (C₁ → C₂); since Homeomorph.symm inverts it, the relation is symmetric, though symmetry is not asserted here.
Group convention. Mathlib's FundamentalGroup multiplication is p * q = q.trans p (reversed w.r.t. Hatcher). Equality of subgroups is unaffected by this convention.
Edge instantiation. If C₁ = C₂ the right side is rfl-true and the left side is witnessed by Homeomorph.refl; nothing degenerate arises. If $\pi_1(X,x_0)$ is trivial, the right side is always true and the theorem then asserts that any two path-connected pointed covers of a simply-connected, locally path-connected X are pointed-isomorphic (both to X itself), which is the correct textbook consequence.
Compared with a textbook, nothing is missing from the statement of Prop. 1.37; the theorem does not include Hatcher's follow-up remark that, ignoring basepoints, isomorphism corresponds to conjugacy — that is the third conjunct of classification_of_covering_spaces.

Human review

Endorsed by Shuze Chen · Sep 8, 2026
Endorsed by korbonits · Sep 8, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Proposition 1.37: basepoint-preserving isomorphism iff p1∗π1(X~1,x~1)=p2∗π1(X~2,x~2)p_{1*}\pi_1(\tilde X_1,\tilde x_1)=p_{2*}\pi_1(\tilde X_2,\tilde x_2)p1∗​π1​(X~1​,x~1​)=p2∗​π1​(X~2​,x~2​)

Setting and binders

Hypotheses

Conclusion

Remarks

Proposition 1.37: basepoint-preserving isomorphism iff $p_{1}\pi_1(\tilde X_1,\tilde x_1)=p_{2}\pi_1(\tilde X_2,\tilde x_2)$