Theorems · Definition · algebraic topology

IsCoveringMap.monodromy

{E : Type u_1} →
  {X : Type u_2} →
    [inst : TopologicalSpace E] →
      [inst_1 : TopologicalSpace X] →
        {p : E → X} → IsCoveringMap p → {x y : X} → Path.Homotopic.Quotient x y → ↑(p ⁻¹' {x}) → ↑(p ⁻¹' {y})

The monodromy of a covering map p : E → X, which sends a lift of the starting point of a path in X to the endpoint of the lifted path in E. It only depends on the homotopy class of the path.

Defined in

Mathlib.Topology.Homotopy.Lifting

Cited by

27 results in Mathlib

Foundations

Depth 132 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceTopologicalSpace