A connected covering of a simply connected space is a homeomorphism

Proved

PoincareFormalization.covering_is_homeomorph

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

covering-spacespoincare-conjecturetopology

Let $E$ be a nonempty connected topological space, let $X$ be a simply connected and locally path connected topological space, and let $p:E\to X$ be a covering map. Then $p$ itself is a homeomorphism:

\exists e:E\cong X,\qquad e=p.

No compactness, Hausdorff, or dimension assumption is needed. This gives the final covering-space step in deriving Poincaré from a spherical covering. The hypothesis that such a covering exists is not part of this result's conclusion.

Preamble

import Mathlib.Topology.Homotopy.Lifting

Formal statement

theorem PoincareFormalization.covering_is_homeomorph
    {E X : Type*} [TopologicalSpace E] [TopologicalSpace X]
    [ConnectedSpace E] [SimplyConnectedSpace X] [LocallyPathConnectedSpace X]
    (p : E → X) (hp : IsCoveringMap p) :
    ∃ e : E ≃ₜ X, (e : E → X) = p := by sorry

Source

Corollary of Hatcher, Algebraic Topology (2002), Section 1.3, Propositions 1.33 (pp. 61–62, existence of lifts) and 1.34 (p. 62, uniqueness of lifts): https://pi.math.cornell.edu/~hatcher/AT/AT.pdf . Uses the existing Mathlib implementations in Topology/Homotopy/Lifting.lean and Topology/Covering/Basic.lean, revision 0df444a360eaa60ab8c11dca51a86af692955474.

View graph