4.3. Quotient by properly discontinuous, free group actions🔗

Covering spaces arise from group actions and Mathlib has API to support this. A key concept is that of quotient covering map. If a group G acts on E and f : E → X then we say f is a quotient covering map if:

• f is a quotient map whose fibres are the orbits of G (i.e., it is a quotient map for the action of G)

• G acts by homeomorphims

• every point of E has a neighborhood whose translates by the group elements are pairwise disjoint

This is the definition IsQuotientCoveringMap. Included in the API for such maps are the following facts:

• Quotient covering maps are covering maps IsQuotientCoveringMap.isCoveringMap

• If G acts freely and properly discontinuously by homeomorphisms on a locally compact Hausdorff space then we have a quotient covering map Topology.IsQuotientMap.isQuotientCoveringMap_of_properlyDiscontinuousSMul.

• If E is simply connected and f is a quotient covering map, then the fundamental group of X is G, IsQuotientCoveringMap.fundamentalGroupEquiv.