Read-back: Def_Hatcher_Circle bundle

All declarations live in a namespace called Hatcher and depend only on Mathlib. Throughout, the following Mathlib notions are used and are expanded here once so that each paragraph below can refer back to them.

• The circle. Circle is the type of complex numbers of norm one, $S^1 = \{ z \in \mathbb{C} : \lVert z \rVert = 1 \}$ (formally, the metric sphere in $\mathbb{C}$ of radius $1$ centred at $0$), carrying the subspace topology from $\mathbb{C}$ and the multiplicative commutative group structure inherited from $\mathbb{C}$; its identity element $1$ is the complex number $1$.
• The exponential onto the circle. Circle.exp is the continuous map $\mathbb{R} \to S^1$, $t \mapsto e^{it}$ (formally the complex number $\exp(t \cdot i)$ together with a proof that it has norm one).
• The unit interval. unitInterval, written $I$ below, is the subset $[0,1] = \{ x \in \mathbb{R} : 0 \le x \le 1 \}$ of the reals, viewed as a topological space with the subspace topology. An element $s \in I$ is, when used in a real-number expression, silently replaced by its underlying real number.
• Paths. For points $x, y$ of a topological space $X$, a Path x y is a continuous map $\gamma : I \to X$ together with proofs that $\gamma(0) = x$ and $\gamma(1) = y$. A path from $x$ to $x$ is a loop based at $x$.
• Path homotopy and its quotient. Two paths $\gamma_0, \gamma_1$ from $x$ to $y$ are homotopic (Path.Homotopic) if there exists a continuous map $F : I \times I \to X$ with $F(0, s) = \gamma_0(s)$, $F(1, s) = \gamma_1(s)$ for all $s$, and $F(t, 0) = \gamma_0(0) = x$, $F(t, 1) = \gamma_0(1) = y$ for all $t$ (endpoints fixed throughout). This is an equivalence relation, and Path.Homotopic.Quotient x y is the set of equivalence classes. The bracket $\llbracket \gamma \rrbracket$ (written ⟦γ⟧ in the code) denotes the equivalence class of the path $\gamma$ in this quotient.
• Fundamental group. FundamentalGroup X x is defined as the set of endomorphisms of the object $x$ in Mathlib's fundamental groupoid of $X$; concretely its underlying set is exactly Path.Homotopic.Quotient x x, the set of homotopy classes of loops based at $x$. Its group structure is: identity $=$ the class of the constant loop at $x$; product $p \cdot q$ $=$ the class of the concatenation "first traverse $q$, then $p$" (note the order); inverse $=$ the class of the reversed loop. FundamentalGroup.fromPath is the map Path.Homotopic.Quotient x x → FundamentalGroup X x that sends a homotopy class of loops to itself regarded as an element of the fundamental group (it is definitionally the identity; it only changes the type label).

The Lean symbol π here is the real number $\pi$ (from the Real namespace, which is opened).

---

circleCover (definition)

For every real number $s \in \mathbb{R}$, this defines an element of the circle $S^1$ by

$$\operatorname{circleCover}(s) \;:=\; \operatorname{Circle.exp}(2 \pi s) \;=\; e^{2 \pi i s} \in S^1 .$$

Here $2 \pi s$ is the real product $2 \cdot \pi \cdot s$ and $\operatorname{Circle.exp}$ is the map $t \mapsto e^{it}$ described above. This is a total function $\mathbb{R} \to S^1$ with no restrictions on $s$ (it is marked noncomputable, which has no mathematical content).

continuous_circleCover (theorem)

Asserts that the function $\operatorname{circleCover} : \mathbb{R} \to S^1$, $s \mapsto e^{2\pi i s}$, is continuous, where $\mathbb{R}$ has its usual topology and $S^1$ has the subspace topology from $\mathbb{C}$. There are no hypotheses.

circleCover_zero (theorem)

Asserts the single equation

$$\operatorname{circleCover}(0) = 1 ,$$

i.e. $e^{2\pi i \cdot 0} = 1$, where $0$ is the real number zero and $1$ is the identity element of the group $S^1$ (the complex number $1$). No hypotheses.

circleCover_intCast (theorem)

For every integer $n \in \mathbb{Z}$, asserts

