The acting group of a quotient covering map is its deck group

Let f : E → X be a quotient covering map for a group G acting on E, in the sense of Mathlib's IsQuotientCoveringMap. Every group element then acts on E by a homeomorphism over X, so translation gives a group homomorphism G →* Deck f.

This homomorphism is injective as soon as E is nonempty, because the action of a quotient covering map is free. It is surjective when E is preconnected: a deck transformation agrees at one point with some translation, and two deck transformations of a preconnected covering that agree at a point agree everywhere (and if E is empty there is nothing to prove). So for preconnected nonempty E the acting group is the deck group, G ≃* Deck f.

Neither hypothesis is needed to see that the deck action of a quotient covering map is regular; that consequence is recorded in TauCeti/AlgebraicTopology/UniversalCover/Deck/Quotient/Covering.lean, where it generalizes the previous statement for the acting group Deck f itself.

Main declarations

• TauCeti.Deck.IsQuotientCoveringMap.toDeckHom: translation by a group element, as a homomorphism from the acting group to the deck group.
• TauCeti.Deck.IsQuotientCoveringMap.toDeckHom_injective: it is injective on a nonempty total space.
• TauCeti.Deck.IsQuotientCoveringMap.toDeckHom_surjective: it is surjective on a preconnected total space.
• TauCeti.Deck.IsQuotientCoveringMap.toDeckHom_bijective: it is bijective on a preconnected nonempty total space.
• TauCeti.Deck.IsQuotientCoveringMap.deckMulEquiv: for a preconnected nonempty total space, the acting group is isomorphic to the deck group.

References

This supplies a prerequisite for the Tau Ceti universal-covers roadmap, Stage 1 and Stage 4: a cover presented as a quotient by a group action has that group as its deck group, which is how the deck group of a concrete cover such as Sⁿ → RPⁿ is computed. The quotient covering map API it consumes (Mathlib/Topology/Covering/Quotient.lean) is due to Junyan Xu. Surjectivity rests on uniqueness of lifts through a covering map, IsCoveringMap.eq_of_comp_eq in Mathlib/Topology/Covering/Basic.lean, due to Thomas Browning after Hatcher, Algebraic Topology, Proposition 1.34; it is used here through the Tau Ceti wrapper TauCeti.Deck.eq_of_apply_eq.

def TauCeti.Deck.IsQuotientCoveringMap.toDeckHom {E : Type u_1} {X : Type u_2} {G : Type u_3} [TopologicalSpace E] [TopologicalSpace X] {f : E → X} [Group G] [MulAction G E] (hf : IsQuotientCoveringMap f G) : G →* ↥(Deck f)

Translation by a group element, as a homomorphism from the group of a quotient covering map to the deck transformation group of that map. Each translation is a homeomorphism because the action is continuous, and it lies over the base because the fibres of f are the orbits.

Equations

• TauCeti.Deck.IsQuotientCoveringMap.toDeckHom hf = { toFun := fun (g : G) => ⟨Homeomorph.smul g, ⋯⟩, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem TauCeti.Deck.IsQuotientCoveringMap.toDeckHom_apply {E : Type u_1} {X : Type u_2} {G : Type u_3} [TopologicalSpace E] [TopologicalSpace X] {f : E → X} [Group G] [MulAction G E] (hf : IsQuotientCoveringMap f G) (g : G) (e : E) : ↑((toDeckHom hf) g) e = g • e

On points, the deck transformation attached to a group element is translation by that element.

@[simp]

theorem TauCeti.Deck.IsQuotientCoveringMap.toDeckHom_symm_apply {E : Type u_1} {X : Type u_2} {G : Type u_3} [TopologicalSpace E] [TopologicalSpace X] {f : E → X} [Group G] [MulAction G E] (hf : IsQuotientCoveringMap f G) (g : G) (e : E) : (↑((toDeckHom hf) g)).symm e = g⁻¹ • e

On points, the inverse of the deck transformation attached to a group element is translation by the inverse element.

theorem TauCeti.Deck.IsQuotientCoveringMap.toDeckHom_injective {E : Type u_1} {X : Type u_2} {G : Type u_3} [TopologicalSpace E] [TopologicalSpace X] {f : E → X} [Group G] [MulAction G E] (hf : IsQuotientCoveringMap f G) [Nonempty E] : Function.Injective ⇑(toDeckHom hf)

Passing from a group element to a deck transformation is injective, because the action of a quotient covering map is free.

theorem TauCeti.Deck.IsQuotientCoveringMap.toDeckHom_surjective {E : Type u_1} {X : Type u_2} {G : Type u_3} [TopologicalSpace E] [TopologicalSpace X] {f : E → X} [Group G] [MulAction G E] (hf : IsQuotientCoveringMap f G) [PreconnectedSpace E] : Function.Surjective ⇑(toDeckHom hf)

Every deck transformation of a quotient covering map with preconnected total space is translation by a group element: it agrees with one such translation at a point, and deck transformations of a preconnected covering are determined by one value.

theorem TauCeti.Deck.IsQuotientCoveringMap.toDeckHom_bijective {E : Type u_1} {X : Type u_2} {G : Type u_3} [TopologicalSpace E] [TopologicalSpace X] {f : E → X} [Group G] [MulAction G E] (hf : IsQuotientCoveringMap f G) [PreconnectedSpace E] [Nonempty E] : Function.Bijective ⇑(toDeckHom hf)

On a preconnected nonempty total space, passing from a group element to a deck transformation is bijective.

noncomputable def TauCeti.Deck.IsQuotientCoveringMap.deckMulEquiv {E : Type u_1} {X : Type u_2} {G : Type u_3} [TopologicalSpace E] [TopologicalSpace X] {f : E → X} [Group G] [MulAction G E] (hf : IsQuotientCoveringMap f G) [PreconnectedSpace E] [Nonempty E] : G ≃* ↥(Deck f)

The acting group of a quotient covering map with preconnected nonempty total space is its deck transformation group. The isomorphism is translation.

Equations

• TauCeti.Deck.IsQuotientCoveringMap.deckMulEquiv hf = MulEquiv.ofBijective (TauCeti.Deck.IsQuotientCoveringMap.toDeckHom hf) ⋯

@[simp]

theorem TauCeti.Deck.IsQuotientCoveringMap.deckMulEquiv_apply {E : Type u_1} {X : Type u_2} {G : Type u_3} [TopologicalSpace E] [TopologicalSpace X] {f : E → X} [Group G] [MulAction G E] (hf : IsQuotientCoveringMap f G) [PreconnectedSpace E] [Nonempty E] (g : G) (e : E) : ↑((deckMulEquiv hf) g) e = g • e

On points, the isomorphism between the acting group and the deck group is translation.

@[simp]

theorem TauCeti.Deck.IsQuotientCoveringMap.deckMulEquiv_symm_apply {E : Type u_1} {X : Type u_2} {G : Type u_3} [TopologicalSpace E] [TopologicalSpace X] {f : E → X} [Group G] [MulAction G E] (hf : IsQuotientCoveringMap f G) [PreconnectedSpace E] [Nonempty E] (φ : ↥(Deck f)) (e : E) : (deckMulEquiv hf).symm φ • e = ↑φ e

The inverse isomorphism returns the group element whose translation is the given deck transformation.