Every loop in $S^1$ at $(1,0)$ is homotopic to $\omega_n$ for a unique $n$

Declaration Hatcher.loop_homotopic_omegaLoopN.

Throughout, $S^1$ denotes the type Circle from Mathlib: the set of complex numbers $z$ with $\lVert z - 0\rVert = 1$, i.e. $\{z \in \mathbb{C} : |z| = 1\}$, carrying the subspace topology (and metric) inherited from $\mathbb{C}$ and the multiplicative group structure of $\mathbb{C}$; its identity element $1$ is the complex number $1$. Mathlib's Circle.exp is the continuous map $\mathbb{R} \to S^1$, $t \mapsto e^{\,t\,i}$ (complex exponential of $t\cdot i$). The custom definition circleCover from the bundle is

$I$ denotes unitInterval, the closed real interval $[0,1] = \{s \in \mathbb{R} : 0 \le s \le 1\}$ viewed as a subspace of $\mathbb{R}$.

A path from $1$ to $1$ in $S^1$ (Path (1 : Circle) 1) is a continuous function $\gamma : [0,1] \to S^1$ together with the two equations $\gamma(0) = 1$ and $\gamma(1) = 1$. For each integer $n \in \mathbb{Z}$, the custom definition omegaLoopN n is the path from $1$ to $1$ in $S^1$ whose underlying function is

where $n$ is cast from $\mathbb{Z}$ to $\mathbb{R}$ and $s \in [0,1]$ is used as a real number; the endpoint equations are $\omega_n(0) = e^{0} = 1$ and $\omega_n(1) = e^{2\pi i n} = 1$. In particular $\omega_0$ is the constant path at $1$, and for negative $n$ the exponent $2\pi i n s$ has negative imaginary part (so $\omega_{-1}(s) = e^{-2\pi i s}$, etc.).

For two paths $p_0, p_1$ from $1$ to $1$ in $S^1$, "$p_0$ is homotopic to $p_1$" (Path.Homotopic, i.e. Nonempty (Path.Homotopy p₀ p₁)) means: there exists a continuous map

such that

• $H(0, s) = p_0(s)$ for every $s \in [0,1]$;
• $H(1, s) = p_1(s)$ for every $s \in [0,1]$;
• for every $t \in [0,1]$ and every $s \in \{0, 1\}$, $H(t, s) = p_0(s)$ — i.e. $H(t,0) = p_0(0) = 1$ and $H(t,1) = p_0(1) = 1$ for all $t$ (the homotopy fixes both endpoints at $1$, relative to $\{0,1\}$).

This is Mathlib's ContinuousMap.HomotopyRel of the underlying continuous maps relative to the set $\{0,1\} \subseteq [0,1]$; no further condition (e.g. on the intermediate paths beyond fixed endpoints) is imposed.

The statement. For every path $f$ from $1$ to $1$ in $S^1$ (that is, every continuous $f : [0,1] \to S^1$ with $f(0) = 1$ and $f(1) = 1$), there exists exactly one integer $n \in \mathbb{Z}$ such that $f$ is homotopic to $\omega_n$ in the above sense. Spelled out, "exactly one" (∃!) unfolds literally as

where $f \simeq \gamma$ abbreviates "there is an endpoint-fixing homotopy $H : [0,1]\times[0,1] \to S^1$ from $f$ to $\gamma$ as described above". The only hypothesis is that $f$ is a path from $1$ to $1$ in $S^1$; there are no other explicit variables, implicit arguments, or typeclass assumptions in the statement (the topological structure on $S^1$ and $[0,1]$ is the fixed Mathlib one). The quantifier over $n$ ranges over all of $\mathbb{Z}$, including $n = 0$ (the constant loop) and negative values. The declaration lives in the namespace Hatcher; in the given file its proof is left as sorry (not supplied).