Motivation

The fundamental group $\pi_1(X, x_0)$ is the first algebraic invariant a student of topology meets, and $\pi_1(S^1)\cong\mathbb{Z}$ is the first computation of it that carries real content. Allen Hatcher's Algebraic Topology (Cambridge University Press, 2002; freely available at pi.math.cornell.edu/~hatcher/AT/AT.pdf) is the standard text on the subject. Its Chapter 1 opens with exactly this computation (Theorem 1.7, p. 29) and immediately draws three classical consequences from it: the Fundamental Theorem of Algebra (Theorem 1.8), the Brouwer fixed point theorem for the disk (Theorem 1.9), and the Borsuk–Ulam theorem for the sphere (Theorem 1.10).

This mission is the opening entry in a series that formalizes Hatcher's book capstone by capstone. It covers the subsection "The Fundamental Group of the Circle" of Section 1.1 (pp. 29–33): the covering-space lifting properties that drive the proof, the theorem itself, and its three applications. Later entries in the series (van Kampen's theorem, the classification of covering spaces, simplicial and singular homology) will build on the declarations introduced here, which all live in the shared Lean namespace Hatcher.

Setting

A path in a topological space $X$ is a continuous map $f : I \to X$, where $I = [0,1]$. A homotopy of paths is a family $f_t : I \to X$, $0 \le t \le 1$, such that the endpoints $f_t(0) = x_0$ and $f_t(1) = x_1$ are independent of $t$ and the associated map $F : I \times I \to X$, $F(s,t) = f_t(s)$, is continuous. A loop at a basepoint $x_0$ is a path with $f(0) = f(1) = x_0$. The set of homotopy classes $[f]$ of loops at $x_0$ is the fundamental group $\pi_1(X, x_0)$; its product is $[f][g] = [f\cdot g]$, where $f\cdot g$ traverses $f$ and then $g$, each at double speed (Hatcher, Proposition 1.3).

The circle $S^1 \subset \mathbb{R}^2$ is realised as the unit circle of $\mathbb{C}$, so the point $(\cos\theta, \sin\theta)$ is $e^{i\theta}$ and the basepoint $(1,0)$ is $1$. Hatcher's map

$$p : \mathbb{R} \to S^1, \qquad p(s) = (\cos 2\pi s, \sin 2\pi s) = e^{2\pi i s}$$

is Hatcher.circleCover. The loops

$$\omega_n(s) = (\cos 2\pi n s, \sin 2\pi n s) = p(ns), \qquad n \in \mathbb{Z},$$

based at $(1,0)$ are Hatcher.omegaLoopN n, and $\omega = \omega_1$ is Hatcher.omegaLoop; its class $[\omega] \in \pi_1(S^1, 1)$ is Hatcher.omegaClass.

