$p(s)=(\cos 2\pi s,\sin 2\pi s)$ is a covering space of $S^1$

Proved

Hatcher.isCoveringMap_circleCover

by korbonits · Sep 4, 2026 · Mathlib 0df444a (Lean v4.33.1)

algebraic-topologycovering-spacesfundamental-grouphatcher

Let $p:\mathbb{R}\to S^1$ be Hatcher's map $p(s)=(\cos 2\pi s,\sin 2\pi s)=e^{2\pi i s}$ onto the unit circle. Then $p$ is a covering space of $S^1$ in Hatcher's sense: every point $x\in S^1$ has an open neighbourhood $U$ such that $p^{-1}(U)$ is a disjoint union of open subsets of $\mathbb{R}$ , each mapped homeomorphically onto $U$ by $p$ (such a $U$ is evenly covered). In symbols,

\forall x\in S^1\ \exists U\ni x \text{ open},\quad p^{-1}(U)=\bigsqcup_\alpha \tilde U_\alpha,\qquad p|_{\tilde U_\alpha}:\tilde U_\alpha\xrightarrow{\ \cong\ }U .

Hatcher records this as the observation that "any open arc in $S^1$ is evenly covered". It is the hypothesis under which the path- and homotopy-lifting properties are applied in the proof of Theorem 1.7, so it is the first brick of the computation $\pi_1(S^1)\cong\mathbb{Z}$ .

Formalization Note The covering-space condition is Mathlib's IsCoveringMap: for each $x$ , the fibre $p^{-1}\{x\}$ is discrete and $p$ is locally trivial over an open neighbourhood of $x$ with that fibre. This is equivalent to Hatcher's condition $(\ast)$ ; neither formulation requires $p$ to be surjective. Mathlib already knows Circle.isCoveringMap_exp; here the map is Circle.exp precomposed with $s\mapsto 2\pi s$ .

Preamble

import Definitions.Def_Hatcher_Circle
import Mathlib

open unitInterval Hatcher

Formal statement

namespace Hatcher
theorem isCoveringMap_circleCover : IsCoveringMap circleCover := by sorry
end Hatcher

Source

A. Hatcher, Algebraic Topology, Cambridge University Press 2002, https://pi.math.cornell.edu/~hatcher/AT/AT.pdf, Section 1.1, p. 29: definition (∗) of a covering space and the sentence 'for the previously defined map p : ℝ → S¹ any open arc in S¹ is evenly covered'

Read-back

What the Lean code literally says, in plain math · claude-fable-5-1

Declaration Hatcher.isCoveringMap_circleCover. The statement has no hypotheses and no free variables; it asserts a single closed proposition about one fixed map.

The map. Write $S^1$ for the unit circle in $\mathbb{C}$ , i.e. the set $\{z \in \mathbb{C} : \|z\| = 1\}$ , carrying the subspace topology inherited from $\mathbb{C}$ (this is Mathlib's Circle). The custom function $p : \mathbb{R} \to S^1$ (called circleCover in the code) is defined for every real $s$ by

p(s) \;=\; \exp\bigl(2\pi s \cdot i\bigr) \;=\; \cos(2\pi s) + i\,\sin(2\pi s),

where $\pi$ is the real number $\pi$ and the value is regarded as a point of $S^1$ . (Concretely, $p(s)$ is Mathlib's Circle.exp applied to the real number $2\pi s$ , and Circle.exp t is the point $e^{t i}$ of the unit circle.) The domain $\mathbb{R}$ carries its usual topology.

The assertion. The theorem states that $p$ is a covering map in the following precise sense (Mathlib's IsCoveringMap): for every point $x \in S^1$ , the point $x$ is evenly covered by $p$ with fibre indexed by the set $p^{-1}(\{x\}) \subseteq \mathbb{R}$ , meaning that all of the following hold:

the set $p^{-1}(\{x\}) = \{ s \in \mathbb{R} : p(s) = x \}$ , given the subspace topology from $\mathbb{R}$ , is a discrete topological space; and
there exists a subset $U \subseteq S^1$ $U \subseteq S^{1}$ such that
- $x \in U$ ,
- $U$ is open in $S^1$ ,
- the preimage $p^{-1}(U) \subseteq \mathbb{R}$ is open in $\mathbb{R}$ , and
- there exists a homeomorphism

H : p^{-1}(U) \;\xrightarrow{\;\cong\;}\; U \times p^{-1}(\{x\})

(where $p^{-1}(U)$ has the subspace topology from $\mathbb{R}$, $U$ the subspace topology from $S^1$, $p^{-1}(\{x\})$ the subspace topology from $\mathbb{R}$, and the right-hand side the product topology) such that for every $y \in p^{-1}(U)$, the first coordinate of $H(y)$, viewed as a point of $S^1$, equals $p(y)$; i.e. $H$ commutes with the projections to $U$.

Notes on what is and is not said.

The fibre type used in the local trivialisation is specifically the preimage of the single point $\{x\}$ under $p$ , not an arbitrary discrete space; it is required to be discrete but is not required to be nonempty, and its cardinality is not specified.
Nothing is asserted about $p$ being surjective, continuous, or a local homeomorphism as separate claims; only the pointwise even-covering condition above is asserted, for every $x \in S^1$ .
The statement quantifies over all points of $S^1$ ; since $S^1$ is nonempty, the claim is not vacuous.
The proof of the declaration is omitted (sorry); the read-back describes only the statement.

Human review

Endorsed by Shuze Chen · Sep 5, 2026
Endorsed by korbonits · Sep 5, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

p(s)=(cos⁡2πs,sin⁡2πs)p(s)=(\cos 2\pi s,\sin 2\pi s)p(s)=(cos2πs,sin2πs) is a covering space of S1S^1S1

$p(s)=(\cos 2\pi s,\sin 2\pi s)$ is a covering space of $S^1$