$$\operatorname{circleCover}(n) = 1 ,$$

where on the left $n$ is regarded as a real number (via the canonical inclusion $\mathbb{Z} \hookrightarrow \mathbb{R}$), so the claim is $e^{2 \pi i n} = 1$ in $S^1$ for every integer $n$, including $n = 0$ and negative $n$. No further hypotheses.

omegaLoopN (definition)

For every integer $n \in \mathbb{Z}$, this defines a loop in $S^1$ based at $1$, i.e. an element of Path (1 : Circle) 1, denoted here $\omega_n$. Its underlying function $I \to S^1$ is

$$\omega_n(s) \;:=\; \operatorname{circleCover}(n \cdot s) \;=\; e^{2 \pi i\, n s}, \qquad s \in [0,1],$$

where $n \cdot s$ is the real product of $n$ (cast to $\mathbb{R}$) with the real number underlying $s \in I$. The definition packages, in addition to this function:

• a proof that $s \mapsto e^{2\pi i n s}$ is continuous on $I$;
• a proof that $\omega_n(0) = 1$ (the start point is the identity element of $S^1$);
• a proof that $\omega_n(1) = 1$ (the end point is the identity element of $S^1$).

Note that $n = 0$ is allowed, in which case $\omega_0$ is the constant loop at $1$; negative $n$ are also allowed.

omegaLoop (definition)

Defines a loop in $S^1$ based at $1$ (an element of Path (1 : Circle) 1), denoted here $\omega$, whose underlying function is

$$\omega(s) \;:=\; \operatorname{circleCover}(s) \;=\; e^{2 \pi i s}, \qquad s \in [0,1],$$

where $s \in I$ is used via its underlying real number. Packaged with it are proofs that this function is continuous on $I$, that $\omega(0) = 1$, and that $\omega(1) = 1$ (the last obtained from circleCover_intCast with $n = 1$). Note that $\omega$ is defined directly and not as $\omega_1$; the relationship between the two is a separate theorem below.

omegaLoopN_apply (theorem)

For every integer $n \in \mathbb{Z}$ and every point $s \in I = [0,1]$, asserts

$$\omega_n(s) = \operatorname{circleCover}(n \cdot s) \;\bigl(= e^{2\pi i n s}\bigr),$$

where $\omega_n$ is the loop defined by omegaLoopN evaluated at $s$. This holds by definition (the proof is rfl); the statement records how the loop evaluates pointwise.

omegaLoop_apply (theorem)

For every point $s \in I = [0,1]$, asserts

$$\omega(s) = \operatorname{circleCover}(s) \;\bigl(= e^{2\pi i s}\bigr),$$

where $\omega$ is the loop defined by omegaLoop. Again this holds by definition.

omegaLoopN_one (theorem)

Asserts the equality of loops

$$\omega_1 = \omega ,$$

i.e. the loop omegaLoopN 1 (with underlying function $s \mapsto e^{2 \pi i \cdot (1 \cdot s)}$, where $1$ is the integer one cast to $\mathbb{R}$) is equal, as an element of Path (1 : Circle) 1, to the loop omegaLoop (with underlying function $s \mapsto e^{2 \pi i s}$). Equality of paths here means equality of the underlying functions $I \to S^1$ at every point $s \in I$ (the endpoint proofs carry no data). No hypotheses.

omegaClass (definition)

Defines an element of the fundamental group of $S^1$ at the basepoint $1$, i.e. of FundamentalGroup Circle 1, by

$$\operatorname{omegaClass} \;:=\; \operatorname{FundamentalGroup.fromPath}\bigl(\llbracket \omega \rrbracket\bigr),$$

where $\llbracket \omega \rrbracket$ is the homotopy class (relative to the fixed endpoints $0, 1 \in I$) of the loop $\omega : s \mapsto e^{2\pi i s}$ in the quotient Path.Homotopic.Quotient 1 1, and $\operatorname{FundamentalGroup.fromPath}$ re-labels that class as an element of the group FundamentalGroup Circle 1 (whose elements are exactly such classes, with product "concatenate, second factor first", identity the class of the constant loop at $1$, and inverse given by reversal). Nothing is asserted about this element (for instance, no claim is made that it generates the group, that it is non-trivial, or that it has infinite order); the declaration only names it.