A regular covering is a quotient covering map for its deck group

For a covering map p : E → B with preconnected total space whose deck action is regular (surjective, with deck p acting transitively on every fibre), p exhibits B as the quotient of E by the deck transformation group: p is a IsQuotientCoveringMap for deck p. This is the deck-side formulation of UniversalCover x₀ / π₁(X, x₀) ≃ X, packaged so that it consumes Mathlib's quotient covering map theory rather than re-deriving it.

Conversely, a quotient covering map has regular deck action, for any acting group: its fibres are the orbits, and translation by a group element is a deck transformation. For a preconnected covering map, this gives an equivalence between being a quotient covering map for the deck group and regularity of the deck action.

Main declarations

• TauCeti.Deck.IsRegular.isQuotientCoveringMap: a regular, preconnected covering map is a quotient covering map for its deck group.
• IsQuotientCoveringMap.isRegular: quotient covering maps have regular deck action, whatever the acting group.
• TauCeti.Deck.isQuotientCoveringMap_iff_isRegular: for a preconnected covering map, being a quotient covering map for the deck group is equivalent to regularity of the deck action.
• TauCeti.Deck.IsRegular.isOpenQuotientMap: a regular covering map is an open quotient map.

References

Mathlib's quotient covering map theory is IsQuotientCoveringMap (Mathlib/Topology/Covering/Quotient.lean).

theorem TauCeti.Deck.IsRegular.isQuotientCoveringMap {E : Type u_1} {B : Type u_2} [TopologicalSpace E] [TopologicalSpace B] {p : E → B} [PreconnectedSpace E] (hreg : IsRegular p) (hp : IsCoveringMap p) : IsQuotientCoveringMap p ↥(deck p)

A regular covering map with preconnected total space is a quotient covering map for its deck transformation group: it presents the base as the quotient E / deck p.

theorem IsQuotientCoveringMap.isRegular {E : Type u_1} {B : Type u_2} [TopologicalSpace E] [TopologicalSpace B] {p : E → B} {G : Type u_3} [Group G] [MulAction G E] (h : IsQuotientCoveringMap p G) : TauCeti.Deck.IsRegular p

A quotient covering map for any acting group has regular deck action: its fibres are the orbits of the acting group, and each group element translates by a deck transformation.

theorem TauCeti.Deck.isQuotientCoveringMap_iff_isRegular {E : Type u_1} {B : Type u_2} [TopologicalSpace E] [TopologicalSpace B] {p : E → B} [PreconnectedSpace E] (hp : IsCoveringMap p) : IsQuotientCoveringMap p ↥(deck p) ↔ IsRegular p

For a covering map with preconnected total space, being a quotient covering map for the deck transformation group is equivalent to regularity of the deck action.

theorem TauCeti.Deck.IsRegular.isOpenQuotientMap {E : Type u_1} {B : Type u_2} [TopologicalSpace E] [TopologicalSpace B] {p : E → B} (hreg : IsRegular p) (hp : IsCoveringMap p) : IsOpenQuotientMap p

A regular covering map is an open quotient map.