Regularity from one fibre

Deck transformations commute with transport between fibres by covering-space monodromy. Thus, over a path-connected base, transitivity of the deck action on one nonempty fibre implies transitivity on every fibre (and also supplies surjectivity of the covering map). This reduces regularity to a condition at a single chosen fibre.

Main declarations

• TauCeti.Deck.isRegular_iff_fiber_isPretransitive: over a path-connected base, a covering is regular exactly when its deck group acts transitively on one chosen fibre.

References

The proof uses Junyan Xu's path-lifting and monodromy API in Mathlib.Topology.Homotopy.Lifting. It supplies the fibre-transport step of the regular cover criterion.

theorem TauCeti.Deck.isRegular_iff_fiber_isPretransitive {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {p : E → X} {x : X} [PathConnectedSpace X] (hp : IsCoveringMap p) (e : ↑(p ⁻¹' {x})) : IsRegular p ↔ MulAction.IsPretransitive ↥(deck p) ↑(p ⁻¹' {x})

Over a path-connected base, a covering map with a chosen point in one fibre is regular exactly when the deck action on that one fibre is transitive.

Monodromy transports transitivity to every other fibre. The chosen point also transports to every fibre, proving the surjectivity required by Deck.IsRegular.