Deck actions and monodromy transport

Deck transformations commute with transport between fibres by covering-space monodromy.

Main declaration

• TauCeti.Deck.monodromy_smul: deck transformations commute with monodromy along a path.

References

The proof specializes IsCoveringMap.fiberMap_monodromy to the continuous map underlying a deck transformation. It supplies the fibre-transport step of the regular-cover criterion.

@[simp]

theorem TauCeti.Deck.monodromy_smul {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {p : E → X} {x y : X} (hp : IsCoveringMap p) (γ : Path.Homotopic.Quotient x y) (φ : ↥(deck p)) (e : ↑(p ⁻¹' {x})) : hp.monodromy γ (φ • e) = φ • hp.monodromy γ e

Transport by covering-space monodromy commutes with the action of a deck transformation.

Both sides transport a point of the fibre over x to the fibre over y: one first applies the deck transformation and then lifts the path, while the other first lifts the path and then applies the deck transformation.