Proposition 1.39 (final clause): for the universal cover, $G(\tilde X)\cong\pi_1(X)$

Proved

Hatcher.deckGroup_equiv_fundamentalGroup

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.39, final clause. If $p:\tilde X\to X$ is a simply-connected covering space (a universal cover) of the path-connected, locally path-connected space $X$ , then the deck transformation group is isomorphic to the fundamental group:

G(\tilde X)\cong\pi_1(X,x_0)\qquad\text{for every }x_0\in X.

This is Proposition 1.39(b) with $H=p_*\pi_1(\tilde X)=1$ (by injectivity of $p_*$ ), so $N(H)=\pi_1(X,x_0)$ and $N(H)/H=\pi_1(X,x_0)$ .

Formalization Note Simple connectivity of $\tilde X$ is SimplyConnectedSpace, which includes nonemptiness and path-connectedness; with $X$ path-connected this forces $p$ to be surjective. The statement asserts the existence of a group isomorphism.

Preamble

import Definitions.Def_Hatcher_Covering
import Mathlib

open Hatcher unitInterval

Formal statement

namespace Hatcher
theorem deckGroup_equiv_fundamentalGroup {E X : Type*} [TopologicalSpace E] [TopologicalSpace X]
    [PathConnectedSpace X] [LocallyPathConnectedSpace X] [SimplyConnectedSpace E]
    {p : E → X} (hp : IsCoveringMap p) (x₀ : X) :
    Nonempty (deckGroup p ≃* FundamentalGroup X x₀) := 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. 71, Proposition 1.39, final sentence ('Hence for the universal cover X̃ → X we have G(X̃) ≈ π₁(X)')

Read-back

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

Read-back of Hatcher.deckGroup_equiv_fundamentalGroup.

Setting and binders

E X : Type* — two types in independent, arbitrary universes.
[TopologicalSpace E] [TopologicalSpace X].
[PathConnectedSpace X] — $X$ nonempty and path-connected.
[LocallyPathConnectedSpace X] — every neighbourhood filter in $X$ has a basis of path-connected neighbourhoods.
[SimplyConnectedSpace E] — Mathlib's class: Nonempty (FundamentalGroupoid E ≌ Discrete Unit), i.e. the fundamental groupoid of $E$ is equivalent to the one-object, one-morphism groupoid. Mathlib proves this is equivalent to: $E$ is path-connected (so nonempty) and any two paths in $E$ with the same endpoints are homotopic rel endpoints. Consequently $\pi_1(E,e)$ is trivial for every $e$ . SimplyConnectedSpace E provides a PathConnectedSpace E instance.
{p : E → X} and (hp : IsCoveringMap p) — Mathlib's covering-map predicate (every point evenly covered with discrete fibre; range clopen; surjectivity not built in but here forced since $E\neq\emptyset$ and $X$ is connected).
(x₀ : X) — an arbitrary base point in $X$ . No base point in $E$ is chosen, and no lift of $x_0$ is named.

Definitions used:

deckGroup p : Subgroup (E ≃ₜ E) — $\mathrm{Deck}(p) = \{f \in \mathrm{Homeo}(E) \mid \forall e,\ p(f e) = p e\}$ with $(fg)(e) = f(g(e))$ , coerced to a type carrying the induced group structure.
FundamentalGroup X x₀ — $\pi_1(X,x_0)$ (loop classes at $x_0$ , with Mathlib's product $[\gamma]\cdot[\delta] = [\delta \ast \gamma]$ ).
A ≃* B (MulEquiv) — a bijection $A \to B$ that preserves multiplication, i.e. a group isomorphism.
Nonempty (deckGroup p ≃* FundamentalGroup X x₀) — the proposition that at least one such isomorphism exists.

Hypotheses

$X$ path-connected and locally path-connected; $E$ simply connected (in particular nonempty and path-connected); $p : E\to X$ a covering map; $x_0 \in X$ arbitrary.

Conclusion

\mathrm{Deck}(p)\ \cong\ \pi_1(X, x_0)\quad\text{as abstract groups;}

that is, there exists a bijective, multiplication-preserving map from the group of homeomorphisms $f:E\to E$ with $p\circ f = p$ onto the fundamental group of $X$ at $x_0$ .

Remarks

This is the textbook corollary of Hatcher Prop. 1.39(b) applied to a simply connected (universal) cover: $H = p_*\pi_1(E,e_0)$ is trivial, so $N(H) = \pi_1(X,x_0)$ and $G(\tilde X)\cong\pi_1(X,x_0)$ . It also appears as Hatcher's remark that the universal cover is a normal covering with deck group $\pi_1(X)$ .
Only abstract existence of an isomorphism is asserted (Nonempty of the type of isomorphisms). No particular isomorphism is named, and nothing ties it to a base point $e_0\in p^{-1}(x_0)$ . In the textbook, the isomorphism depends on the choice of $e_0$ in the fibre (different choices differ by conjugation), so "abstract existence" is the honest base-point-free formulation.
Opposite-group issue. Because only existence of some isomorphism is claimed, and every group is isomorphic to its opposite via $g\mapsto g^{-1}$ , Mathlib's reversed loop multiplication has no effect on the truth of this statement.
Nonvacuous. SimplyConnectedSpace E implies $E\neq\emptyset$ ; with $X$ connected and the range of a covering map clopen, $p$ is surjective and every fibre is nonempty. Thus $x_0$ does have lifts even though none is named.
Edge case: if $X$ is also simply connected, $p$ is a homeomorphism ( $E$ , $X$ both connected, fibres discrete with $\pi_1(X)$ acting transitively), both groups are trivial, and the statement holds trivially. If $X$ is the circle and $E=\mathbb R$ , the statement asserts $\mathrm{Deck}\cong\mathbb Z$ , as expected.
The hypothesis that $E$ be a universal cover is expressed purely by SimplyConnectedSpace E; no uniqueness or maximality of the cover is mentioned or needed.
No Hausdorff or semilocal simple-connectivity assumption on $X$ ; the latter would only be needed for existence of a simply connected cover, which is not asserted here (the cover is given).
Deck transformations must be homeomorphisms (not merely continuous maps or bijections), as in Hatcher.
Fully universe-polymorphic in E, X.

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.39 (final clause): for the universal cover, G(X~)≅π1(X)G(\tilde X)\cong\pi_1(X)G(X~)≅π1​(X)

Setting and binders

Hypotheses

Conclusion

Remarks

Proposition 1.39 (final clause): for the universal cover, $G(\tilde X)\cong\pi_1(X)$