Deck transformations

For a map p : E → X, the deck transformation group deck p is the subgroup of E ≃ₜ E consisting of self-homeomorphisms h with p ∘ h = p. No topology on X or continuity of p is assumed.

The definition is stated for an arbitrary p; no IsCoveringMap hypothesis is needed for the basic group structure or the canonical action. Theorems characterising deck transformations via path lifting (when p is a covering map of a path-connected, locally path-connected base) belong to follow-up files.

Main definitions

• deck p: the subgroup of E ≃ₜ E consisting of homeomorphisms commuting with p.

Main results

• deck p is a Group, acts on E via MulAction, the action is faithful and continuous in the second variable; these all follow automatically from the Subgroup-action transfers together with Homeomorph.applyMulAction.
• deck.proj_smul: deck transformations commute with p.

def deck {E : Type u_1} {X : Type u_2} [TopologicalSpace E] (p : E → X) : Subgroup (E ≃ₜ E)

The deck transformation group of a map p : E → X: the subgroup of self-homeomorphisms of E commuting with p.

Equations

• deck p = { carrier := {h : E ≃ₜ E | p ∘ ⇑h = p}, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }

theorem deck.mem_iff {E : Type u_1} {X : Type u_2} [TopologicalSpace E] {p : E → X} {h : E ≃ₜ E} : h ∈ deck p ↔ p ∘ ⇑h = p

@[simp]

theorem deck.comp_eq {E : Type u_1} {X : Type u_2} [TopologicalSpace E] {p : E → X} (h : ↥(deck p)) : p ∘ ⇑↑h = p

theorem deck.proj_smul {E : Type u_1} {X : Type u_2} [TopologicalSpace E] {p : E → X} (h : ↥(deck p)) (e : E) : p (h • e) = p e

instance deck.instContinuousConstSMulSubtypeHomeomorphMemSubgroup {E : Type u_1} {X : Type u_2} [TopologicalSpace E] {p : E → X} : ContinuousConstSMul (↥(deck p)) E