The path-class universal cover
Hatcher constructs a simply-connected cover of a path-connected, locally
path-connected, semilocally simply-connected space from homotopy classes of
paths starting at a basepoint. The topology here is generated directly by
Hatcher's basic sets U[γ].
Define Hatcher.SemilocallySimplyConnectedSpace X to mean that every
x : X has an open neighborhood U for which the inclusion-induced map
π₁(U,x) →* π₁(X,x)
is trivial. The definition should use the subtype basepoint explicitly and
include a lemma transporting the property between basepoints inside a
path-connected U.
Formalized as Hatcher.SemilocallySimplyConnectedSpace in
Hatcher/Covering/SemilocallySimplyConnected.lean. The accompanying theorem
Hatcher.trivial_fundamentalGroupMap_of_isPathConnected proves the requested
basepoint independence inside a path-connected subspace.
This is Hatcher's unnumbered definition on page 63. It is weaker than local simple connectivity, and it must not be replaced by local contractibility. The pinned Mathlib has no corresponding class.
For a locally path-connected, semilocally simply-connected space X, the
path-connected open subsets U whose inclusion into X induces the trivial
map on fundamental groups form a basis for the topology.
Intended artifact: Hatcher.isTopologicalBasis_nullhomotopicOpens.
The statement must carry the basepoint-independence lemma from the semilocal
definition, since Hatcher uses arbitrary endpoints when defining U[γ].
Formalized in Hatcher/Covering/NullhomotopicOpenBasis.lean, using the
basepoint-independent predicate Hatcher.IsNullhomotopicOpen.
Dependencies
For a path-connected, locally path-connected, semilocally simply-connected
space X with basepoint x₀, define the total space
Hatcher.UniversalCover X x₀ = Σ x, Path.Homotopic.Quotient x₀ x.
Equip it with Hatcher's topology generated by the sets U[γ], where U is a
small path-connected open neighborhood of the endpoint and paths are extended
inside U. Define the endpoint projection and the constant-path basepoint.
The main artifact is Hatcher.UniversalCover; supporting artifacts should be
Hatcher.UniversalCover.basicOpen, Hatcher.UniversalCover.proj, and
Hatcher.UniversalCover.basepoint.
Formalized in Hatcher/Covering/UniversalCoverPathSpace.lean. Its topology is
generated directly by the path-extension sets attached to
Hatcher.IsNullhomotopicOpen neighborhoods.
Dependencies
For a small path-connected open set U and a path class [γ] ending in U,
let U[γ] consist of classes obtained by extending γ along a path inside
U. These sets form a topological basis on Hatcher.UniversalCover X x₀.
Moreover, U[γ] = U[γ'] whenever [γ'] ∈ U[γ], and endpoint projection is a
bijection from U[γ] to U.
Intended artifact: Hatcher.UniversalCover.isTopologicalBasis_basicOpen.
This node uses Hatcher's direct basis argument. It does not require the compact-open tube-neighborhood API from PR #38292.
Formalized in Hatcher/Covering/UniversalCoverBasis.lean. The same file proves
basicOpen_eq_of_mem and bijOn_proj_basicOpen, covering the equality and
endpoint-bijection clauses of the source statement.
Dependencies
Let X be path-connected, locally path-connected, and semilocally
simply-connected. For the path-class space, the endpoint projection
Hatcher.UniversalCover.proj : UniversalCover X x₀ → X
is a covering map. For each small open U, the sets U[γ] partition the
preimage of U, and projection restricts to a homeomorphism on every part.
Intended artifact: Hatcher.UniversalCover.isCoveringMap_proj.
Hatcher's general definition permits empty fibers, but this endpoint map is
surjective because X is path-connected.
Formalized in Hatcher/Covering/UniversalCoverIsCovering.lean. The file also
exports continuity and surjectivity of the endpoint map, discreteness of its
fibers, and openness of the basic sheets used in the covering trivializations.
Let X be path-connected, locally path-connected, and semilocally
simply-connected. The total space Hatcher.UniversalCover X x₀ is
path-connected. A point represented by γ is joined to the constant-path basepoint by the path
t ↦ [γₜ], where γₜ follows γ up to time t and is then stationary.
Intended artifact: Hatcher.UniversalCover.pathConnectedSpace.
The same file must first prove continuity of the initial-segment family in the
U[γ] basis; the path construction is not merely set-level.
Formalized in Hatcher/Covering/UniversalCoverPathConnected.lean. The file
exports the initial-segment family, its continuity theorem, and the resulting
path before installing the path-connected-space instance.
Let X be path-connected, locally path-connected, and semilocally
simply-connected. The total space Hatcher.UniversalCover X x₀ is
simply-connected.
Intended artifact: Hatcher.UniversalCover.simplyConnectedSpace.
Follow Hatcher's proof. The endpoint projection injects fundamental groups, and a base loop in the image has a closed lift in the path-class cover only when its original homotopy class is trivial.
Formalized in Hatcher/Covering/UniversalCoverSimplyConnected.lean. The proof
identifies projected paths with their endpoint coordinates by lift uniqueness,
cancels a projected loop, and applies covering-map injectivity on path classes.
Dependencies
Open Mathlib PR #38292 is implementation prior art, but uses a different compact-open quotient route. The roadmap does not identify the two topologies without an equivalence proof.