Intermediate quotients of a quotient covering map

Let a group G act on a space E so that q : E → X presents X as the quotient E / G in the strong sense of Mathlib's IsQuotientCoveringMap: the fibres of q are the orbits, and every point of E has a neighbourhood whose G-translates are pairwise disjoint. Let H be a subgroup of G, and let qH : E → Y present Y as E / H in the same sense. The projection q then factors through qH, and the theorem of this file is that the factor

r : E / H → E / G

is a covering map. Neither space is assumed connected, and no local connectedness of X is needed: the sheets of r over the base set q '' U are the images in Y of the translates g • U, whose overlaps the disjointness hypothesis controls directly.

The intended reading is that a subgroup of the deck group of a regular covering cuts out an intermediate covering. That is the shape of the subgroup-to-cover half of the classification of covering spaces, where E is the universal cover of X and G is its fundamental group; that application is TauCeti.UniversalCover.isCoveringMap_subgroupQuotientProj.

Main results

• TauCeti.IsQuotientCoveringMap.isCoveringMap_of_comp: the map from the quotient by a subgroup down to the quotient by the whole group is a covering map.

Implementation notes

The sheets are produced by hand rather than by exhibiting r as a quotient covering map for some group, because in general it is not one. The fibre of r over q e consists of the classes of the points g • e for g : G, two of which agree exactly when g differs by an element of H; the normalizer quotient N_G(H) / H acts on E / H over X by deck transformations of r, but on that fibre it acts transitively only when H is normal in G. (Whether it exhausts the deck transformations of r is a further question, needing connectedness hypotheses that are not assumed here.)

So the construction goes through Mathlib's IsOpen.trivializationDiscrete, which turns a family of pairwise disjoint sets on which the map is injective into a Bundle.Trivialization. The index type of that family is the set of translate images itself, which makes the family injective and its pairwise disjointness exactly the statement that two meeting translate images coincide.

References

The IsQuotientCoveringMap interface this file is built on — the predicate itself, its disjoint and apply_eq_iff_mem_orbit fields, and IsQuotientCoveringMap.isOpenQuotientMap — is Junyan Xu's, in Mathlib/Topology/Covering/Quotient.lean.

theorem TauCeti.IsQuotientCoveringMap.isCoveringMap_of_comp {E : Type u_1} {X : Type u_2} {Y : Type u_3} [TopologicalSpace E] [TopologicalSpace X] [TopologicalSpace Y] {G : Type u_4} [Group G] [MulAction G E] {H : Subgroup G} {q : E → X} {qH : E → Y} {r : Y → X} (hq : IsQuotientCoveringMap q G) (hqH : IsQuotientCoveringMap qH ↥H) (hr : r ∘ qH = q) : IsCoveringMap r

An intermediate quotient of a quotient covering map is a covering map.

If q : E → X presents X as the quotient of E by a group G in the sense of IsQuotientCoveringMap, and qH : E → Y presents Y as the quotient of E by a subgroup H of G, then the map r : Y → X through which q factors is a covering map.