$[\omega]^n=[\omega_n]$ in $\pi_1(S^1)$

Declaration Hatcher.omegaClass_zpow. For every integer $n \in \mathbb{Z}$ (the only binder; there are no hypotheses and no typeclass assumptions beyond those fixed by the ambient types), the following equality holds in the group $\pi_1(S^1, 1)$:

where every symbol is defined as follows.

The space $S^1$ and its basepoint. $S^1$ denotes the unit circle, realised as the metric sphere $\{z \in \mathbb{C} : |z - 0| = 1\}$ inside $\mathbb{C}$, carrying the subspace topology and the commutative group structure given by complex multiplication (identity the complex number $1$, inverse $z \mapsto z^{-1}$). The basepoint is $1 \in S^1$. The map $\exp_{S^1} : \mathbb{R} \to S^1$ is $t \mapsto e^{it} = \cos t + i \sin t$; it is continuous.

The custom loops. Define the continuous map $c : \mathbb{R} \to S^1$ by

For an integer $n$, $\omega_n$ is the path in $S^1$ from $1$ to $1$ (a continuous map $[0,1] \to S^1$ sending $0 \mapsto 1$ and $1 \mapsto 1$) given by

where $n$ is regarded as a real number and $s \in [0,1] \subset \mathbb{R}$. (At $s = 0$ this is $e^{0} = 1$; at $s = 1$ it is $e^{2\pi i n} = 1$ because $n$ is an integer.) Separately, $\omega_{\mathrm{loop}}$ is the path from $1$ to $1$ given by $\omega_{\mathrm{loop}}(s) = c(s) = e^{2\pi i s}$; it is a distinct definition from $\omega_1$, though $\omega_1(s) = e^{2\pi i \cdot 1 \cdot s}$ has the same values.

The group $\pi_1(S^1,1)$ and the bracket. Two paths $p_0, p_1 : [0,1] \to S^1$ from $1$ to $1$ are called homotopic if there is a continuous $H : [0,1] \times [0,1] \to S^1$ with $H(0, s) = p_0(s)$ and $H(1, s) = p_1(s)$ for all $s$, and $H(t, 0) = p_0(0)$ and $H(t, 1) = p_0(1)$ for all $t$ (i.e. endpoints fixed throughout; here both endpoints are $1$). This is an equivalence relation, and $[\,p\,]$ denotes the equivalence class of the path $p$. The set $\pi_1(S^1, 1)$ is exactly the set of such classes of paths from $1$ to $1$ (formally: the endomorphisms of the object $1$ in the fundamental groupoid of $S^1$, whose morphisms $x \to y$ are homotopy classes of paths from $x$ to $y$; the conversion "from path class to group element" used on the right-hand side is the identity on this set). Its group structure is:

• identity $1 = [\,\mathrm{const}_1\,]$, the class of the constant path $s \mapsto 1$;
• product $P \cdot Q = [\,q \ast p\,]$ for representatives $p \in P$, $q \in Q$, where the concatenation $q \ast p$ is the path $s \mapsto q(2s)$ for $s \le \tfrac12$ and $s \mapsto p(2s - 1)$ for $s > \tfrac12$ — that is, the product $P \cdot Q$ traverses a representative of $Q$ first and then of $P$;
• inverse $P^{-1} = [\,\bar p\,]$ where $\bar p(s) = p(1 - s)$ is the reversed path.

Integer powers. For $P \in \pi_1(S^1,1)$ and $n \in \mathbb{Z}$, $P^{\,n}$ is the standard group power: $P^{0} = 1$, $P^{k+1} = P^{k} \cdot P$ for $k \ge 0$, and $P^{-(k+1)} = \bigl(P^{k+1}\bigr)^{-1}$ for $k \ge 0$. Unfolding the product and inverse above, for $k \ge 1$ the element $P^{k}$ is the class of a $k$-fold concatenation of a representative loop with itself (with the particular bracketing dictated by the recursion), and $P^{-k}$ is the class of the reversal of that concatenation.

The element $\omega$. $\omega$ is the element of $\pi_1(S^1, 1)$ defined as $\omega = [\,\omega_{\mathrm{loop}}\,]$, the homotopy class of the loop $s \mapsto e^{2\pi i s}$.

Statement, fully expanded. For every integer $n$ (including $n = 0$ and every negative $n$): the $n$-th power, in the group $\pi_1(S^1,1)$ described above, of the class of the loop $s \mapsto e^{2\pi i s}$ equals the homotopy class (endpoints fixed at $1$) of the single loop $s \mapsto e^{2\pi i n s}$ on $[0,1]$. In the case $n = 0$ the left side is the identity element $[\mathrm{const}_1]$ and the right side is the class of the loop $s \mapsto e^{0} = 1$, which is literally the constant loop. For $n < 0$ the right side is the class of the loop $s \mapsto e^{2\pi i n s}$, which traverses the circle in the clockwise direction $|n|$ times, while the left side is the inverse of the $|n|$-th power of $\omega$.