Covering spaces
Hatcher §1.3 (pages 56–82). The selected slice follows the classification and deck-transformation spine from lifting properties through Proposition 1.40. Permutation reconstruction and geometric examples remain deferred.
Mathlib v4.34.1 contains most of the hard lifting theory together with the based monodromy action and the basic deck-transformation group. The roadmap separates exact upstream declarations from the thin source-facing wrappers and project-specific consequences Hatcher's statements require. Universal covers and the classification itself remain project-local.
Lifting and monodromy
Proposition 1.30 is a source-facing wrapper around Mathlib's existing lifted homotopy and its uniqueness characterization.
Hatcher, Proposition 1.30 (page 60). Given a covering map p : E → X, a
homotopy H : I × A → X, and a continuous lift f₀ : A → E of the time-zero
map, there exists a unique continuous homotopy H̃ : I × A → E that lifts H
and begins at f₀.
Formalized as Hatcher.Covering.existsUnique_liftHomotopy in
Hatcher/Covering/HomotopyLifting.lean.
This is a thin source-facing wrapper around
IsCoveringMap.liftHomotopy, liftHomotopy_lifts,
liftHomotopy_zero, and eq_liftHomotopy_iff'. No new subdivision proof
belongs in this node.
Sources
The based monodromy action is now supplied by Mathlib. The next local nodes identify the induced subgroup and derive Hatcher's sheet-index calculation. The primary statement for Proposition 1.32 is a fiber-to-coset equivalence, since Mathlib's natural-number subgroup index encodes infinite index as zero.
For a covering p : E → X and basepoint x₀ : X, package endpoint transport
on the fiber over x₀ as a homomorphism
π₁(X,x₀) →* Equiv.Perm (p ⁻¹' {x₀}).
This is IsCoveringMap.monodromyPerm in Mathlib v4.34.1.
Use Mathlib's IsCoveringMap.monodromy transport directly. Its
FundamentalGroup multiplication is already opposite categorical path
composition, so monodromy_trans_apply makes direct endpoint transport a
homomorphism to Equiv.Perm. Inverting transport here would reverse products
and would not define the claimed homomorphism.
The upstream definition IsCoveringMap.fundamentalGroupMulAction exposes the
action, and IsCoveringMap.coe_monodromyPerm identifies it pointwise with
endpoint transport. Hatcher/Covering/Monodromy.lean retains the
project-specific fixed-point characterization used by the next node.
Mathlib PR #33108
is the historical provenance for the implementation, including the pointwise
identification with IsCoveringMap.monodromy; that API is now included in the
v4.34.1 pin.
Dependencies
For a covering map p : E → X and endpoints e₀,e₁ : E, composition with
p is injective on endpoint-preserving path-homotopy classes from e₀ to
e₁. Specializing to e₀ = e₁ gives the injectivity clause of Hatcher's
Proposition 1.31.
This is exactly the pinned declaration
IsCoveringMap.injective_path_homotopic_map, whose docstring cites
Proposition 1.31.
Dependencies
Hatcher, Proposition 1.31, second clause (page 61). For a pointed covering
p : (E,e₀) → (X,x₀), a class in π₁(X,x₀) lies in the range of the induced
map from π₁(E,e₀) exactly when its lift beginning at e₀ ends at e₀.
Equivalently, the image subgroup is the stabilizer of e₀ for the monodromy
action.
Formalized as Hatcher.Covering.mem_range_map_iff_monodromy_fixed in
Hatcher/Covering/Monodromy.lean. The forward implication is Mathlib's
IsCoveringMap.monodromy_map; the reverse implication lifts a representative
loop and uses the fixed endpoint to make that lift a loop based at e₀.
Sources
Dependencies
Hatcher, Proposition 1.32 (page 61). For a pointed covering with
path-connected base and total spaces, let H be the image subgroup in
π₁(X,x₀). The fiber over the basepoint is equivalent to Hatcher's right-coset
type H \ π₁(X,x₀). Because Mathlib's fundamental-group multiplication is
opposite Hatcher's first-then path concatenation, this is represented in Lean
by the ordinary quotient π₁(X,x₀) ⧸ H, using QuotientGroup.leftRel.
Consequently the fiber and this quotient have equal cardinality.
Formalized as Hatcher.Covering.fiberEquivQuotientRange in
Hatcher/Covering/SheetIndex.lean, with the cardinal-valued corollary
Hatcher.Covering.mk_fiber_eq_mk_quotientRange. The proof makes the direct
monodromy action transitive using path-connectedness of the total space, then
applies orbit-stabilizer and the closed-lift characterization of the
stabilizer.
Do not state the general result only with Subgroup.index : ℕ: Mathlib assigns
zero to an infinite index, while Hatcher's number of sheets is cardinal-valued.
The finite-sheeted natural-number corollary can be added after the equivalence.
Sources
The lifting criterion already exists in its difficult direction; the local node supplies Hatcher's exact equivalence. Proposition 1.34 is an exact pinned declaration.
Hatcher, Proposition 1.33 (pages 61–62). Let Y be path-connected and
locally path-connected. A pointed continuous map f : (Y,y₀) → (X,x₀) has a
pointed lift through p : (E,e₀) → (X,x₀) if and only if
range(f∗) ≤ range(p∗).
Formalized as Hatcher.Covering.exists_lift_iff_range_le in
Hatcher/Covering/LiftingCriterion.lean.
The pinned theorem
IsCoveringMap.existsUnique_continuousMap_lifts_of_range_le proves the hard
direction and uniqueness. The reverse implication uses the supplied lift and
functoriality of induced fundamental-group maps. No semilocal simple
connectivity hypothesis on X is needed.
Sources
Hatcher, Proposition 1.34 (page 62). Two continuous lifts from a connected space that agree at one point agree everywhere.
The pinned declaration IsCoveringMap.eq_of_comp_eq states this with
PreconnectedSpace and a supplied comparison point. The point supplies the
nonemptiness implicit in Hatcher's connectedness hypothesis.
Sources
Dependencies
If p : E → X is a covering map and X is locally path-connected, then E
is locally path-connected.
Formalized as Hatcher.Covering.locPathConnectedSpace_total in
Hatcher/Covering/LocalPathConnected.lean.
Hatcher uses this unnumbered fact before the classification theorem. It is a small local-homeomorphism argument, but it must be explicit before applying the lifting criterion with one covering space as the domain of a map to another.
The path-class universal cover
Hatcher's construction needs a local nullhomotopy condition, a basis of small
path-connected opens, and topology on endpoint-preserving path classes. This
roadmap uses Hatcher's U[γ] basis directly. Open Mathlib PR
#38292
contains implementation prior art for based paths and universal covers, but its
compact-open quotient topology is not silently mixed with the direct basis.
- The path-class universal cover
- Semilocally simply-connected spaces
- Small nullhomotopy neighborhoods form a basis
- The path-class universal-cover space
- The universal-cover basic sets form a basis
- The endpoint map is a covering
- The path-class cover is path-connected
- The path-class cover is simply-connected
Subgroups and classification
For a subgroup H ≤ π₁(X,x₀), quotient the path-class cover by Hatcher's
same-endpoint relation and calculate the image subgroup. This is Proposition
1.36.
Let X be path-connected, locally path-connected, and semilocally
simply-connected, and fix H ≤ π₁(X,x₀). On the path-class universal cover,
identify two points represented by paths γ and γ' when they have the same
endpoint and the loop class of γ.trans γ'.symm lies in H. Define
SubgroupCover H as the quotient, with its endpoint projection and the class
of the constant path as basepoint.
The main artifact is Hatcher.SubgroupCover H; supporting artifacts should be
Hatcher.SubgroupCover.proj and Hatcher.SubgroupCover.basepoint.
The equivalence relation and quotient topology must be stated directly. Do not silently assume a deck-transformation action, which is part of the later deferred material in Hatcher.
Formalized in Hatcher/Covering/SubgroupCoverSpace.lean. The direct relation,
its generated setoid, the endpoint projection, and the constant-path
basepoint are all exported; the standard Quotient topology supplies the
coinduced quotient topology through a named instance, without introducing a
deck action.
Let X be path-connected, locally path-connected, and semilocally
simply-connected. For every H ≤ π₁(X,x₀), the endpoint projection from
SubgroupCover H to X is a covering map and its total space is
path-connected.
The main artifact is Hatcher.SubgroupCover.isCoveringMap_proj; the same file
should provide Hatcher.SubgroupCover.pathConnectedSpace.
Use the images of Hatcher's basic sets U[γ]. If any points from two such sets
are identified by the subgroup relation, the whole sets are identified, so
their images are sheets over U.
Formalized in Hatcher/Covering/SubgroupCoverIsCovering.lean. The proof descends
the universal-cover basic opens through the subgroup quotient, proves that they
form disjoint sheets with discrete fibers, and builds the covering trivialization.
Hatcher, Proposition 1.36 (pages 66–67). Let X be path-connected,
locally path-connected, and semilocally simply-connected. For every subgroup
H ≤ π₁(X,x₀), the pointed projection from SubgroupCover H has induced
fundamental-group image exactly H.
Intended artifact: Hatcher.SubgroupCover.range_map_eq.
A loop in X lifts from the constant-path class to the class represented by
that loop, and this endpoint is the basepoint of the quotient precisely when
the loop class belongs to H.
Formalized in Hatcher/Covering/SubgroupCoverImage.lean. The proof computes
the monodromy endpoint using the initial-segment lift and reduces equality with
the quotient basepoint to the defining subgroup relation.
Sources
The classification is phrased through a small project-local bundle of pointed
connected covers. Realization and rigidity do not need a category of all
objects over X. The formalized classification uses a fixed-universe quotient
of covers by isomorphism, while a separate cross-universe theorem identifies
every pointed connected cover with its canonical subgroup-cover representative.
Define a small, universe-indexed record Hatcher.BasedConnectedCover X x₀
containing:
- a total-space type with its topology;
- a projection to
Xand a proof that it is a covering map; - a chosen point over
x₀; and - path-connectedness of the total space.
The same file should define basepoint-preserving covering isomorphisms as homeomorphisms commuting with projection, unpointed connected covers, and the corresponding isomorphism relations.
Formalized in Hatcher/Covering/ConnectedCover.lean. Cover isomorphisms may
relate total spaces in different universes, while the named setoid instances
remain fixed at one total-space universe for later classification quotients.
This direct record is deliberately smaller than a category inside
TopCat.Over X. Fix the total-space universe as an explicit parameter so the
classification theorem cannot hide a size assumption.
Dependencies
Hatcher, Proposition 1.37 (page 67). Let X be path-connected and locally
path-connected. Two pointed path-connected covering spaces over (X,x₀) are
isomorphic by a basepoint-preserving covering isomorphism if and only if their
induced image subgroups in π₁(X,x₀) are equal.
Formalized as Hatcher.BasedConnectedCover.nonempty_iso_iff_range_eq in
Hatcher/Covering/Rigidity.lean. The same file defines the source-facing image
subgroup Hatcher.BasedConnectedCover.fundamentalGroupRange.
For the reverse direction, lift each projection through the other cover using the lifting criterion. Unique lifting makes the two composites identities.
Sources
Hatcher, Theorem 1.38, based clause (page 67). For a path-connected,
locally path-connected, semilocally simply-connected X, assigning the image
subgroup to a pointed connected cover gives a bijection from
basepoint-preserving isomorphism classes of covers to subgroups of
π₁(X,x₀).
Intended artifact: Hatcher.BasedConnectedCover.classificationEquiv.
Formalized in Hatcher/Covering/PointedCoverClassification.lean. The
classification uses the quotient of pointed connected covers whose total
spaces live in the same universe as X. This fixed-universe quotient is
equivalent to the subgroups of π₁(X,x₀). A separate cross-universe theorem,
Hatcher.BasedConnectedCover.isomorphic_ofSubgroup_fundamentalGroupRange,
shows that every pointed connected cover in any universe is isomorphic to its
canonical subgroup-cover representative in the fixed universe.
Dependencies
For a path-connected covering of (X,x₀), changing the chosen point in the
fiber from e₀ to e₁ changes the induced image subgroup by conjugation with
the class of the projection of any path from e₀ to e₁. Conversely, every
conjugate is realized by lifting a representative loop from e₀.
Formalized as Hatcher.Covering.range_mapOfEq_basepointChange in
Hatcher/Covering/BasepointChange.lean. The same file proves the converse
Hatcher.Covering.exists_basepoint_range_eq_map_conj by taking the monodromy
endpoint of a representative class. The Lean theorem assumes the connecting
path explicitly, so it does not need a global path-connectedness hypothesis.
The source writes the new subgroup as g⁻¹ H g. Mathlib's fundamental-group
multiplication reverses Hatcher's first-then path concatenation, so the Lean
statement becomes g H g⁻¹, represented by H.map (MulAut.conj g).
Hatcher, Theorem 1.38, unbased clause (pages 67–68). For a
path-connected, locally path-connected, semilocally simply-connected X,
isomorphism classes of path-connected covers of X correspond bijectively to
conjugacy classes of subgroups of π₁(X,x₀).
Intended artifact: Hatcher.ConnectedCover.classificationEquivConjClasses.
Formalized in Hatcher/Covering/UnpointedCoverClassification.lean. The
classification uses the quotient of connected covers whose total spaces live
in the same universe as X, and the quotient of subgroups by Mathlib's
conjugation-orbit relation. Changing the chosen point over x₀ changes the
image subgroup only by conjugacy, so the resulting class is independent of
that choice.
As in the pointed classification, fixing the universe avoids a size mismatch
between the type of all covers and the subgroup type. The cross-universe
theorem Hatcher.ConnectedCover.isomorphic_ofSubgroup_chosenRange shows that
every connected cover in any universe is isomorphic to a canonical subgroup
cover in the fixed universe.
Let U → X be a pointed simply-connected cover and E → X a pointed
path-connected cover, with X path-connected and locally path-connected.
There is a unique basepoint-preserving map U → E over X, and this map is a
covering map. Consequently any two pointed simply-connected covers of X are
isomorphic as covering spaces.
Intended artifact: Hatcher.BasedConnectedCover.existsUnique_map_fromSimplyConnected;
the same file should provide
Hatcher.BasedConnectedCover.nonempty_iso_of_simplyConnected.
This is an initial, not terminal, property in the category whose morphisms are
pointed maps of covers over X. Existence is the lifting criterion because the
source fundamental group is trivial. Unique lifting identifies comparison
maps. A supporting local lemma should show that such a map between covers is
itself a covering map.
Formalized in Hatcher/Covering/UniversalCoverInitial.lean. The proof first
constructs the unique lift by the fundamental-group lifting criterion. It then
proves the comparison map is a covering by combining path-lifting
surjectivity, cancellation for local homeomorphisms, and compatible
path-connected trivialization neighborhoods. Applying the construction in
both directions gives the pointed covering isomorphism.
Deck transformations and quotient actions
Proposition 1.39 turns the induced subgroup into a deck-group calculation. The normalizer acts on the cover, its kernel is the covering subgroup, and normal covers are exactly those whose image subgroup is normal. Proposition 1.40 applies this to orbit quotients satisfying Hatcher's exact local-disjoint condition.
- Deck transformations and quotient actions
- Deck transformations and normal covers
- A deck transformation is determined by one lifted point
- The normalizer acts by deck transformations
- The normalizer map is surjective with kernel the covering subgroup
- The deck group is the normalizer quotient
- Covering-space actions give quotient coverings
- Orbit quotients are normal and have the expected deck group
- The orbit-quotient fundamental group recovers the acting group
Deferred within §1.3
Example 1.35, the reconstruction of arbitrary covers from permutation actions, and Examples 1.41–1.48 are deferred. Mathlib PR #40135 is the historical source of the basic deck-group API now included in v4.34.1; the normalizer, normal-cover, and quotient-action consequences in this roadmap remain local.