A covering space of $X$ is a space $\tilde X$ together with a map $p : \tilde X \to X$ such that every $x \in X$ has an open neighbourhood $U$ for which $p^{-1}(U)$ is a disjoint union of open sets each mapped homeomorphically onto $U$ by $p$ (Hatcher's condition $(\ast)$, p. 29; such a $U$ is evenly covered). A lift of a map $f : Y \to X$ is a map $\tilde f : Y \to \tilde X$ with $p \circ \tilde f = f$.

Formalization targets

Goal (Theorem 1.7)

$\pi_1(S^1, 1)$ is an infinite cyclic group generated by $[\omega]$. In the form stated in Lean:

$$\forall\, g \in \pi_1(S^1, 1)\quad \exists!\, n \in \mathbb{Z}:\quad [\omega]^n = g.$$

Surjectivity of $n \mapsto [\omega]^n$ says $[\omega]$ generates; uniqueness of $n$ says the group is infinite cyclic rather than finite.

Milestones on the road to the goal

1. $p(s) = e^{2\pi i s}$ is a covering space of $S^1$ (Hatcher, p. 29).
2. Homotopy lifting property (c): for a covering space $p : \tilde X \to X$, a map $F : Y \times I \to X$ and a lift of $F|_{Y \times \{0\}}$ extend uniquely to a lift of $F$ (p. 30).
3. Path lifting property (a): a path $f$ starting at $x_0$ and a point $\tilde x_0 \in p^{-1}(x_0)$ determine a unique lift $\tilde f$ starting at $\tilde x_0$ (p. 29).
4. Lifting homotopies of paths (b): a homotopy of paths $f_t$ starting at $x_0$ lifts uniquely to a homotopy of paths $\tilde f_t$ starting at $\tilde x_0$ (p. 29).
5. Every loop in $S^1$ at $(1,0)$ is homotopic to $\omega_n$ for a unique $n \in \mathbb{Z}$ (the reformulation of Theorem 1.7 that Hatcher actually proves, p. 29).
6. $[\omega]^n = [\omega_n]$ for every $n \in \mathbb{Z}$ (Hatcher's remark after Theorem 1.7, p. 29).

Applications (Theorems 1.8–1.10)

$$\text{Every nonconstant } f \in \mathbb{C}[z] \text{ has a root in } \mathbb{C}.$$ $$\text{Every continuous } h : D^2 \to D^2 \text{ has a fixed point.}$$ $$\text{Every continuous } f : S^2 \to \mathbb{R}^2 \text{ satisfies } f(x) = f(-x) \text{ for some } x \in S^2.$$

Significance

The result itself. The computation $\pi_1(S^1) \cong \mathbb{Z}$ assigns to every loop in the circle an integer, its winding number, and shows that this integer is the only homotopy invariant of the loop. It is the seed of degree theory, and in Hatcher's text it is the starting point for every later computation of fundamental groups (products, van Kampen, covering spaces). The three applications are the standard demonstration that a single algebraic invariant can settle purely geometric or algebraic existence questions.

Formalizing it. Mathlib (revision 0df444a) already contains the covering-space infrastructure: IsCoveringMap, path lifting (IsCoveringMap.liftPath, eq_liftPath_iff'), homotopy lifting (IsCoveringMap.liftHomotopy, eq_liftHomotopy_iff'), monodromy, and the fact that Circle.exp is a covering map (Circle.isCoveringMap_exp). It also has FundamentalGroup X x as the endomorphism group of the fundamental groupoid. It does not contain the computation $\pi_1(S^1) \cong \mathbb{Z}$, nor the two-dimensional Brouwer and Borsuk–Ulam theorems. The Fundamental Theorem of Algebra is in Mathlib as Complex.exists_root (proved by Liouville's theorem rather than by Hatcher's argument); it is kept as a milestone because it is one of the section's stated theorems, and a solver may close it directly from Mathlib. Milestones 2–4 are also within reach of the existing lifting API, but they are the lemmas Hatcher states and uses, and a faithful record of them in the mission's own namespace is what later entries in the series will import.

Difficulty

The obvious first idea for the goal is to define the winding number of a loop through the complex argument. That fails because $\arg$ is discontinuous on $S^1$; the integer has to be produced by lifting the loop through $p$ and reading off the endpoint of the lift, which is only well defined because of the uniqueness in the path lifting property. The second difficulty is uniqueness of $n$: this needs lifting of homotopies (milestone 4), not just of paths, together with the observation that a lifted homotopy of paths has constant endpoints.

Connecting the concrete loops to Mathlib's abstract $\pi_1$ is its own obstacle. FundamentalGroup Circle 1 multiplies by composing morphisms of the fundamental groupoid, so identifying $[\omega]^n$ with the class of the explicit loop $\omega_n$ (milestone 6) requires reparametrization arguments for concatenated paths, for negative $n$ as well as positive.

For Theorem 1.9 the difficulty is the construction and continuity of the retraction $r : D^2 \to S^1$ from a fixed-point-free map, and then the non-existence of a retraction, which uses that $\pi_1(S^1) \neq 0$. For Theorem 1.10 Hatcher's proof lifts a loop $g(s) = f(\cos 2\pi s, \sin 2\pi s)/\lvert \cdots \rvert$ through $p$ and shows the lift changes by an odd integer over half a turn; making that parity argument rigorous in Lean is the substance of the milestone.

Formalization scope

• $S^1$ is Circle (the unit circle in $\mathbb{C}$) with basepoint 1; $D^2$ is Metric.closedBall (0 : EuclideanSpace ℝ (Fin 2)) 1; $S^2$ is Metric.sphere (0 : EuclideanSpace ℝ (Fin 3)) 1, with $-x$ the antipodal point.
• A covering space is Mathlib's IsCoveringMap p. This agrees with Hatcher's condition $(\ast)$; neither requires $p$ to be surjective.
• Paths are continuous maps C(I, X) or Mathlib Paths; for homotopies of paths, the square is written I × I with Hatcher's coordinate order $F(s,t) = f_t(s)$: the first coordinate is the path parameter, the second the homotopy parameter. In the general homotopy lifting property the domain is Y × I with $Y$ an arbitrary topological space, as in Hatcher.
• $\pi_1(S^1, 1)$ is Mathlib's FundamentalGroup Circle 1, and $[\omega]$ is FundamentalGroup.fromPath ⟦omegaLoop⟧. Because the goal quantifies over integer powers of a single element, the order of multiplication in FundamentalGroup is immaterial to its truth.
• The goal is stated as $\forall g\, \exists! n,\ [\omega]^n = g$ rather than as an abstract isomorphism with $\mathbb{Z}$, so that the generator is pinned to Hatcher's explicit loop; an isomorphism FundamentalGroup Circle 1 ≃* Multiplicative ℤ sending $[\omega]$ to $1$ is an immediate corollary and a welcome contribution.
• "Nonconstant polynomial" is 0 < f.degree, which excludes both the zero polynomial and nonzero constants.

Contributions welcome: proofs of the milestones from Mathlib's lifting API, a degree homomorphism $\pi_1(S^1,1) \to \mathbb{Z}$ packaged for reuse, and any lemma about concatenation and reparametrization of loops in Circle that later chapters of the series can import.

Selected references

• A. Hatcher, Algebraic Topology, Cambridge University Press, 2002. Section 1.1, "The Fundamental Group of the Circle", pp. 29–33. https://pi.math.cornell.edu/~hatcher/AT/AT.pdf
• L. E. J. Brouwer, Über Abbildung von Mannigfaltigkeiten, Mathematische Annalen 71 (1911), 97–115. https://doi.org/10.1007/BF01456931
• K. Borsuk, Drei Sätze über die n-dimensionale euklidische Sphäre, Fundamenta Mathematicae 20 (1933), 177–190. https://doi.org/10.4064/fm-20-1-177-190
• Mathlib, Mathlib/Topology/Homotopy/Lifting.lean (path and homotopy lifting for covering maps). https://github.com/leanprover-community/mathlib4/blob/0df444a360eaa60ab8c11dca51a86af692955474/Mathlib/Topology/Homotopy/Lifting.lean
• Mathlib, Mathlib/AlgebraicTopology/FundamentalGroupoid/FundamentalGroup.lean (the fundamental group). https://github.com/leanprover-community/mathlib4/blob/0df444a360eaa60ab8c11dca51a86af692955474/Mathlib/AlgebraicTopology/FundamentalGroupoid/FundamentalGroup.lean