Theorem 1.7: $\pi_1(S^1)$ is infinite cyclic generated by $[\omega]$

Declaration Hatcher.fundamentalGroup_circle.

Statement. For every element $g$ of $\pi_1(S^1, 1)$ (the fundamental group of the space Circle at the basepoint $1$, as spelled out below), there exists exactly one integer $n \in \mathbb{Z}$ such that

$$\omega^{\,n} = g,$$

where $\omega$ is the specific element of $\pi_1(S^1,1)$ defined below. "Exactly one" is the literal expansion of $\exists!$: there is some $n \in \mathbb{Z}$ with $\omega^n = g$, and every $m \in \mathbb{Z}$ with $\omega^m = g$ satisfies $m = n$. The only binder is $g$; there are no further hypotheses on $g$, and no typeclass or side assumptions beyond the fixed structures described below.

The space $S^1$ (Mathlib Circle). The set $\{ z \in \mathbb{C} : \lVert z - 0 \rVert = 1 \}$, the unit sphere in $\mathbb{C}$, carrying the subspace topology from $\mathbb{C}$ and the commutative group structure given by complex multiplication. Its identity element $1$ is the complex number $1$, and this is the basepoint used throughout.

The map $\exp_{S^1}$ (Mathlib Circle.exp). The continuous map $\mathbb{R} \to S^1$, $t \mapsto e^{it} = \cos t + i \sin t$ (as an element of $\mathbb{C}$ of norm $1$).

Custom definition $c$ (circleCover). $c : \mathbb{R} \to S^1$ is $c(s) = \exp_{S^1}(2\pi s) = e^{2\pi i s}$.

Paths and loops. A path in a topological space $X$ from $x$ to $y$ is a continuous map $\gamma : [0,1] \to X$ (with $[0,1] = \{ t \in \mathbb{R} : 0 \le t \le 1 \}$) such that $\gamma(0) = x$ and $\gamma(1) = y$. A loop at $x$ is a path from $x$ to $x$.

Custom definition $\omega_0$ (omegaLoop). $\omega_0$ is the loop at $1$ in $S^1$ given by

$$\omega_0(s) = c(s) = e^{2\pi i s}, \qquad s \in [0,1],$$

with the endpoint conditions $\omega_0(0) = e^{0} = 1$ and $\omega_0(1) = e^{2\pi i} = 1$.

Homotopy of paths and the quotient $\llbracket \cdot \rrbracket$. Two paths $p_0, p_1$ from $x$ to $y$ are called homotopic when there is a continuous $H : [0,1] \times [0,1] \to X$ with $H(0, s) = p_0(s)$ and $H(1, s) = p_1(s)$ for all $s$, and such that for every $t \in [0,1]$ the intermediate path $H(t,\cdot)$ agrees with $p_0$ on the set $\{0, 1\}$, i.e. $H(t,0) = p_0(0) = x$ and $H(t,1) = p_0(1) = y$ (endpoints fixed). This is an equivalence relation, and $\llbracket p \rrbracket$ denotes the equivalence class of $p$ in the quotient of the set of paths from $x$ to $y$ by this relation.

The fundamental group $\pi_1(X, x)$ (Mathlib FundamentalGroup X x). By definition this is the set of endomorphisms of the object $x$ in Mathlib's fundamental groupoid of $X$, which is literally the set of homotopy classes $\llbracket \gamma \rrbracket$ of loops $\gamma$ at $x$ (the construction FundamentalGroup.fromPath is the identity map from this set of classes to $\pi_1(X,x)$). Its group structure is:

• identity: $1 = \llbracket \mathrm{const}_x \rrbracket$, the class of the constant loop $s \mapsto x$;
• product: $p \cdot q = q \ast p$, where for loops $\gamma, \gamma'$ the concatenation $\gamma \ast \gamma'$ is the loop

$$(\gamma \ast \gamma')(t) = \begin{cases} \gamma(2t) & t \le \tfrac12 \\ \gamma'(2t - 1) & t > \tfrac12 \end{cases}$$

(descended to classes); so $\llbracket \gamma \rrbracket \cdot \llbracket \gamma' \rrbracket = \llbracket \gamma' \ast \gamma \rrbracket$ — the product traverses the right-hand factor first, then the left-hand factor;

• inverse: $\llbracket \gamma \rrbracket^{-1} = \llbracket \bar\gamma \rrbracket$ where $\bar\gamma(t) = \gamma(1 - t)$.

Integer powers. For $a \in \pi_1(X,x)$ and $n \in \mathbb{Z}$, $a^n$ is the standard group power determined by $a^0 = 1$, $a^{k+1} = a^k \cdot a$ for $k \in \mathbb{N}$, and $a^{-(k+1)} = \left(a^{k+1}\right)^{-1}$ for $k \in \mathbb{N}$. In particular $a^0$ is the class of the constant loop, $a^1 = a$, and negative powers are inverses of positive powers.

Custom definition $\omega$ (omegaClass). $\omega \in \pi_1(S^1, 1)$ is the homotopy class of the loop $\omega_0$:

$$\omega = \llbracket\, s \mapsto e^{2\pi i s} \,\rrbracket .$$

Fully expanded claim. For every homotopy class $g$ of loops at $1$ in the unit circle $\{z \in \mathbb{C} : |z| = 1\}$ (loops being continuous $\gamma : [0,1] \to S^1$ with $\gamma(0)=\gamma(1)=1$, homotopies keeping both endpoints at $1$), there is exactly one integer $n$ such that the $n$-th group power (in the sense above, with $n = 0$ giving the constant-loop class and $n < 0$ giving the inverse of the $|n|$-th power) of the class of $s \mapsto e^{2\pi i s}$ equals $g$. Equality here is equality of homotopy classes, i.e. some representative of $\omega^n$ is homotopic (rel endpoints) to some representative of $g$.

Edge cases made explicit. The quantifier over $g$ includes the identity class $g = 1$; for it, the statement asserts $\omega^n = 1$ holds for exactly one integer $n$ (this includes, as part of the uniqueness clause, that $\omega^m \ne 1$ for every $m \ne$ that unique $n$). The statement is made only at the basepoint $1 \in S^1$. The other declarations in the definitions bundle (omegaLoopN, circleCover_zero, circleCover_intCast, omegaLoopN_one, continuous_circleCover) are not referenced by the theorem statement and play no role in what it asserts.