Regular connected covers and normal subgroups

A pointed connected covering recovers the image of the fundamental group of its total space in the fundamental group of the base. This file proves the regular-cover criterion: over a path-connected base, the covering is regular exactly when that recovered subgroup is normal.

The proof combines two existing classification results. Normality says that the recovered subgroup is independent of the chosen point in a fibre, while pointed-cover classification says that equality of those subgroups is exactly the existence of a deck transformation carrying one chosen point to the other. The monodromy transport API then promotes transitivity on the chosen fibre to regularity on every fibre.

Main declaration

• IsCoveringMap.isRegular_iff_normal_range: a connected covering is regular exactly when its recovered subgroup of the fundamental group is normal.

References

This is the regular-cover criterion: a cover attached to H is regular (normal/Galois) exactly when H is normal. It uses Mathlib's covering-space lifting criterion, due to Junyan Xu, through Tau Ceti's pointed-cover classification.

theorem IsCoveringMap.isRegular_iff_normal_range {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {p : E → X} {x : X} [PathConnectedSpace E] [LocallyPathConnectedSpace E] [PathConnectedSpace X] (hp : IsCoveringMap p) (e : ↑(p ⁻¹' {x})) : TauCeti.Deck.IsRegular p ↔ (FundamentalGroup.mapOfEq { toFun := p, continuous_toFun := ⋯ } ⋯).range.Normal

Regular-cover criterion. Let p : E → X be a covering map with path-connected, locally path-connected total space and path-connected base. For any chosen lift e of x, the deck action is regular exactly when the recovered subgroup p_* π₁(E, e) ≤ π₁(X, x) is normal.