The exponential covering sends the winding-one loop to the deck translation 2πi

Proved

BraidsLinksMCG.complex_exp_winding_one_deck_translation

by WillR · Sep 28, 2026 · Mathlib 0df444a (Lean v4.33.1)

Let exp : ℂ → {z : ℂ // z ≠ 0} be the complex exponential, viewed as a covering map whose deck group is AddSubgroup.zmultiples (2 * Real.pi * Complex.I), the additive subgroup of ℂ generated by 2πi. Let expWindingLoop be the counterclockwise circle of radius one about the origin, based at the point 1, and let expFibreBase be the point 0 of the fibre over 1 (since exp 0 = 1).

Then the monodromy of the loop class of expWindingLoop, measured as an element of the deck group, is exactly one step of that subgroup: the element 2πi itself, and not a multiple k · 2πi for some other integer k.

Concretely, the lift of expWindingLoop that starts at the fibre point 0 is the straight line segment s ↦ 2 * Real.pi * s * Complex.I from 0 to 2πi; lifting the loop once around the origin advances the starting point of the lift by exactly one deck translation, which is the assertion.

Preamble

import Mathlib
import Definitions.Def_exp_covering_helpers

Formal statement

namespace BraidsLinksMCG

open scoped Topology

/-- Under the exponential covering `Complex.exp : ℂ → {z : ℂ // z ≠ 0}`, the loop
`expWindingLoop` (one counterclockwise turn about the origin, based at `1`) has
deck translation exactly one step of the deck group `AddSubgroup.zmultiples`,
namely the element `2 * π·i`.

The lift of `expWindingLoop` starting at the fibre point `0` is the straight segment
`s ↦ 2 * Real.pi * s * Complex.I`, which runs from `0` to `2 * Real.pi * Complex.I`.
-/
theorem complex_exp_winding_one_deck_translation :
    Complex.isAddQuotientCoveringMap_exp.fundamentalGroupToMulOpposite expFibreBase
      (FundamentalGroup.fromPath (Path.Homotopic.Quotient.mk expWindingLoop)) =
      MulOpposite.op ((1 : ℤ) • (⟨2 * Real.pi * Complex.I, AddSubgroup.mem_zmultiples (2 * Real.pi * Complex.I)⟩ : AddSubgroup.zmultiples (2 * Real.pi * Complex.I))) := by sorry

end BraidsLinksMCG

View graph