Pointed connected covers are determined by the subgroup they recover #

A pointed cover of (X, x) is a covering map p : E → X together with a lift e₀ of x. It recovers the subgroup p_* π₁(E, e₀) ≤ π₁(X, x), and IsCoveringMap.stabilizer_eq_range identifies that subgroup with the stabiliser of e₀ for the monodromy action. This file proves that, for path-connected and locally path-connected total spaces, the recovered subgroup determines the pointed cover:

there is a map of pointed covers (E, e₀) → (F, f₀) over X exactly when p_* π₁(E, e₀) ≤ q_* π₁(F, f₀), and it is then unique;
if the two recovered subgroups are equal, that map is a homeomorphism over X.

This is the faithful-and-full half of the correspondence between pointed connected covers of (X, x) and subgroups of π₁(X, x); the remaining half is the construction, from a subgroup H, of a cover recovering H, which is a separate milestone. Nothing here needs X itself to be path-connected, locally path-connected or semilocally simply connected: those hypotheses are what make the correspondence onto, not what makes it injective.

The existence direction is Mathlib's lifting criterion IsCoveringMap.existsUnique_continuousMap_lifts_of_range_le, applied with the total space E as the source; the only work is the basepoint bookkeeping needed to state it symmetrically in the two covers, since a pointed cover recovers a subgroup of π₁(X, x) rather than of π₁(X, p e₀). The containment direction is elementary functoriality. Turning the two resulting maps into a homeomorphism uses Mathlib's uniqueness of lifts on a preconnected space, IsCoveringMap.eq_of_comp_eq, and no further covering-space input.

Specialising to simply connected total spaces gives the uniqueness of the universal cover: any two simply connected covers of X are isomorphic over X, by a homeomorphism matching chosen lifts of a basepoint. (Their universal property is already Mathlib's IsCoveringMap.existsUnique_continuousMap_lifts, which lifts any map from a simply connected, locally path-connected space.)

Main declarations #

IsCoveringMap.existsUnique_continuousMap_comp_eq_of_range_le: a unique map of pointed covers over X exists as soon as the recovered subgroups are nested.
IsCoveringMap.exists_continuousMap_comp_eq_iff_range_le: such a map exists exactly when the recovered subgroups are nested.
IsCoveringMap.exists_homeomorph_comp_eq_of_range_eq and IsCoveringMap.totalSpaceHomeomorphOfRangeEq: pointed covers recovering the same subgroup are isomorphic over X by a homeomorphism matching the chosen lifts.
IsCoveringMap.exists_homeomorph_comp_eq_iff_range_eq: the recovered subgroup is a complete invariant of a pointed cover.
IsCoveringMap.eq_totalSpaceHomeomorphOfRangeEq: that homeomorphism is the only map of pointed covers over X.
IsCoveringMap.deckMulEquivOfRangeEq: consequently their deck transformation groups are isomorphic.
IsCoveringMap.exists_homeomorph_comp_eq_of_simplyConnectedSpace: uniqueness of the universal cover.

References #

It consumes the lifting criterion in TauCeti.Topology.Homotopy.Covering and the recovered-subgroup API of TauCeti.Topology.Homotopy.Monodromy.Basic. The lifting criterion IsCoveringMap.existsUnique_continuousMap_lifts_of_range_le is Junyan Xu's, in Mathlib.Topology.Homotopy.Lifting, while the uniqueness of lifts IsCoveringMap.eq_of_comp_eq is Thomas Browning's, in Mathlib.Topology.Covering.Basic, where it is recorded as Proposition 1.34 of [hatcher02].