Deck transformations and quotient actions
Hatcher's Propositions 1.39 and 1.40 identify the deck group of a connected cover from its fundamental-group subgroup, then recover this calculation for orbit quotients by covering-space actions.
Mathlib v4.34.1 contains both the quotient-covering machinery and the basic
deck group API in Mathlib/Topology/Covering/Deck.lean. Mathlib PR
#40135 is its
historical provenance. The local modules retain the fiber action, normal-cover
predicate, normalizer calculation, and Hatcher-specific quotient-action
consequences.
For a map p : E → X, Mathlib v4.34.1 defines deck p as the subgroup of
self-homeomorphisms of E that commute with p. The upstream file also
provides the induced action on E, together with deck.mem_iff,
deck.comp_eq, and deck.proj_smul.
The supporting Homeomorph.applyMulAction,
Homeomorph.applyFaithfulSMul, and Homeomorph.continuousConstSMul
instances are likewise present in the current pin.
Define Hatcher.Covering.IsNormal p to mean that p is a covering map, is
surjective, and has a transitive deck action on every fiber. Requiring
surjectivity matters: Mathlib and Hatcher's local definition of a covering map
permit empty fibers, so fiber transitivity alone would call the empty map
normal.
Mathlib PR #40135
is the historical provenance for this API, which is now included in the
v4.34.1 pin. Hatcher/Covering/Deck.lean retains only the project extensions:
deck.mulActionFiber restricts the action to each fiber, and
Hatcher.Covering.IsNormal records the covering, surjectivity, and fiberwise
transitivity requirements used downstream.
Dependencies
Let C be a pointed path-connected cover of a path-connected, locally
path-connected space (X,x₀), and let e₁ lie over x₀. There is exactly one
deck transformation carrying the chosen point e₀ to e₁ if and only if the
image subgroups obtained by basing the cover at e₀ and e₁ are equal.
Formalized as
Hatcher.BasedConnectedCover.existsUnique_deck_apply_basepoint_iff_range_eq
in Hatcher/Covering/DeckRealization.lean. The supporting theorem
deck.ext_of_eq_at supplies uniqueness from agreement at one point.
Existence is Proposition 1.37 applied to the same cover with two choices of
lifted basepoint. Uniqueness follows because two deck transformations that
agree at one point are equal on the connected total space. Export this
extensionality statement as deck.ext_of_eq_at before proving the main
equivalence.
Let C be a pointed connected cover of a path-connected, locally
path-connected base, and let H be the image of its induced fundamental-group
map. Construct the homomorphism
Hatcher.BasedConnectedCover.normalizerToDeck : normalizer H →* deck C.proj.
For g : normalizer H, lift a representative of g⁻¹ from the chosen point.
The basepoint-change formula identifies the subgroup at its endpoint with H,
so the deck-realization theorem supplies the unique deck transformation
carrying the chosen point to that endpoint.
The defining formula must match the project's monodromy convention:
normalizerToDeck g • e₀ = monodromyPerm (g : π₁(X,x₀))⁻¹ e₀.
The inverse belongs here, not in monodromyPerm. Direct monodromy is
multiplicative for Mathlib's fundamental-group law, while the deck
transformation selected by an endpoint composes in the opposite order unless
the normalizer argument is inverted.
Formalized in Hatcher/Covering/NormalizerToDeck.lean. The same file proves
the displayed formula as
Hatcher.BasedConnectedCover.normalizerToDeck_smul_basepoint and exports
deck.smul_monodromy and deck.smul_monodromyPerm for the commutation
calculations used below.
Dependencies
For a pointed connected cover over a path-connected, locally path-connected base, the normalizer homomorphism is surjective and has kernel
H.subgroupOf (normalizer H).
The main artifact should package these two assertions as
Hatcher.BasedConnectedCover.normalizerToDeck_ker_and_surjective. The same
file should expose the representative calculation: a lifted endpoint is in
the deck orbit of the chosen point exactly when the represented loop class
lies in normalizer H.
For the kernel, use the closed-lift characterization and the inverse in the
normalizer action formula. For surjectivity, join e₀ to the image of e₀
under an arbitrary deck transformation, project this path to a loop, and use
deck extensionality after matching the endpoint.
Formalized in Hatcher/Covering/NormalizerToDeckExactness.lean. The same file
exports Hatcher.BasedConnectedCover.exists_deck_smul_eq_monodromy_inv_iff_mem_normalizer
as the representative endpoint calculation.
Dependencies
Hatcher, Proposition 1.39 (page 71). Let C be a pointed path-connected
cover of a path-connected, locally path-connected space, and let H be the
image subgroup in π₁(X,x₀). Then:
C.projis normal exactly whenHis a normal subgroup; and- the deck group is isomorphic to
(normalizer H) ⧸ H.subgroupOf (normalizer H).
The main artifact is
Hatcher.BasedConnectedCover.normalizerQuotientEquivDeck, in the natural
direction produced by the first isomorphism theorem. The same file should
export isNormal_iff_range_normal and the normal-cover corollary
π₁(X,x₀) ⧸ H ≃* deck C.proj, installing the normality instance only after it
has been proved. It should first derive
Hatcher.BasedConnectedCover.proj_surjective from the chosen point and
path-connectedness of the base, rather than treating every Mathlib covering
map as surjective.
Construct the quotient equivalence from normalizerToDeck using
QuotientGroup.quotientKerEquivOfSurjective. For the first clause, first prove
that deck transformations commute with covering monodromy. Use this to show
that, over a path-connected base, deck transitivity on the chosen fiber is
equivalent to transitivity on every fiber. The normalizer endpoint criterion
then identifies chosen-fiber transitivity with normalizer H = ⊤; finish with
Subgroup.normalizer_eq_top_iff.
Formalized in Hatcher/Covering/DeckGroupCalculation.lean. Besides the main
equivalence, the file exports
Hatcher.BasedConnectedCover.proj_surjective,
Hatcher.BasedConnectedCover.isNormal_iff_range_normal, and the normal-cover
corollary Hatcher.BasedConnectedCover.fundamentalGroupQuotientEquivDeck.
Sources
Assume [Group G], [MulAction G Y], [TopologicalSpace Y], and
[ContinuousConstSMul G Y]. Define Hatcher's covering-space action condition
Hatcher.IsCoveringSpaceAction G Y by requiring that each y : Y have a
neighborhood U such that
((g • ·) '' U ∩ U).Nonempty → g = 1
for every g : G. Also record the equivalent pairwise-disjoint-translates
form used in Hatcher's condition (*).
For the orbit projection
q : Y → Quotient (MulAction.orbitRel G Y),
the main artifact is
Hatcher.IsCoveringSpaceAction.isQuotientCoveringMap_orbitQuotient, proving
IsQuotientCoveringMap q G directly from the pinned quotient-map API. The
same file should define the canonical homomorphism
Hatcher.Covering.actionToDeck : G →* deck q.
Also record Hatcher's preceding unnumbered observation: if p : E → X is a
covering map and E is path-connected, then the canonical action of deck p
on E is a covering-space action. Choose one covering sheet at a point; if two
of its deck translates meet, unique lifting forces the corresponding deck
transformations to be equal.
Do not replace this hypothesis with ProperlyDiscontinuousSMul: Mathlib's
class expresses finiteness of translates meeting pairs of compact sets, not
Hatcher's local pairwise-disjoint condition. The pinned theorem converting
that class to a quotient covering additionally assumes LocallyCompactSpace
and T2Space, which would strengthen this result. No connectedness,
Hausdorffness, or local compactness is needed for this node.
Formalized in Hatcher/Covering/CoveringSpaceAction.lean. The file also
defines Hatcher.Covering.actionToDeck, proves the pairwise-disjoint-translates
characterization, and shows that the deck action of a covering with
path-connected total space is a covering-space action.
Dependencies
Hatcher, Proposition 1.40(a,b) (page 72). If a group G acts on Y by a
covering-space action, the orbit projection
q : Y → Quotient (MulAction.orbitRel G Y)
is a normal covering. If Y is path-connected, the canonical homomorphism
from G to deck q is an isomorphism.
The main artifact is Hatcher.Covering.actionEquivDeck. The same file should
export the normality theorem without adding connectedness when it is not
needed. Fiber transitivity comes from
IsQuotientCoveringMap.mulActionFiber_isPretransitive, transported along
actionToDeck to the deck action; surjectivity is part of the
quotient-covering structure. To prove every deck transformation arises from
G, match it at one point and apply unique lifting on the path-connected total
space.
Formalized in Hatcher/Covering/OrbitQuotientDeckGroup.lean. The file also
exports Hatcher.Covering.isNormal_orbitQuotient, whose statement does not
require path-connectedness.
Hatcher, Proposition 1.40(c) (page 72). Let G act on a path-connected,
locally path-connected space Y by a covering-space action, let q be the
orbit projection, and choose y₀ : Y. Then there is a group isomorphism
π₁(Y/G, q(y₀)) ⧸ range(π₁(q)) ≃* G.
Intended artifact:
Hatcher.Covering.orbitQuotientFundamentalGroupEquiv.
Use the path-connected and locally path-connected structures inherited by the
orbit quotient, namely Quotient.instPathConnectedSpace and
Quotient.locPathConnectedSpace. The subgroup is the range of
FundamentalGroup.map ⟨q, ...⟩ y₀, where the continuous map is the orbit
projection; mapOfEq is unnecessary because the target basepoint is
definitionally q y₀. Proposition 1.39 identifies the deck group with the
displayed fundamental-group quotient, and Proposition 1.40(b) identifies the
same deck group with G. Form the quotient only after obtaining the
normal-subgroup instance from normality of the orbit cover.
Formalized in Hatcher/Covering/OrbitQuotientFundamentalGroup.lean. The proof
explicitly identifies the direct FundamentalGroup.map range with the
mapOfEq range stored by the pointed-cover structure before transporting the
quotient equivalence.