Tarcha: Braid Theory and the Artin Presentation with Explicit Half-Twist GeneratorsTextbook
## Motivation
A **braid** on $n$ strands is the everyday object it sounds like: $n$ strings hanging between two
horizontal plates, each string descending monotonically, no two strings meeting. Emil Artin turned
this picture into algebra in 1925 by showing that braids form a group under concatenation and that
this group has a finite presentation with $n-1$ generators. The braid groups sit at the crossroads
of low-dimensional topology (they are the mapping class groups of punctured discs, and closures of
braids produce every link), of algebra (they are the prototypical Artin–Tits groups, torsion-free
and orderable), and of representation theory and mathematical physics through the Burau, Lawrence–
Krammer and Temperley–Lieb representations.
This mission formalizes the braid-group development of a 2023 master's dissertation, Alexsander
Andrey Gomes Tarcha's *Um Estudo Introdutório da Teoria de Tranças* (UNESP, Rio Claro), whose
capstone is Teorema 3.15: the braid group on $n$ strands admits Artin's presentation. The
dissertation builds the group structure on equivalence classes of geometric braids (Teorema 3.9),
shows that the Artin generators generate (Teorema 3.11), derives the braid and commutation
relations (Proposição 3.14), establishes the presentation (Teorema 3.15), and closes with two
structural properties: the full twist is central (Proposição 3.16) and $B_m$ embeds in $B_n$ for
$m \le n$ (Proposição 3.17).
## Setting
Work in the plane $E^2 = \mathbb{C}$. The **ordered configuration space**
$$F_{0,n}E^2 = \{(z_1,\dots,z_n) \in \mathbb{C}^n : z_k \neq z_l \text{ for } k \neq l\}$$
carries the subspace topology of $\mathbb{C}^n$, and the symmetric group $\Sigma_n$ acts on it by
permuting coordinates. The **unordered configuration space** $B_{0,n}E^2 = F_{0,n}E^2/\Sigma_n$
carries the quotient topology; its points are the $n$-element subsets of the plane. The base
configuration is $(1,2,\dots,n)$, and $*$ denotes its class in $B_{0,n}E^2$. The **geometric braid
group** is
$$\pi_1\bigl(B_{0,n}E^2, *\bigr),$$
a loop of $n$-point configurations being exactly a geometric braid, and homotopy of loops being
exactly the equivalence by elementary moves used in the dissertation.
The **elementary half-twist** $\sigma_{i+1}$, for $0 \le i \le n-2$, is the loop that rotates the
two base points $i+1$ and $i+2$ by the angle $\pi$ about their midpoint $i + \tfrac32$, leaving the
other $n-2$ points fixed:
$$t \;\longmapsto\; \Bigl\{\, i+\tfrac32 \pm \tfrac12 e^{\pi i t} \,\Bigr\} \;\cup\;
\{\,k+1 : k \neq i,\, i+1 \,\}, \qquad t \in [0,1].$$
It returns to the base configuration at $t = 1$ with the two moving points interchanged, so it is a
loop in $B_{0,n}E^2$ and defines a class in $\pi_1(B_{0,n}E^2,*)$.
The **abstract braid group** $B_n$ is the group presented by generators $\sigma_1,\dots,\sigma_{n-1}$
subject to
$$\sigma_i\sigma_j = \sigma_j\sigma_i \quad (|i-j| \ge 2), \qquad
\sigma_i\sigma_{i+1}\sigma_i = \sigma_{i+1}\sigma_i\sigma_{i+1} \quad (1 \le i \le n-2).$$
## Formalization targets
### Goal — Teorema 3.15, with the isomorphism pinned on generators
$$\exists\, \varphi : B_n \;\xrightarrow{\ \sim\ }\; \pi_1\bigl(B_{0,n}E^2,*\bigr), \qquad
\varphi(\sigma_{i+1}) = \bigl[\text{half-twist}_i\bigr] \ \ (0 \le i \le n-2).$$
This is the statement the dissertation actually proves: the map $\varphi$ of its proof is defined on
generators by $\varphi(x_i) = [\sigma_i]$, and the work consists in showing that it is a
well-defined homomorphism which is surjective and injective. Asking only for an abstract
isomorphism would leave the generators unconstrained; naming their images is what makes the
presentation usable downstream.
### Milestones
$$\langle\,[\text{half-twist}_i]\,\rangle = \pi_1\bigl(B_{0,n}E^2,*\bigr) \qquad \text{(Teorema 3.11)}$$
$$[\text{half-twist}_i][\text{half-twist}_j] = [\text{half-twist}_j][\text{half-twist}_i]\ (|i-j|\ge 2),
\qquad
[\text{ht}_i][\text{ht}_{i+1}][\text{ht}_i] = [\text{ht}_{i+1}][\text{ht}_i][\text{ht}_{i+1}]$$
$$\forall b \in B_2,\ \exists m \in \mathbb{Z},\ b = \sigma_1^m \qquad \text{(Proposição 3.13)}$$
$$\forall b \in B_3,\ b = \sigma_1^{a_1}\sigma_2^{b_1}\cdots\sigma_1^{a_m}\sigma_2^{b_m}
\qquad \text{(Proposição 3.14)}$$
$$(\sigma_1\sigma_2\cdots\sigma_{n-1})^n \in Z(B_n) \qquad \text{(Proposição 3.16)}$$
$$B_m \hookrightarrow B_n \ \ (m \le n) \qquad \text{(Proposição 3.17)}$$
## Significance
Artin's presentation is what makes the braid groups computable: the word problem, the Burau and
Lawrence–Krammer representations, the Markov moves on braid closures, and the Garside normal form
all start from generators and relations, while the topological side supplies the meaning of those
generators. A formalization that only exhibits an abstract isomorphism cannot be used to compute
with a given geometric braid; the version stated here transports each half-twist loop to a
generator word, which is what downstream work needs.
On the formalization side, the geometric model (configuration spaces and their fundamental groups)
and the algebraic model (a presented group) are already available on the platform in this
environment, and the abstract form of Artin's theorem is already stated there as an open problem.
What this mission adds is: the elementary half-twist as an explicit, machine-checked loop in
$B_{0,n}E^2$ — this definition is proved sorry-free here, including the injectivity of the moving
configuration at every time and the continuity of the path; the sharpened goal that fixes the
isomorphism on generators; and the dissertation's supporting results, none of which is currently
on the platform. None of the milestones or the goal has a machine-checked proof yet.
## Difficulty
Surjectivity of $\varphi$ — every braid is a product of half-twists — is a compactness-and-general-
position argument in the dissertation: cut the braid into finitely many slabs in which a single
crossing occurs. Turning that into a formal proof requires the homotopy-theoretic substitute, since
"general position" is not available for free: a loop of configurations must be subdivided and each
piece pushed to a standard crossing.
Injectivity is harder and is the step where a naive approach fails. It is not enough to check that
the relations hold; one has to know that they are *all* the relations, i.e. that a word whose braid
is null-homotopic is a consequence of the braid relations. The dissertation follows the classical
route through elementary moves on braid diagrams (its Figuras 3.22–3.26), which formalizes as a
long case analysis. The standard modern alternative is the Fadell–Neuwirth fibration together with
an induction on $n$; its inductive step needs the exact sequence of the fibration
$F_{0,n}E^2 \to F_{0,n-1}E^2$, which is itself substantial work.
## Formalization scope
The plane is $\mathbb{C}$; configurations are injective tuples indexed by `Fin n`; the unordered
configuration space is the quotient by the coordinate-permutation action with the quotient
topology; the base configuration is $(1,2,\dots,n)$ (not $(0,1,\dots,n-1)$). Braid generators are
indexed by `Fin (n-1)`, the index $i$ standing for the book generator $\sigma_{i+1}$; truncated
natural subtraction means the degenerate values $n = 0, 1$ give the trivial group, and the
statements are asserted for all $n$ including those cases. The abstract braid group is the
presented group on `Fin (n-1)` modulo the normal closure of the commutation and braid relators.
The half-twist rotates counterclockwise. The mirror symmetry $z \mapsto \bar z$ fixes the base
configuration and exchanges the two orientations, so the goal statement does not depend on this
choice; a solver may use either convention internally.
The goal cannot be satisfied trivially: it asks for a group isomorphism whose values on the
generators are the prescribed classes of explicit loops, so neither the identity on a presented
group nor an abstract counting argument suffices.
Contributions welcome beyond the milestones: the Fadell–Neuwirth exact sequence for the plane, the
pure braid group as the kernel of the map to $\Sigma_n$, the exponent-sum homomorphism, and
torsion-freeness of $B_n$. The half-twist definition published with this mission is reusable for
any further work on braids in this environment.
## Selected references
- Alexsander Andrey Gomes Tarcha, *Um Estudo Introdutório da Teoria de Tranças*, master's
dissertation, UNESP Rio Claro, 2023. https://repositorio.unesp.br/items/9d2ffbf0-8bd2-4ec7-9e45-e2cee8a1b202
- Emil Artin, *Theorie der Zöpfe*, Abhandlungen aus dem Mathematischen Seminar der Universität
Hamburg 4 (1925), 47–72. https://doi.org/10.1007/BF02950718
- Joan S. Birman, *Braids, Links, and Mapping Class Groups*, Annals of Mathematics Studies 82,
Princeton University Press, 1974. https://doi.org/10.1515/9781400881420
- Edward Fadell and Lee Neuwirth, *Configuration spaces*, Mathematica Scandinavica 10 (1962),
111–118. https://doi.org/10.7146/math.scand.a-10517
42 thms5 active usersReviewed
Captain: Lucas
Braids, Links and Mapping Class Groups I: Artin's Presentation of the Braid GroupTextbook
## Motivation
The **braid group** is one of the places where group theory, low-dimensional topology and
knot theory meet. Artin introduced it in 1925 (E. Artin, *Theorie der Zöpfe*, Abh. Math. Sem.
Univ. Hamburg 4 (1925), 47–72) and returned to it in 1947; since then it has become standard
equipment in the study of links (closed braids and Markov's theorem), of mapping class groups
of punctured surfaces, and of configuration spaces. Birman's *Braids, Links, and Mapping Class
Groups* (Annals of Mathematics Studies 82, Princeton University Press, 1974) is the classical
reference that develops all three subjects from the braid group outwards, and its Chapter 1
is the foundation on which the rest of the book rests.
The chapter's structure is itself the reason to formalize it first: everything later in the
book — the closed-braid picture of links, Markov's theorem, the Magnus representations, the
mapping class group of the punctured sphere — is phrased in terms of the group
$\pi_1 B_{0,n}E^2$ and of the presentation established here. A mission that fixes faithful Lean
definitions of the configuration spaces and of the abstract braid group therefore fixes the
vocabulary for the whole series.
Timeline of the results collected here: Artin (1925) gave the presentation and the
characterization of braid automorphisms of a free group; Chow (1948) determined the centre;
Fadell–Neuwirth (1962) introduced the configuration-space fibrations, and Fadell–Van Buskirk
(1962) used them to give the proof of the presentation reproduced by Birman.
## Setting
Write $E^2$ for the Euclidean plane, identified throughout with the complex numbers $\mathbb{C}$.
For $n \ge 0$ let
$$F_{0,n}E^2 = \{\,(z_1,\dots,z_n) \in \mathbb{C}^n : z_i \neq z_j \text{ for } i \neq j\,\}$$
be the **ordered configuration space** of $n$ points in the plane, topologized as a subspace of
$\mathbb{C}^n$. The symmetric group $\Sigma_n$ acts on it by permuting coordinates; the quotient
$$B_{0,n}E^2 = F_{0,n}E^2 / \Sigma_n,$$
with the quotient topology, is the **unordered configuration space**. A point of $B_{0,n}E^2$ is
an unordered set of $n$ distinct points of the plane. The base configuration is
$\bar z^{\,0} = (1,2,\dots,n)$, and all fundamental groups below are taken at $\bar z^{\,0}$ or at
its image.
The **braid group of the plane** is $\pi_1 B_{0,n}E^2$: a loop is a motion of $n$ points of the
plane returning to the same set of points, and homotopy classes of such motions compose as
braids. The **pure braid group** is $P_n = \pi_1 F_{0,n}E^2$, the subgroup of motions returning
each point to its own starting position.
Separately, let $B_n$ denote the abstract group given by generators $\sigma_1,\dots,\sigma_{n-1}$
subject to
$$\sigma_i\sigma_j = \sigma_j\sigma_i \quad (|i-j| \ge 2), \qquad
\sigma_i\sigma_{i+1}\sigma_i = \sigma_{i+1}\sigma_i\sigma_{i+1} \quad (1 \le i \le n-2).$$
These are equations (1-1) and (1-2) of the book (p. 11). Geometrically $\sigma_i$ interchanges the
$i$-th and $(i+1)$-st points along a semicircle.
## Formalization targets
### Goal — Theorem 1.8 (Artin, 1925; Birman p. 18)
$$B_n \;\cong\; \pi_1 B_{0,n} E^2 .$$
The group of motions of $n$ points of the plane is the group with generators
$\sigma_1,\dots,\sigma_{n-1}$ and the two families of relations above: the relations are not only
valid but *defining*.
### Milestones
The milestone list follows the chapter: the covering-space description of the projection
$F_{0,n}E^2 \to B_{0,n}E^2$ (Proposition 1.1, p. 11), the Fadell–Neuwirth exact sequence
(Theorem 1.4, p. 14), the semidirect-product decomposition of the pure braid group
(Corollary 1.8.1, p. 24), the faithful representation of $B_n$ by automorphisms of a free group
(Corollary 1.8.3, p. 25), the centre of $B_n$ (Corollary 1.8.4, p. 28, due to Chow), and Artin's
algebraic characterization of the braid automorphisms (Theorem 1.9, p. 30).
## Significance
Theorem 1.8 is what makes the braid group *computable*: with defining relations in hand one can
combine braids into the normal form of Corollary 1.8.2 and solve the word problem, represent
braids by automorphisms of a free group, and pass to the link-theoretic material of Chapters 2
and 5 where braid words, not motions, are the objects manipulated. Corollary 1.8.3 turns braids
into concrete data — a braid is determined by what it does to the generators of a free group —
and Theorem 1.9 says exactly which endomorphisms arise this way; both are the algebraic engine
behind the conjugacy-problem and Magnus-representation chapters.
For formalization the state of play is that Mathlib has free groups, presented groups, the
fundamental groupoid and fundamental group, covering maps and fibre bundles, but no braid
groups and no configuration spaces: nothing here can be assembled from existing declarations.
The mission therefore produces reusable infrastructure — configuration spaces of the plane, the
symmetric-group quotient, the Artin presentation, the Artin action on a free group — as well as
machine-checked proofs of results that are classical but, as far as the mission's search of the
library showed, not yet formalized in Mathlib.
## Difficulty
The generators and relations are easy to write down and easy to verify *in* $\pi_1 B_{0,n}E^2$;
what is hard is completeness, i.e. that no further relations are needed. The naive route —
draw the braid, push it into a normal form by hand — is exactly what a formal proof cannot do.
The Fadell–Van Buskirk argument reproduced by Birman instead runs an induction on $n$ driven by
the fibration $F_{0,n}E^2 \to F_{0,n-1}E^2$: its homotopy exact sequence gives a split extension
of $P_{n-1}$ by a free group, presentations are assembled along the extension, and finally the
covering $F_{0,n}E^2 \to B_{0,n}E^2$ with deck group $\Sigma_n$ transfers the answer from the pure
braid group to the full braid group. Each of those steps needs genuine algebraic topology —
local triviality of the projection, exactness of the homotopy sequence, freeness of
$\pi_1$ of a punctured plane — which is where the formalization work actually lies.
## Formalization scope
The plane is $\mathbb{C}$. $F_{0,n}E^2$ is the subtype of injective functions
$\mathrm{Fin}\,n \to \mathbb{C}$; $B_{0,n}E^2$ is its quotient by the equivalence "differ by
precomposition with a permutation", with the quotient topology. Base point: the configuration
$i \mapsto i+1$, i.e. $(1,2,\dots,n)$, and its image. Fundamental groups are Mathlib's
`FundamentalGroup` at those base points. Braid generators are indexed by $\mathrm{Fin}(n-1)$
with $0$-based indices ($i$ stands for $\sigma_{i+1}$), and free-group generators by
$\mathrm{Fin}\,n$; the abstract braid group is a `PresentedGroup` on that index set. Truncated
subtraction makes the generator set empty for $n \le 1$, so $B_0$ and $B_1$ are trivial, as
intended. Two milestones are stated with the shift $n \mapsto n+1$ (i.e. for the projection
$F_{0,n+1}E^2 \to F_{0,n}E^2$) to avoid truncated subtraction in the maps.
Two conventions are worth flagging because they weaken what the Lean text asserts relative to
the prose. First, the goal asserts the existence of *some* isomorphism $B_n \cong \pi_1B_{0,n}E^2$;
it does not pin the isomorphism down on the geometric generators of Figure 2, since those loops
are not part of the formal development. Second, Artin's representation is formalized as the
existence of a homomorphism $\xi$ from $B_n$ to the automorphism group of the free group whose
value on each $\sigma_i$ is the explicit endomorphism of equation (1-14), together with its
injectivity; Theorem 1.9 is then stated for an arbitrary such $\xi$, given as a hypothesis, and
is non-vacuous precisely because Corollary 1.8.3 supplies one.
No trivializing formalization is available: the goal is an isomorphism statement between two
groups that are both defined independently of it, and the degenerate cases $n \le 1$ (both sides
trivial) are genuine special cases of it, not the content.
Infrastructure a complete development needs, all reusable: freeness of $\pi_1$ of a punctured
plane, local triviality of the Fadell–Neuwirth projection, the homotopy exact sequence of a
fibration in the range needed, presentations of split extensions, and the transfer of a
presentation along a regular covering. Contributions of any of these as standalone lemmas are
welcome, as is a formalization of the geometric generators (1-9) that would let the goal be
strengthened to pin the isomorphism on $\sigma_i$.
## Selected references
- E. Artin, *Theorie der Zöpfe*, Abhandlungen aus dem Mathematischen Seminar der Universität
Hamburg 4 (1925), 47–72. https://doi.org/10.1007/BF02950718
- E. Artin, *Theory of braids*, Annals of Mathematics 48 (1947), 101–126.
https://doi.org/10.2307/1969218
- W.-L. Chow, *On the algebraical braid group*, Annals of Mathematics 49 (1948), 654–658.
https://doi.org/10.2307/1969333
- E. Fadell, L. Neuwirth, *Configuration spaces*, Mathematica Scandinavica 10 (1962), 111–118.
https://doi.org/10.7146/math.scand.a-10517
- E. Fadell, J. Van Buskirk, *The braid groups of $E^2$ and $S^2$*, Duke Mathematical Journal 29
(1962), 243–257. https://doi.org/10.1215/S0012-7094-62-02925-3
- J. S. Birman, *Braids, Links, and Mapping Class Groups*, Annals of Mathematics Studies 82,
Princeton University Press, 1974. https://doi.org/10.1515/9781400881420
39 thms5 active usersReviewed
Captain: Lucas
Gribov Ambiguity: no continuous gauge fixing (Singer 1978)Research Paper
## Motivation
In the Feynman path-integral approach to a non-abelian gauge theory one wants to integrate a
gauge-invariant weight over the space $\mathfrak{A}$ of vector potentials (connections) of a
principal bundle. The integrand is constant on the orbits of the group $\mathcal{G}$ of gauge
transformations, so the integral over $\mathfrak{A}$ diverges and one is supposed to integrate
instead over the orbit space $\mathfrak{R} = \mathfrak{A}/\mathcal{G}$. The Faddeev–Popov
procedure realizes this by *fixing a gauge*: choosing, continuously in the orbit, exactly one
vector potential on each orbit, and correcting by a Jacobian determinant.
V. N. Gribov (SLAC Translation 176, 1977) observed that for $SU(2)$ potentials on
$\mathbb{R}^3$ (or $\mathbb{R}^4$) with suitable conditions at infinity, the Coulomb gauge
condition does not do this: the Coulomb slice through the zero potential meets the orbit of the
zero potential again, far from the origin. These extra intersections are the **Gribov copies**;
R. Jackiw, I. Muzinich and C. Rebbi (Phys. Rev. D 17 (1978) 1576) analyzed them in detail.
I. M. Singer, *Some Remarks on the Gribov Ambiguity* (Commun. Math. Phys. **60** (1978) 7–12),
showed that the phenomenon is not a defect of the Coulomb gauge. If the conditions at infinity
are those of Gribov — gauge transformations extending to the one-point compactification with
value $I$ at infinity, so that the base manifold is $M = S^3$ or $M = S^4$ — then **no**
continuous gauge fixing exists at all, in any gauge. The obstruction is topological: the space
of irreducible connections is weakly contractible, while the gauge group is not, and a
weakly contractible principal bundle admits no global continuous section.
## Setting
Fix $N \ge 2$ and take the structure group $SU(N)$, the group of $N \times N$ complex matrices
$U$ with $U^\ast U = I$ and $\det U = 1$, topologized as a subspace of matrices. Let
$S^r$ denote the unit sphere of $\mathbb{R}^{r+1}$, with base point $m$ the north pole.
For the trivial $SU(N)$-bundle over a space $M$, a gauge transformation is a map
$\varphi : M \to SU(N)$, and the **gauge group** is
$$\mathcal{G}(M,N) \;=\; C\bigl(M, SU(N)\bigr),$$
continuous maps with pointwise multiplication and the compact-open topology. Two subobjects
matter. The **based gauge group** $\mathcal{G}_m = \{\varphi : \varphi(m) = I\}$ is the subgroup
of transformations that are the identity at the base point. The constant transformations with
value in the centre $Z_N = \{e^{2\pi i k/N} I\}$ of $SU(N)$ form a normal subgroup, and the
**reduced gauge group** is the quotient
$$\overline{\mathcal{G}}(M,N) \;=\; \mathcal{G}(M,N)/Z_N$$
with the quotient topology. The centre acts trivially on vector potentials, so
$\overline{\mathcal{G}}$ is the group that acts effectively.
A group $G$ acting continuously on a space $\mathfrak{A}$ has orbit space
$\mathfrak{A}/G$ with the quotient topology, and a **gauge fixing** is a continuous map
$s : \mathfrak{A}/G \to \mathfrak{A}$ with $p \circ s = \mathrm{id}$, where
$p : \mathfrak{A} \to \mathfrak{A}/G$ is the projection: a continuous choice of exactly one point
on each orbit. The action is **principal** when it is free and the division map, which sends a
pair of points on one orbit to a group element carrying the second to the first, can be chosen
continuously; this is the topological content of "$p$ is a principal $G$-bundle". The space
$\mathfrak{A}$ is **weakly contractible** when it is nonempty and all its homotopy groups vanish.
In the paper, $\mathfrak{A}$ is the affine space of connections, $\mathfrak{R}$ its set of
irreducible members, and Theorems 1 and 2 say exactly that $\mathfrak{R}$ is a weakly
contractible principal $\overline{\mathcal{G}}$-space.
## Formalization targets
### Goal — Corollary 4 (no gauge fixing)
For $r \in \{3,4\}$, $N \ge 2$, and every weakly contractible principal
$\overline{\mathcal{G}}(S^r,N)$-space $A$:
$$\nexists\, s : A/\overline{\mathcal{G}}(S^r,N) \longrightarrow A \quad\text{continuous with}\quad p \circ s = \mathrm{id}.$$
By Theorems 1 and 2 of the paper the space of irreducible connections over $S^3$ or $S^4$ is such
an $A$, so the goal contains Singer's Corollary 4 for that space; it leaves the analytic
construction of the space of connections unfixed, which is what makes it statable today.
### Milestone level — Theorem 3
$$\exists\, j \ge 1: \quad \pi_j\bigl(\overline{\mathcal{G}}(S^r,N)\bigr) \neq 0, \qquad r \in \{3,4\},\ N \ge 2 .$$
### Milestone level — Theorem 5 and its homotopy inputs
$$\pi_j\bigl(\mathcal{G}_m(S^r,N)\bigr) \;\cong\; \pi_{j+r}\bigl(SU(N)\bigr), \qquad
\pi_3(SU(N)) \cong \mathbb{Z}, \qquad \pi_4(SU(N)) = 0 \ (N\ge 3), \qquad \pi_4(SU(2)) \cong \mathbb{Z}/2 .$$
## Significance
The result rules out the existence of a global gauge in the topological sense: every gauge
condition used in practice is at best a local slice, and the Faddeev–Popov construction has to be
read as a local statement, patched with a partition of unity over the orbit space (as the last
section of the paper proposes). It is the mathematical reason why the Gribov ambiguity cannot be
repaired by a cleverer gauge condition, and it is the origin of the Gribov–Zwanziger restriction
of the functional integral to a fundamental domain.
Formalizing it adds a machine-checked version of an argument that is quoted far more often than
it is checked, and it forces into Lean a piece of infrastructure that Mathlib currently lacks:
homotopy groups of mapping spaces, the long exact sequence of a fibration in the form needed for
$0 \to \mathcal{G}_m \to \mathcal{G} \to SU(N) \to 0$, and the classical computations
$\pi_3(SU(N)) \cong \mathbb{Z}$, $\pi_4(SU(N)) = 0$ for $N \ge 3$, $\pi_4(SU(2)) \cong \mathbb{Z}/2$.
Singer's results are proved mathematics; none of them is formalized, and Mathlib as of the pinned
revision contains homotopy groups as a definition together with their group structure, but
essentially no computation of them.
## Difficulty
The naive approach to the goal — build a section by hand, or average over the group — fails
because $\overline{\mathcal{G}}$ is neither compact nor contractible and the obstruction is
global: locally, slices do exist (that is the content of the generalized Coulomb gauge), so no
local argument can produce a contradiction. The proof has to convert a section into a
homotopy-theoretic statement: a section of a principal bundle trivializes it, exhibiting the
group as a retract of the total space, so all homotopy groups of the group would vanish; the work
is then to show that some homotopy group of the reduced gauge group does not vanish, which needs
the identification of the based gauge group with a mapping space, the exact sequences relating
$\mathcal{G}_m$, $\mathcal{G}$ and $\overline{\mathcal{G}}$, and non-trivial homotopy groups of
$SU(N)$ — including $\pi_6(S^3) \cong \mathbb{Z}/12$ for the $SU(2)$ case of Theorem 3.
## Formalization scope
The formalization commits to the following conventions, all of them visible in the definitions of
this mission.
- The bundle is the **trivial** $SU(N)$-bundle, so gauge transformations are literally maps
$M \to SU(N)$. This is the case of Gribov's original setting over $S^3$; over $S^4$ the paper
also treats bundles of nonzero Pontrjagin index, which are out of scope here.
- Gauge transformations are **continuous**, not smooth, with the compact-open topology; Singer's
Theorem 5 uses smoothing homotopies to pass between the two, and the homotopy-theoretic content
is the same.
- $SU(N)$ is the special unitary group of complex $N \times N$ matrices, with its subspace
topology; $S^r$ is the unit sphere of $\mathbb{R}^{r+1}$ with its subspace topology.
- Homotopy groups are Mathlib's `HomotopyGroup`, based at the identity element.
- The **space of connections is not constructed**: Mathlib has no space of connections on a
principal bundle, and building one is a mission of its own. The goal therefore quantifies over
an arbitrary topological space carrying a weakly contractible principal action of the reduced
gauge group — exactly the properties Theorems 1 and 2 establish for the irreducible
connections.
- This quantification is not vacuous: such spaces exist (the total space of a universal
$\overline{\mathcal{G}}$-bundle is one), so the goal is a genuine non-existence statement and
not a statement about an empty class. Conversely it is not trivially true: the hypotheses do
not mention any homotopy invariant of the gauge group, and refuting a section requires
Theorem 3.
- The paper's analytic statements — Theorem 1 (openness and density of the irreducible
connections, principal bundle structure), Theorem 2 (weak contractibility), Theorem 6
($\pi_1$ of the irreducible orbit space), Theorem 7 (no flat connection), Theorem 8 (tangency
of orbits to the Coulomb slice) and Theorem 9 (the canonical connection and its curvature) —
are out of scope until a space of connections exists in Lean. Contributions that build one, in
reusable form, are welcome and would let this mission be extended to them.
## Selected references
- V. N. Gribov, *Instability of non-abelian gauge theories and impossibility of choice of Coulomb
gauge*, SLAC Translation 176 (1977); Nucl. Phys. B **139** (1978) 1–19,
[doi:10.1016/0550-3213(78)90175-X](https://doi.org/10.1016/0550-3213(78)90175-X).
- I. M. Singer, *Some Remarks on the Gribov Ambiguity*, Commun. Math. Phys. **60** (1978) 7–12,
[doi:10.1007/BF01609471](https://doi.org/10.1007/BF01609471).
- R. Jackiw, I. Muzinich, C. Rebbi, *Coulomb gauge description of large Yang-Mills fields*,
Phys. Rev. D **17** (1978) 1576, [doi:10.1103/PhysRevD.17.1576](https://doi.org/10.1103/PhysRevD.17.1576).
- H. Toda, *Composition methods in homotopy groups of spheres*, Annals of Mathematics Studies 49,
Princeton University Press (1962).
8 thms1 active userReviewed
🏆Completed
Captain: Rui Chao
Counterexamples to the Zeng–Pryadko Homological-Distance ConjectureResearch Paper
## Background and main question
The tensor product of chain complexes is a basic construction in homological algebra and in the theory of quantum CSS codes. If $A$ and $B$ are finite based chain complexes over a finite field, their tensor product is graded by total degree,
$$
(A\otimes B)_j=\bigoplus_{i=0}^{j} A_i\otimes B_{j-i}.
$$
Each complex carries a basis-dependent homological distance: $d_j(A)$ is the least Hamming weight of a degree-$j$ cycle that is not a boundary, with $d_j(A)=\infty$ when the degree-$j$ homology vanishes. A natural candidate for the distance of the tensor product is therefore
$$
m_j(A,B)=\min_{0\le i\le j} d_i(A)d_{j-i}(B).
$$
Every nonzero pair of homology classes in complementary degrees gives a pure-tensor class of the corresponding product weight, so one always has $d_j(A\otimes B)\le m_j(A,B)$. The substantive question is whether this upper bound is always sharp.
In the preprint [*Higher-Dimensional Quantum Hypergraph-Product Codes with Finite Rates*](https://arxiv.org/abs/1810.01519), posted in 2018 and subsequently [published in *Physical Review Letters*](https://link.aps.org/doi/10.1103/PhysRevLett.122.230501), Zeng and Pryadko proved that the bound is sharp when one factor is a binary one-complex. Their exact formula is Eq. (13) of the arXiv version and is the capstone theorem of the Prove2Me mission [*Higher-Dimensional Quantum Hypergraph-Product Codes with Finite Rates*](https://prove2.me/missions/Higher-Dimensional%20Quantum%20Hypergraph-Product%20Codes%20with%20Finite%20Rates). The present formalization is a direct sequel: it retains the same definitions and degree conventions while examining what happens when the one-complex restriction is removed.
Zeng and Pryadko later considered arbitrary finite chain complexes over arbitrary finite fields in [*Minimal distances for certain quantum product codes and tensor products of chain complexes*](https://link.aps.org/doi/10.1103/PhysRevA.102.062402), published in 2020. In [the corresponding arXiv preprint](https://arxiv.org/abs/2007.12152), Conjecture 18 asserts the unrestricted equality
$$
d_j(A\otimes B)=m_j(A,B).
$$
The conjecture is appealing because it would make tensor-product distance completely compositional: the degreewise distances of the two factors would determine the distance of their product. The obstruction is that a homology class in $A\otimes B$ need not have a minimum-weight representative supported in a single bidegree. A representative spread across several summands of the total complex can be lighter than every pure-tensor representative. The purpose of this formalization is to turn that observation into a concrete, machine-checked counterexample to Conjecture 18 while preserving the valid one-complex theorem as a sharply delimited special case.
## The counterexample mechanism
The common foundation is recorded in the Prove2Me entry [*Based binary chain complexes and homological distance*](https://prove2.me/theorems/9d65f1ac-c78c-4540-8ac4-38597548a9ff). In particular, the boundary in degree $j$ is a map $\partial_j:A_j\to A_{j-1}$, and
$$
d_j(A)=\inf\{\operatorname{wt}(x):x\in\ker\partial_j,\ x\notin\operatorname{im}\partial_{j+1}\}.
$$
The one-complex result is separately available as [*Eq. (13) — Exact distance with a one-complex*](https://prove2.me/theorems/4f4006fe-af5b-42ba-a936-bb49e92c92b6). The construction below uses exactly the same notion of distance, but both tensor factors are genuine three-term complexes.
Begin with binary CSS check maps
$$
H_X:\mathbb F_2^n\longrightarrow\mathbb F_2^{r_X},
\qquad
H_Z:\mathbb F_2^n\longrightarrow\mathbb F_2^{r_Z},
$$
assumed surjective and satisfying $H_XH_Z^T=H_ZH_X^T=0$. Suppose there are logical vectors $x,z\in\mathbb F_2^n$ such that
$$
H_Zx=0,\qquad H_Xz=0,\qquad x\cdot z=1.
$$
The check maps determine two dual three-term complexes
$$
A:\quad \mathbb F_2^{r_X}\xleftarrow{H_X}\mathbb F_2^n
\xleftarrow{H_Z^T}\mathbb F_2^{r_Z},
\qquad
B:\quad \mathbb F_2^{r_Z}\xleftarrow{H_Z}\mathbb F_2^n
\xleftarrow{H_X^T}\mathbb F_2^{r_X}.
$$
Their degree-two tensor space has three bidegree summands, corresponding to $(2,0)$, $(1,1)$, and $(0,2)$. Under the natural matrix identifications, consider the element whose three blocks are
$$
(I_{r_Z},I_n,I_{r_X}).
$$
The CSS orthogonality relations make this element a cycle. Its pairing with the chosen logical vectors certifies that it is not a boundary. Its Hamming weight is exactly $r_Z+n+r_X$, whereas the componentwise candidate in degree two reduces to
$$
m_2(A,B)=d_1(A)d_1(B).
$$
Consequently, any CSS datum satisfying
$$
r_Z+n+r_X<d_1(A)d_1(B)
$$
produces the strict inequality $d_2(A\otimes B)<m_2(A,B)$. For orientation, a binary quantum Golay CSS presentation with parameters $[[23,1,7]]$ has $r_X=r_Z=11$, giving the numerical comparison $45<49$. The formal proof must supply an explicit CSS instance and verify its algebraic and distance properties, rather than relying on the parameter notation alone.
## Formalization objectives
The first milestone proves the general certificate: for every CSS datum satisfying the hypotheses above, the element $(I_{r_Z},I_n,I_{r_X})$ is a nontrivial degree-two cycle of weight $r_Z+n+r_X$, and the componentwise minimum is $d_1(A)d_1(B)$.
The second milestone constructs and verifies one explicit CSS datum for which $r_Z+n+r_X<d_1(A)d_1(B)$. This is the step that turns the general mechanism into an actual counterexample.
The capstone packages the construction as the direct existential statement
$$
\exists\,A,B\qquad d_2(A\otimes B)<\min_{0\le i\le 2}d_i(A)d_{2-i}(B).
$$
Thus the final theorem is not conditional on the existence of suitable code data: it exhibits finite based binary chain complexes for which the equality proposed in Conjecture 18 fails.
## Relation to prior work
The counterexample concerns only the unrestricted passage from a one-complex factor to two arbitrary bounded complexes. It does not conflict with Zeng and Pryadko's Eq. (13), whose one-complex hypothesis rules out the three-bidegree interaction used here.
The broader literature also indicates why additional structure matters. [Bravyi and Hastings](https://dl.acm.org/doi/10.1145/2591796.2591870) introduced homological-product codes and analyzed logical representatives in product constructions; [Audoux and Couvreur](https://www.numdam.org/articles/10.4171/aihpd/71/) developed tensor products of CSS codes through chain-complex methods. More recently, [Akhmechet et al.](https://arxiv.org/abs/2410.11252) discussed the Zeng–Pryadko conjecture in the structured setting of complexes derived from Khovanov homology, while [Berthusen et al.](https://arxiv.org/abs/2508.04794) restated it as Conjecture 5.1 in their study of automorphism gadgets. [Golowich and Guruswami](https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CCC.2025.25) obtained strong distance guarantees for iterated homological products under expansion and local-testability hypotheses. These results are compatible with the proposed counterexample: they concern special families or impose hypotheses that are absent from Conjecture 18.
Besides settling the unrestricted statement, the formalization isolates a reusable obstruction. It shows precisely how a low-weight class assembled across several bidegrees can evade a formula based only on the degreewise distances of the factors. This distinction should help guide corrected formulations in which an exact product formula, or a useful lower bound, is recovered from additional geometric, expansion, or local-testability assumptions.
The main formal issues are mathematically substantive rather than presentational: the proof must respect the endpoint conventions for the boundary maps, distinguish a cycle from a non-boundary, compare finite weights with $\infty$-valued distances, and verify a concrete strict-gap instance. Making each of these points explicit is especially important here, because an indexing shift or a merely conditional existence statement would no longer constitute a refutation of the conjecture as stated.
## References
- W. Zeng and L. P. Pryadko, [*Higher-Dimensional Quantum Hypergraph-Product Codes with Finite Rates*](https://link.aps.org/doi/10.1103/PhysRevLett.122.230501), *Physical Review Letters* 122, 230501 (2019); [arXiv:1810.01519 (2018), Eq. (13)](https://arxiv.org/abs/1810.01519).
- W. Zeng and L. P. Pryadko, [*Minimal distances for certain quantum product codes and tensor products of chain complexes*](https://link.aps.org/doi/10.1103/PhysRevA.102.062402), *Physical Review A* 102, 062402 (2020); [arXiv:2007.12152, Conjecture 18](https://arxiv.org/abs/2007.12152).
- S. Bravyi and M. B. Hastings, [*Homological Product Codes*](https://dl.acm.org/doi/10.1145/2591796.2591870), STOC 2014; [arXiv:1311.0885](https://arxiv.org/abs/1311.0885).
- B. Audoux and A. Couvreur, [*On tensor products of CSS codes*](https://www.numdam.org/articles/10.4171/aihpd/71/), *Annales de l'Institut Henri Poincaré D* 6 (2019); [arXiv:1512.07081](https://arxiv.org/abs/1512.07081).
- R. Akhmechet et al., [*Khovanov homology and quantum error-correcting codes*](https://arxiv.org/abs/2410.11252), arXiv:2410.11252 (2024).
- N. Berthusen et al., [*Automorphism gadgets in homological product codes*](https://arxiv.org/abs/2508.04794), arXiv:2508.04794 (2025).
- L. Golowich and V. Guruswami, [*Quantum LDPC Codes of Almost Linear Distance via Iterated Homological Products*](https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CCC.2025.25), CCC 2025; [full version](https://arxiv.org/abs/2411.03646).
6 thms2 active usersReviewed
🏆Completed
Captain: Rui Chao
Higher-Dimensional Quantum Hypergraph-Product Codes with Finite RatesResearch Paper
## Motivation
Quantum low-density parity-check codes encode quantum information using sparse
parity constraints. A standard way to construct them is to translate binary
chain complexes into Calderbank--Shor--Steane codes and to combine complexes by
tensor product. Homology identifies the logical operators of the resulting
code, while the smallest Hamming weight of a nontrivial homology class controls
one of its distances. Determining how this distance behaves under a tensor
product is therefore a basic structural question, not merely a parameter
calculation.
Weilei Zeng and Leonid P. Pryadko studied products in which one factor is an
arbitrary finite binary chain complex and the other is the one-complex induced
by a binary matrix. Their paper was published as [“Higher-Dimensional Quantum
Hypergraph-Product Codes with Finite Rates,” *Physical Review Letters* 122,
230501 (2019)](https://doi.org/10.1103/PhysRevLett.122.230501). Its main
distance result is Eq. (13) in the [arXiv version](https://arxiv.org/abs/1810.01519):
for this particular tensor factor, the usual product upper bound is always
exact. The result extends the familiar two-complex setting of quantum
hypergraph-product codes to the local structure occurring in complexes of any
dimension.
## Setting
A **based binary chain complex** consists of finite-dimensional vector spaces
$A_i$ over $\mathbb F_2$, each equipped with a specified coordinate basis, and
linear boundary maps
$$
\cdots\longrightarrow A_{i+1}\xrightarrow{\partial_{i+1}}A_i
\xrightarrow{\partial_i}A_{i-1}\longrightarrow\cdots
$$
such that $\partial_i\partial_{i+1}=0$. Its degree-$i$ homology is
$H_i(\mathcal A)=\ker\partial_i/\operatorname{im}\partial_{i+1}$. The
**homological distance** is measured in the chosen basis:
$$
d_i(\mathcal A)=
\min\{\operatorname{wt}(x):x\in\ker\partial_i\setminus
\operatorname{im}\partial_{i+1}\}.
$$
Following the paper, the minimum of an empty set is $\infty$. Thus
$d_i(\mathcal A)=\infty$ when $H_i(\mathcal A)$ is trivial.
The endpoint convention is also the one stated explicitly after Eq. (1). For
an $m$-complex, $\partial_0:A_0\to\{0\}$ is the zero $0\times n_0$ matrix and
$\partial_{m+1}:\{0\}\to A_m$ is the zero $n_m\times0$ matrix. Consequently
$$
d_0(\mathcal A)=\min\{\operatorname{wt}(x):
x\in A_0\setminus\operatorname{im}\partial_1\}
$$
and
$$
d_m(\mathcal A)=\min\{\operatorname{wt}(x):
0\ne x\in\ker\partial_m\}.
$$
For an $r\times c$ binary matrix $P$, the **one-complex**
$\mathcal K(P)$ has $\mathbb F_2^c$ in degree one,
$\mathbb F_2^r$ in degree zero, and boundary $P$. Its two distances are
$$
d_1(\mathcal K(P))=
\min\{\operatorname{wt}(x):Px=0,\ x\ne0\}
$$
and
$$
d_0(\mathcal K(P))=
\min\{\operatorname{wt}(y):y\notin\operatorname{im}P\}.
$$
In particular, $d_0=1$ unless $P$ has full row rank, in which case
$d_0=\infty$. The degree-$j$ chain group of
$\mathcal A\times\mathcal K(P)$ is
$$
(A_j\otimes\mathbb F_2^r)\oplus
(A_{j-1}\otimes\mathbb F_2^c),
$$
with the standard tensor-product boundary. Over $\mathbb F_2$ the usual sign
in that boundary has no effect.
## Formalization targets
### Tensor-product upper bound for arbitrary complexes
The first milestone is Eq. (11) for two arbitrary finite-length based binary
chain complexes:
$$
d_j(\mathcal A\times\mathcal B)\le
\min_i d_i(\mathcal A)d_{j-i}(\mathcal B).
$$
### Rank-sensitive lower bound
Let $u=\operatorname{rank}P$ and
$\delta=d_1(\mathcal K(P))$. The second milestone is Theorem 1, including
both of its cases:
$$
u<r\Longrightarrow
d_j(\mathcal A\times\mathcal K(P))\ge
\min\!\left(d_j(\mathcal A),d_{j-1}(\mathcal A)\delta\right),
$$
and
$$
u=r\Longrightarrow
d_j(\mathcal A\times\mathcal K(P))\ge
d_{j-1}(\mathcal A)\delta.
$$
### Exact distance with a one-complex
The goal is Eq. (13):
$$
d_j(\mathcal A\times\mathcal K(P))=
\min\!\left(
d_{j-1}(\mathcal A)d_1(\mathcal K(P)),
d_j(\mathcal A)d_0(\mathcal K(P))
\right).
$$
No full-rank hypothesis is imposed on $P$.
## Significance
The equality determines the product distance exactly from four component
distances. General tensor-product arguments immediately provide the upper
bound, but an exact formula requires ruling out lower-weight homology classes
that mix the two direct-sum blocks. Once established, the formula can be
applied repeatedly to tensor products of one-complexes, which is the step used
in the paper to obtain higher-dimensional quantum hypergraph-product code
families and to compute their distances.
For formalization, the mission contributes reusable definitions of finite
based binary chain data, homological distance valued in
$\mathbb N\cup\{\infty\}$, the one-complex of a binary matrix, and the relevant
tensor-product boundary maps. Mathlib contains Hamming weight and general
homological-algebra infrastructure, while QECLean contains a closely related
based length-three homological-code interface. Neither the selected Mathlib
environment nor the inspected QECLean development currently supplies this
rank-sensitive exact distance theorem.
## Difficulty
The central issue is that Hamming weight depends on the chosen bases and is not
preserved by arbitrary homological isomorphisms. A Künneth isomorphism
describes the product homology and readily produces low-weight representatives,
which is enough for the upper bound, but it does not by itself exclude a still
lighter representative obtained by cancellation between the two tensor
blocks. The lower bound must also remain valid at the endpoints of the complex
and in singular cases where one or more homology groups vanish and the relevant
distance is $\infty$.
The theorem cannot be reduced to a dimension calculation. It must reason
about supports and Hamming weights of based representatives while respecting
the quotient by boundaries, and it must cover both $\operatorname{rank}P<r$
and $\operatorname{rank}P=r$.
## Formalization scope
The Lean development works over `ZMod 2`. A finite basis in degree $i$ is
represented by `Fin (dimension i)`, and a chain group is the function space
from that coordinate type to `ZMod 2`. `BasedBinaryChainComplex` stores the
dimension and boundary in every nonnegative degree, the chain condition, and a
finite length above which all dimensions are zero. Thus the first milestone
quantifies over genuinely arbitrary finite lengths for both $\mathcal A$ and
$\mathcal B$, rather than over a local window or a one-complex specialization.
If the stored length is $m$, the zero-dimensional source in degree $m+1$
makes $\partial_{m+1}:\{0\}\to A_m$ the unique zero map, just as the
zero-dimensional target below degree zero makes
$\partial_0:A_0\to\{0\}$ the unique zero map. Hence both singular endpoint
cases in Eqs. (1) and (4) are represented directly.
Distances use `WithTop ℕ`. Their definitions are actual minima of Hamming
weights of nontrivial representatives, with `⊤` produced by the empty-set
case; infinite distance is not an extra hypothesis or a separately hard-coded
branch. Coordinate types may be empty, which covers missing endpoint blocks.
The binary matrix $P$ is represented as a linear map between two finite based
function spaces. Its row and column coordinate types need not be nonempty,
and no injectivity or surjectivity assumption is added.
The degree-$j$ product group is indexed by the disjoint union of all coordinate
products $A_i\times B_{j-i}$ for $0\le i\le j$. Consequently its Hamming norm
is the sum of the weights of all tensor-degree blocks. The product boundary is
the standard signed tensor boundary; its sign disappears over $\mathbb F_2$.
A formal proof verifies that every pair of consecutive product boundaries
composes to zero; the cancellation of the two mixed terms uses characteristic
two. Thus the product distance is taken from an actual chain complex, rather
than from unrelated adjacent linear maps.
A basis-free tensor product or an abstract homology group alone is insufficient
for the target, because either would discard the weight data on which the
statement depends.
The mission does not formalize the asymptotic code-family construction later
in the paper, the transposed cohomological distance, or the CSS-code parameter
translation. Those are natural downstream missions; they should reuse rather
than alter the present based-chain definitions.
## Selected references
- Weilei Zeng and Leonid P. Pryadko, [“Higher-Dimensional Quantum Hypergraph-Product Codes with Finite Rates,”](https://doi.org/10.1103/PhysRevLett.122.230501) *Physical Review Letters* 122, 230501 (2019). [arXiv:1810.01519](https://arxiv.org/abs/1810.01519).
- Benjamin Audoux and Alain Couvreur, [“On Tensor Products of CSS Codes,”](https://arxiv.org/abs/1512.07081) arXiv:1512.07081 (2015), especially Proposition 1.13 and Corollary 2.14 as cited by Zeng--Pryadko.
- Jean-Pierre Tillich and Gilles Zémor, [“Quantum LDPC Codes With Positive Rate and Minimum Distance Proportional to the Square Root of the Blocklength,”](https://doi.org/10.1109/TIT.2013.2292061) *IEEE Transactions on Information Theory* 60 (2014), 1193--1202.
4 thms1 active userReviewed
🏆Completed
Captain: korbonits
Hatcher Algebraic Topology III: The Classification of Covering SpacesTextbook
## Motivation
The third mission in the series formalizing Allen Hatcher's *Algebraic Topology* (Cambridge University Press, 2002; [pi.math.cornell.edu/~hatcher/AT/AT.pdf](https://pi.math.cornell.edu/~hatcher/AT/AT.pdf)) turns to the second main topic of Chapter 1, **covering spaces** (Section 1.3, pp. 56–78). The first mission used the covering $\mathbb{R}\to S^1$ to compute $\pi_1(S^1)$, and the second proved van Kampen's theorem. This mission develops the general theory of covering spaces of a fixed space $X$: the lifting properties (pp. 60–62), the classification of connected covering spaces by subgroups of $\pi_1(X)$ (pp. 63–68), and deck transformations and group actions (pp. 70–72). Its goal is the **classification theorem** (Theorem 1.38, p. 67), Hatcher's "Galois correspondence" between path-connected covering spaces of $X$ and subgroups of $\pi_1(X,x_0)$, together with its companions Proposition 1.39 (deck groups and normal covers) and Proposition 1.40 (covering space actions and orbit spaces).
All statements live in the Lean namespace `Hatcher` used by the earlier missions.
## Setting
A **covering space** of $X$ (p. 56) is a space $\tilde X$ with a map $p:\tilde X\to X$ such that every $x\in X$ has an open neighborhood $U$ whose preimage is a disjoint union of open sets each mapped homeomorphically onto $U$; $p^{-1}(U)$ may be empty, so $p$ need not be surjective. This is Mathlib's `IsCoveringMap`. For a covering space with basepoints $p:(\tilde X,\tilde x_0)\to(X,x_0)$ we write
$$p_*:\pi_1(\tilde X,\tilde x_0)\to\pi_1(X,x_0),\qquad H=p_*\big(\pi_1(\tilde X,\tilde x_0)\big)\le\pi_1(X,x_0)$$
for the induced homomorphism (`Hatcher.coverHom`) and its image (`Hatcher.coverSubgroup`).
$X$ is **semilocally simply-connected** (p. 63, `Hatcher.IsSemilocallySimplyConnected`) if each $x\in X$ has a neighborhood $U$ such that every loop at $x$ contained in $U$ is null-homotopic in $X$. The bundle `Hatcher_Covering` also fixes: the structure `CoveringSpace X` (a total space $\tilde X$ and a covering map $p$) and its pointed version `PointedCover X x₀` (with $\tilde x_0\in p^{-1}(x_0)$ and associated subgroup `PointedCover.subgroup`); **isomorphism** of covering spaces (p. 67), a homeomorphism $f:\tilde X_1\to\tilde X_2$ with $p_1=p_2f$, with or without preservation of basepoints (`IsIsomorphic`, `IsPointedIsomorphic`); the **deck transformation group** $G(\tilde X)$ (p. 70, `deckGroup`), the self-homeomorphisms of $\tilde X$ commuting with $p$; **normal** covering spaces (p. 70, `IsNormalCover`); Hatcher's condition $(\ast)$ for a **covering space action** of a group $G$ on $Y$ (p. 72, `IsCoveringSpaceAction`); and the **orbit space** $Y/G$ with its quotient map (`OrbitSpace`, `orbitProj`).
## Formalization targets
### Goal (Theorem 1.38, p. 67)
Let $X$ be path-connected, locally path-connected and semilocally simply-connected, with basepoint $x_0$. Then:
1. every subgroup $H\le\pi_1(X,x_0)$ is $p_*\pi_1(\tilde X,\tilde x_0)$ for some path-connected covering space with basepoint;
2. two path-connected covering spaces with basepoints are isomorphic by a basepoint-preserving isomorphism iff their subgroups coincide;
3. two path-connected covering spaces are isomorphic (basepoints ignored) iff their subgroups, at some choice of basepoints over $x_0$, are conjugate in $\pi_1(X,x_0)$.
Together these say that $(\tilde X,\tilde x_0)\mapsto p_*\pi_1(\tilde X,\tilde x_0)$ is a bijection from basepoint-preserving isomorphism classes of path-connected covering spaces to subgroups, inducing a bijection from isomorphism classes to conjugacy classes of subgroups.
### Milestones
1. **Proposition 1.31** (p. 61), first part: $p_*$ is injective.
2. **Proposition 1.31**, second part: $p_*\pi_1(\tilde X,\tilde x_0)$ consists of the classes of loops at $x_0$ whose lifts starting at $\tilde x_0$ are loops.
3. **Proposition 1.32** (p. 61): for $X,\tilde X$ path-connected, the fibre $p^{-1}(x_0)$ is in bijection with the cosets of $H$, so the number of sheets is the index of $H$.
4. **Proposition 1.33** (p. 61), the lifting criterion: for $Y$ path-connected and locally path-connected, $f:(Y,y_0)\to(X,x_0)$ lifts to $(\tilde X,\tilde x_0)$ iff $f_*\pi_1(Y,y_0)\subseteq H$.
5. **Proposition 1.34** (p. 62), unique lifting: two lifts of $f:Y\to X$ agreeing at one point agree everywhere if $Y$ is connected.
6. **Necessity of semilocal simple connectivity** (p. 63): if $X$ has a simply-connected covering space (surjective onto $X$), then $X$ is semilocally simply-connected.
7. **Existence of a simply-connected covering space** (pp. 63–65): if $X$ is path-connected, locally path-connected and semilocally simply-connected, it has a simply-connected covering space (the universal cover).
8. **Proposition 1.36** (p. 66): under the same hypotheses, every subgroup $H\le\pi_1(X,x_0)$ is realized as $p_*\pi_1(X_H,\tilde x_0)$ for a path-connected covering space.
9. **Proposition 1.37** (p. 67): for $X$ path-connected and locally path-connected, two path-connected covering spaces with basepoints are basepoint-preservingly isomorphic iff their subgroups are equal.
10. **Change of basepoint** (pp. 67–68, proof of Theorem 1.38): moving $\tilde x_0$ within $p^{-1}(x_0)$ replaces $H$ by a conjugate, and every conjugate arises this way.
11. **Proposition 1.39(a)** (p. 71): a path-connected covering space of a path-connected, locally path-connected $X$ is normal iff $H$ is a normal subgroup.
12. **Proposition 1.39(b)**: $G(\tilde X)\cong N(H)/H$, given as a surjective homomorphism $N(H)\to G(\tilde X)$ with kernel $H$.
13. **Proposition 1.39, final clause**: for the universal cover, $G(\tilde X)\cong\pi_1(X,x_0)$.
14. **Proposition 1.40(a)** (p. 72): for a covering space action of $G$ on $Y$, the quotient map $Y\to Y/G$ is a normal covering space.
15. **Proposition 1.40(b)**: if moreover $Y$ is path-connected, $G$ is the group of deck transformations of $Y\to Y/G$, via $g\mapsto(y\mapsto gy)$.
16. **Proposition 1.40(c)**: if $Y$ is path-connected and locally path-connected, $G\cong\pi_1(Y/G)/p_*\pi_1(Y)$, given as a surjective homomorphism $\pi_1(Y/G)\to G$ with kernel $p_*\pi_1(Y)$.
## Significance
*The result itself.* The classification theorem is the central structural fact about covering spaces: the connected coverings of $X$ are "the same as" the subgroups of $\pi_1(X)$, with the universal cover corresponding to the trivial subgroup and normal coverings to normal subgroups. Proposition 1.40 is the standard method for computing fundamental groups of orbit spaces ($\pi_1(\mathbb{RP}^n)=\mathbb{Z}/2$, $\pi_1(T^n)=\mathbb{Z}^n$, lens spaces) and is used throughout Hatcher's later chapters.
*Formalizing it.* Mathlib (at this environment's revision) already has the lifting theory for covering maps: path and homotopy lifting (`IsCoveringMap.liftPath`, `liftHomotopy`), the monodromy action (`IsCoveringMap.monodromy`), the injectivity of $p_*$ (`injective_path_homotopic_map`, cited there as Proposition 1.31), the unique-lifting statement (`IsCoveringMap.eq_of_comp_eq`), and the lifting criterion itself (`existsUnique_continuousMap_lifts_of_range_le`, cited as Proposition 1.33). For quotient maps by a free properly discontinuous action it has `IsQuotientCoveringMap`, with the homomorphism $\pi_1(Y/G)\to G^{\mathrm{op}}$ and its kernel and surjectivity. Milestones 1, 4, 5 and 16 are therefore expected to be short reductions to Mathlib, and Mathlib's quotient-covering theory should carry most of milestones 14–15. Mathlib has no notion of semilocal simple connectivity, no construction of the universal cover or of the coverings $X_H$, no classification theorem, and no deck transformation groups or normal coverings; milestones 6–13 and the goal are new.
## Difficulty
The heart of the mission is the construction of the universal cover (pp. 63–65): the points are homotopy classes of paths from $x_0$, the topology is generated by the sets $U_{[\gamma]}$ for $U$ in the basis of path-connected open sets on which $\pi_1$ dies, and one must verify that this is a topology basis, that $p$ is a covering map, and that the result is simply connected. Proposition 1.36 then passes to a quotient by $H$ and checks that the projection remains a covering map. Both are elementary but long, and formalizing them requires a systematic treatment of path homotopy classes as points of a space.
Propositions 1.37 and 1.39 follow from the lifting criterion and unique lifting; the deck-group homomorphism in 1.39(b) sends a loop in $N(H)$ to the deck transformation produced by the lifting criterion, and its kernel is computed by Proposition 1.31. Proposition 1.40(a) needs the quotient topology on $Y/G$ and the evenly covered neighborhoods $p(U)$ from condition $(\ast)$; part (b) is the observation that a deck transformation of a path-connected cover is determined by one value. Milestone 3 is orbit–stabilizer for the monodromy action.
## Formalization scope
* Spaces are arbitrary topological spaces; hypotheses (path-connectedness, local path-connectedness, semilocal simple connectivity, connectedness of the domain in Proposition 1.34) are stated per theorem, exactly where Hatcher assumes them.
* `CoveringSpace X` bundles a total space in the **same universe** as $X$ with a covering map; the classification quantifies over covering spaces in this sense. Since the universal cover and the coverings $X_H$ are constructed from paths in $X$, they live in that universe, so nothing is lost.
* "Isomorphic" is the existence of a homeomorphism over $X$ (Hatcher, p. 67), a proposition on pairs of covering spaces; Theorem 1.38 is stated as the three-part conjunction above rather than as a bijection between quotient sets, which avoids forming the set of isomorphism classes of types while asserting exactly the same content.
* Conjugacy is expressed with Mathlib's `MulAut.conj`; "number of sheets equals the index" is stated as a bijection $p^{-1}(x_0)\simeq\pi_1(X,x_0)/H$ with the coset space.
* The isomorphisms of Propositions 1.39(b) and 1.40(c) are stated as surjective homomorphisms with prescribed kernel, which is how Hatcher proves them and avoids requiring a `Normal` instance in the statement; the final clause of 1.39 and 1.40(b) are stated as the existence of group isomorphisms, the latter with its action on $Y$ prescribed.
* A covering space action includes continuity of each $y\mapsto gy$ (Hatcher's actions are by homeomorphisms). The orbit space is Mathlib's `MulAction.orbitRel.Quotient` with the quotient topology.
* Trivializing readings are excluded: path-connected spaces are nonempty, and a nonempty covering space of a path-connected base is surjective; milestone 6 assumes surjectivity explicitly because its base need not be connected.
Contributions welcome: a reusable construction of the space of path classes with its topology, the covering $X_H$, and the deck-group homomorphism; the short reductions to Mathlib for Propositions 1.31, 1.33 and 1.34 are good first contributions.
## Selected references
- A. Hatcher, *Algebraic Topology*, Cambridge University Press, 2002. Section 1.3, pp. 56–72. [https://pi.math.cornell.edu/~hatcher/AT/AT.pdf](https://pi.math.cornell.edu/~hatcher/AT/AT.pdf)
- E. H. Spanier, *Algebraic Topology*, Springer, 1966, Chapter 2 (covering spaces and the classification theorem).
- J. R. Munkres, *Topology*, 2nd ed., Prentice Hall, 2000, Chapter 13 (classification of covering spaces).
- Mathlib, `Mathlib/Topology/Covering/Basic.lean` (covering maps). [https://github.com/leanprover-community/mathlib4/blob/0df444a360eaa60ab8c11dca51a86af692955474/Mathlib/Topology/Covering/Basic.lean](https://github.com/leanprover-community/mathlib4/blob/0df444a360eaa60ab8c11dca51a86af692955474/Mathlib/Topology/Covering/Basic.lean)
- Mathlib, `Mathlib/Topology/Homotopy/Lifting.lean` (path and homotopy lifting, monodromy, the lifting criterion). [https://github.com/leanprover-community/mathlib4/blob/0df444a360eaa60ab8c11dca51a86af692955474/Mathlib/Topology/Homotopy/Lifting.lean](https://github.com/leanprover-community/mathlib4/blob/0df444a360eaa60ab8c11dca51a86af692955474/Mathlib/Topology/Homotopy/Lifting.lean)
- Mathlib, `Mathlib/Topology/Covering/Quotient.lean` (quotient covering maps for group actions). [https://github.com/leanprover-community/mathlib4/blob/0df444a360eaa60ab8c11dca51a86af692955474/Mathlib/Topology/Covering/Quotient.lean](https://github.com/leanprover-community/mathlib4/blob/0df444a360eaa60ab8c11dca51a86af692955474/Mathlib/Topology/Covering/Quotient.lean)
18 thms1 active userReviewed
🏆Completed
Captain: korbonits
Hatcher Algebraic Topology II: The van Kampen TheoremTextbook
## Motivation
Once $\pi_1(S^1)\cong\mathbb{Z}$ is known, the next question in Allen Hatcher's *Algebraic Topology* (Cambridge University Press, 2002; [pi.math.cornell.edu/~hatcher/AT/AT.pdf](https://pi.math.cornell.edu/~hatcher/AT/AT.pdf)) is how to compute fundamental groups of spaces built from pieces. Section 1.2 answers this with **van Kampen's theorem** (Theorem 1.20, p. 43): if a space is covered by open sets with a common basepoint and path-connected intersections, its fundamental group is the free product of the fundamental groups of the pieces, modulo relations coming from the intersections. It is the main computational tool of Chapter 1: it gives the fundamental groups of wedges of circles, graphs, surfaces, and every CW complex from its 2-skeleton (Propositions 1.26–1.28), and it underlies the classification of covering spaces in Section 1.3.
This is the second mission in the series formalizing Hatcher's book. The first mission established the covering-space lifting properties and $\pi_1(S^1,1)\cong\mathbb{Z}$ in the Lean namespace `Hatcher`; this one covers the subsection "The van Kampen Theorem" of Section 1.2 (pp. 41–47) together with its warm-up Lemma 1.15 and Proposition 1.14 from Section 1.1 (p. 35).
## Setting
Let $X$ be a topological space with a **basepoint** $x_0$. A **path** is a continuous map $I=[0,1]\to X$, a **loop** at $x_0$ is a path with both endpoints $x_0$, and $\pi_1(X,x_0)$ is the group of homotopy classes of loops at $x_0$ under concatenation. A continuous map $\varphi:X\to Y$ with $\varphi(x_0)=y_0$ **induces** a homomorphism $\varphi_*:\pi_1(X,x_0)\to\pi_1(Y,y_0)$, $[f]\mapsto[\varphi\circ f]$.
Let $(A_\alpha)_{\alpha\in\iota}$ be a family of subsets of $X$, each containing $x_0$, with the subspace topology; write $\pi_1(A_\alpha)$ for $\pi_1(A_\alpha,x_0)$. The inclusions $A_\alpha\hookrightarrow X$ induce
$$j_\alpha:\pi_1(A_\alpha)\to\pi_1(X),$$
which are `Hatcher.inclHom`, and the inclusions $A_\alpha\cap A_\beta\hookrightarrow A_\alpha$ and $A_\alpha\cap A_\beta\hookrightarrow A_\beta$ induce
$$i_{\alpha\beta}:\pi_1(A_\alpha\cap A_\beta)\to\pi_1(A_\alpha),\qquad i_{\beta\alpha}:\pi_1(A_\alpha\cap A_\beta)\to\pi_1(A_\beta),$$
which are `Hatcher.interHomLeft` and `Hatcher.interHomRight`.
The **free product** $\ast_\alpha G_\alpha$ of a family of groups is the group of reduced words in the $G_\alpha$ (Hatcher, pp. 41–42); in Lean it is Mathlib's `Monoid.CoprodI`, here `Hatcher.FreeProd`. Its universal property extends the $j_\alpha$ to a single homomorphism
$$\Phi:\ast_\alpha\pi_1(A_\alpha)\to\pi_1(X),$$
`Hatcher.vanKampenHom`. Since $j_\alpha i_{\alpha\beta}=j_\beta i_{\beta\alpha}$ (both are induced by $A_\alpha\cap A_\beta\hookrightarrow X$), the elements
$$i_{\alpha\beta}(\omega)\,i_{\beta\alpha}(\omega)^{-1},\qquad \omega\in\pi_1(A_\alpha\cap A_\beta),$$
lie in the kernel of $\Phi$. Let $N$ be the **normal subgroup generated** by all of them, `Hatcher.vanKampenNormal`.
## Formalization targets
### Goal (Theorem 1.20)
If $X$ is the union of path-connected open sets $A_\alpha$ each containing $x_0$, each $A_\alpha\cap A_\beta$ is path-connected, and each $A_\alpha\cap A_\beta\cap A_\gamma$ is path-connected, then
$$\Phi \text{ is surjective}\qquad\text{and}\qquad \ker\Phi=N .$$
Hence $\Phi$ induces an isomorphism $\pi_1(X)\cong\ast_\alpha\pi_1(A_\alpha)/N$.
### Milestones
1. **Lemma 1.15** (p. 35). If $X$ is the union of path-connected open sets $A_\alpha$ containing $x_0$ with each $A_\alpha\cap A_\beta$ path-connected, then every loop in $X$ at $x_0$ is homotopic to a product of loops each of which is contained in a single $A_\alpha$.
2. **Proposition 1.14** (p. 35). $\pi_1(S^n)=0$ for $n\ge 2$.
3. **Theorem 1.20, first part** (p. 43). Under the hypotheses of Lemma 1.15, $\Phi$ is surjective.
4. **The kernel contains the relators** (p. 43). $N\le\ker\Phi$, with no hypotheses on the cover.
5. **Theorem 1.20, second part** (p. 43). If moreover every triple intersection is path-connected, $\ker\Phi\le N$.
6. **Induced isomorphism** (p. 43). Under the same hypotheses there is an isomorphism $\ast_\alpha\pi_1(A_\alpha)/N\cong\pi_1(X)$ sending the class of a word to its image under $\Phi$.
## Significance
*The result itself.* Van Kampen's theorem is the gluing law for $\pi_1$. With it Hatcher computes $\pi_1$ of wedge sums (free products), of graphs (free groups), of the closed orientable surfaces (Example 1.26), and shows that attaching $2$-cells kills exactly the attaching loops (Proposition 1.26), so that every group is a fundamental group (Corollary 1.28). The surjectivity half alone gives Proposition 1.14, that spheres of dimension at least two are simply connected, and hence that $\mathbb{R}^2$ is not homeomorphic to $\mathbb{R}^n$ for $n\ne 2$ (Corollary 1.16).
*Formalizing it.* Mathlib has the fundamental groupoid and fundamental group, induced homomorphisms (`FundamentalGroup.map`), free products of groups (`Monoid.CoprodI`) with their universal property, normal closures, and quotient groups. It has no version of van Kampen's theorem for topological spaces (its `CategoryTheory/Limits/VanKampen` concerns colimits in categories, not fundamental groups), and no computation of $\pi_1(S^n)$ for $n\ge 2$; on the platform, however, the theorem `SP4Mission.sphere_simplyConnected` (already proved in this environment) states that the unit sphere of $\mathbb{R}^n$ is simply connected for $n\ge 3$, which is Proposition 1.14 with shifted indexing, so that milestone can be closed by a one-line reduction. The mission supplies the statements in Hatcher's form, on Mathlib's $\pi_1$, so that later missions (covering spaces, cell complexes) can use them directly.
## Difficulty
Surjectivity is a compactness argument: subdivide $I$ so each piece of the loop lies in one $A_\alpha$, then use path-connectedness of the intersections to connect the subdivision points back to $x_0$. The formal difficulty is bookkeeping: producing the subdivision from an open cover of $[0,1]$ (Mathlib's `exists_monotone_Icc_subset_open_cover_unitInterval` is the tool) and showing the reparametrised concatenation is homotopic to the original loop.
The kernel computation is the hard part. Hatcher's proof takes a homotopy $F:I\times I\to X$ between two factorizations, subdivides the square into rectangles each mapped into a single $A_\alpha$, perturbs the grid so at most three rectangles meet at a corner (this is where triple intersections enter), and then shows that moving the loop across one rectangle at a time changes the factorization only by the two elementary moves that hold in $\ast_\alpha\pi_1(A_\alpha)/N$. Every step is elementary, but the induction over the grid is long, and each elementary move requires an explicit path-homotopy in a subspace. The naive idea of proving $\ker\Phi\le N$ by an induction on word length does not work: the relation between two factorizations of the same loop is only visible through a homotopy in $X$, not through the words.
Proposition 1.14 is easy given Lemma 1.15 but requires exhibiting the cover of $S^n$ by two complements of antipodal points, showing each is simply connected (homeomorphic to $\mathbb{R}^n$ via stereographic projection, which Mathlib has as `stereographic`), and showing their intersection is path-connected when $n\ge 2$.
## Formalization scope
* The index set $\iota$ and the space $X$ are arbitrary; the $A_\alpha$ are `Set X` with the subspace topology, and $\pi_1(A_\alpha)$ is Mathlib's `FundamentalGroup ↥(A α) ⟨x₀, _⟩`. Hypotheses are stated explicitly on each theorem: `IsOpen`, `IsPathConnected`, `⋃ α, A α = Set.univ`, and path-connectedness of pairwise (and, where Hatcher requires it, triple) intersections.
* $i_{\alpha\beta}$ and $i_{\beta\alpha}$ are both defined on $\pi_1(A_\alpha\cap A_\beta)$ (rather than on $\pi_1(A_\beta\cap A_\alpha)$ for the second), so no identification of $A_\alpha\cap A_\beta$ with $A_\beta\cap A_\alpha$ is needed; the set of relators ranges over all ordered pairs $(\alpha,\beta)$.
* "Product of loops" in Lemma 1.15 is a finite `List` of loops, each tagged with the index $\alpha$ of the piece it lies in, concatenated right-to-left with the constant loop as empty product (`Hatcher.loopProd`). Any bracketing gives the same homotopy class.
* The goal is stated as the conjunction "surjective and $\ker\Phi=N$"; the isomorphism $\ast_\alpha\pi_1(A_\alpha)/N\cong\pi_1(X)$ is a separate milestone, stated as the existence of a group isomorphism compatible with $\Phi$ on the quotient, which pins it down uniquely.
* $S^n$ is `Metric.sphere (0 : EuclideanSpace ℝ (Fin (n+1))) 1`, and "$\pi_1(S^n)=0$" is Mathlib's `SimplyConnectedSpace` (path-connected with trivial fundamental group), which is what Hatcher means since $S^n$ is path-connected.
* Trivializing readings are excluded: the cover hypotheses do not force $\iota$ nonempty, but then $X=\bigcup A_\alpha=\varnothing$ contradicts the existence of $x_0$, so the statements are not vacuous in any interesting case, and $\Phi$ is the specific homomorphism induced by the inclusions.
Contributions welcome: the subdivision lemma for loops in an open cover, a reusable treatment of factorizations and their elementary moves, and the two-set special case $\pi_1(X)\cong(\pi_1(A)\ast\pi_1(B))/N$ as a corollary.
## Selected references
- A. Hatcher, *Algebraic Topology*, Cambridge University Press, 2002. Section 1.2, pp. 40–49; Lemma 1.15 and Proposition 1.14, p. 35. [https://pi.math.cornell.edu/~hatcher/AT/AT.pdf](https://pi.math.cornell.edu/~hatcher/AT/AT.pdf)
- E. R. van Kampen, *On the connection between the fundamental groups of some related spaces*, American Journal of Mathematics 55 (1933), 261–267. [https://doi.org/10.2307/2371128](https://doi.org/10.2307/2371128)
- H. Seifert, *Konstruktion dreidimensionaler geschlossener Räume*, Berichte Sächs. Akad. Leipzig 83 (1931), 26–66.
- Mathlib, `Mathlib/GroupTheory/CoprodI.lean` (free products of groups). [https://github.com/leanprover-community/mathlib4/blob/0df444a360eaa60ab8c11dca51a86af692955474/Mathlib/GroupTheory/CoprodI.lean](https://github.com/leanprover-community/mathlib4/blob/0df444a360eaa60ab8c11dca51a86af692955474/Mathlib/GroupTheory/CoprodI.lean)
- Mathlib, `Mathlib/AlgebraicTopology/FundamentalGroupoid/FundamentalGroup.lean` (fundamental group and induced homomorphisms). [https://github.com/leanprover-community/mathlib4/blob/0df444a360eaa60ab8c11dca51a86af692955474/Mathlib/AlgebraicTopology/FundamentalGroupoid/FundamentalGroup.lean](https://github.com/leanprover-community/mathlib4/blob/0df444a360eaa60ab8c11dca51a86af692955474/Mathlib/AlgebraicTopology/FundamentalGroupoid/FundamentalGroup.lean)
8 thms1 active userReviewed
Captain: ryanshin
Smooth 4-dimensional Poincaré conjecture: foundations and reductionsOpen Problem
## Motivation
The **smooth four-dimensional Poincaré conjecture** asks whether a smooth manifold with the topology of the four-sphere must also have its standard smooth structure, up to diffeomorphism. The distinction is between the existence of continuous coordinates and the compatibility of differentiable coordinates. The mission concerns this precise sphere question, listed as open in Problem 4.1 of *K3 — A New Problem List in Low-Dimensional Topology*. It does not treat a collection of algebraic obstructions as an existing proof of the conjecture. [Baykur–Kirby–Ruberman, Problem 4.1](https://math.berkeley.edu/sites/default/files/surv-295-ruberman-watermarked-author-pdf.pdf)
### Historical landmarks
- **1961:** Smale proved that a closed smooth manifold homotopy equivalent to a sphere of dimension at least five is homeomorphic to that sphere. This is not a theorem that all such smooth manifolds are diffeomorphic to the standard sphere. [Smale, Theorem A](https://www.math.uchicago.edu/~shmuel/tom-readings/Smale,%20PC.pdf)
- **1982:** Freedman established the topological four-dimensional Poincaré theorem: a topological four-manifold homotopy equivalent to the four-sphere is homeomorphic to it. [Freedman, Theorem 1.6](https://www.maths.gla.ac.uk/~mpowell/1982_The%20topology%20of%20four-dimensional%20manifolds.pdf)
- **2026:** The *K3* problem list continues to distinguish this established topological result from the open smooth sphere problem. [Problem 4.1, pp. 191–192](https://math.berkeley.edu/sites/default/files/surv-295-ruberman-watermarked-author-pdf.pdf)
## Setting
Let $S^4$ be the unit sphere in $ℝ^5$, with its standard stereographic smooth structure. A **homeomorphism** is a continuous bijection with continuous inverse; a **diffeomorphism** is a smooth bijection with smooth inverse. A **smooth atlas** is a collection of local Euclidean coordinates whose transition maps are smooth.
The manifold $M$ is compact and Hausdorff, has no boundary, and is equipped with a specified smooth atlas modeled on $ℝ^4$. The given atlas is arbitrary: it is not defined by transporting the standard structure from $S^4$.
For a homeomorphism $e:N\to S^4$, let $\mathcal A_e$ denote the atlas transported from the standard sphere along $e$. A **structomorphism** for the smooth structure groupoid is a homeomorphism whose coordinate expressions belong to that groupoid. The predicate $\mathsf{SPC4Pullback}$ requires, for every given smooth atlas $\mathcal A$ on such an $N$ and every such $e$, a structomorphism between $(N,\mathcal A)$ and $(N,\mathcal A_e)$. It does not require that structomorphism to be the identity. These are the conventions of the source definitions, not additional uniqueness assumptions. [Shin, *SPC4.lean*, lines 53–81 and 211–221]
## Formalization targets
### Main open goal
For every manifold $M$ with the preceding hypotheses, the goal is
$$
M\cong_{\mathrm{Top}}S^4
\quad\Longrightarrow\quad
M\cong_{\mathrm{Diff}}S^4.
$$
This is the source predicate $\mathsf{SPC4}$. Its conclusion asserts the existence of a diffeomorphism; it does not assert that a particular supplied homeomorphism is smooth.
### Structural and literature milestones
The atlas formulation has the exact equivalence
$$
\mathsf{SPC4}\quad\Longleftrightarrow\quad\mathsf{SPC4Pullback}.
$$
The source supplies a proof of this equivalence without invoking Freedman's theorem or assuming the conjecture as an unconditional fact. It is a reformulation, not a solution. Its foundations include the correspondence
$$
\operatorname{Structomorph}(\mathcal G^{\infty},M,N)
\simeq \operatorname{Diff}^{\infty}(M,N),
$$
where $\mathcal G^{\infty}$ is the smooth coordinate-change groupoid for the common model. [Shin, *SPC4.lean*, lines 334–365; *Bridge.lean*]
Write $F_4$ for the following compact Hausdorff, boundaryless instance of Freedman's topological theorem:
$$
M\simeq S^4\quad\Longrightarrow\quad M\cong_{\mathrm{Top}}S^4,
$$
where $\simeq$ denotes homotopy equivalence and only topological manifold charts are assumed. This is established mathematics, but a proof in the present formal development remains a target. If $\mathsf{SPC4Homotopy}$ denotes the analogous smooth conclusion from a homotopy equivalence, the relation to the main goal is recorded with its hypothesis visible:
$$
F_4\quad\Longrightarrow\quad
(\mathsf{SPC4}\Longleftrightarrow\mathsf{SPC4Homotopy}).
$$
Explicit standard-disk foundations form another track. For every $m\geq0$, they concern the manifold-with-boundary structure on $\overline B^{m+1}$, its boundary set $S^m$, and the smooth collar
$$
c:S^m\times[0,1]\longrightarrow\overline B^{m+1},
\qquad c(u,t)=(1-t/2)u.
$$
The collar is a closed embedding, has image
$$
\{z\in\overline B^{m+1}:\|z\|\geq1/2\},
$$
and satisfies $c(u,0)=u$, using the boundary inclusion. Its image is a neighborhood of every boundary point in the disk. A companion interface characterizes a $C^k$ map from a $C^k$ manifold with corners into the disk as precisely a continuous map whose inclusion into Euclidean space is $C^k$. These targets concern the actual disk smooth structure. [Shin, *Disk.lean*, lines 1076–1141 and 1263–1318]
### Topological two-disk gluing
For each integer $m\geq0$, let $D^{m+1}=\overline B^{m+1}$ be the closed unit disk in $\mathbb R^{m+1}$ and let $\varphi:S^m\to S^m$ be any homeomorphism of its boundary. The **twisted double** identifies the boundary point $u$ in a left copy of the disk with $\varphi(u)$ in a right copy. With the quotient topology, the target is
$$
X_\varphi:=\bigl(D^{m+1}_L\sqcup D^{m+1}_R\bigr)/(u_L\sim\varphi(u)_R)
\quad\cong_{\mathrm{Top}}\quad S^{m+1}.
$$
This statement is published as [SP4Gluing.twistedSphere_homeomorphic](https://prove2.me/theorems/fe8e71c7-85fd-4392-8327-453dda13f24c). The theorem and its supporting [continuity](https://prove2.me/theorems/e09b0118-b3a4-44e3-9ba2-e70fb31a2faa) and [injectivity](https://prove2.me/theorems/12c0403c-fdcf-4202-8b53-9f12893b568f) lemmas have accepted Lean proofs contributed by [carlok](https://prove2.me/users/fca9fd8a-84f4-46ca-8845-a4a2b665381d). All three accepted proofs have also been checked locally with their proved dependencies. It concerns these explicit topological quotients, not arbitrary homotopy spheres or a prescribed smooth structure.
### Seam–interior smooth compatibility
For every regional chart base point, the open-bicollar and left-interior transitions are smooth in both directions. Right-interior-to-seam smoothness requires smooth $\varphi^{-1}$; the reverse requires smooth $\varphi$. The [single compatibility target](https://prove2.me/theorems/f1e93fb9-c414-46aa-8b6c-fc6978243ee7) concerns exact overlap sources, combining four source results internally. It provides neither a global smooth-manifold instance nor smooth standardness. [Shin, *Hemisphere.lean*, lines 2439–3577]
## Significance
A proof of the main goal would identify every smooth structure in its stated sphere class with the standard one, up to diffeomorphism. A proof of the transported-atlas equivalence instead locates the same unresolved comparison in a different formal language. The distinction matters: constructing a smooth structure by transport is not the same as identifying an arbitrary pre-existing one.
The bridge, explicit disk atlas, and stated collar properties have accepted kernel-checked Lean proofs. The clean atlas equivalence also has a proof with no admitted theorem among its axioms. The conjecture remains open, and Freedman's topological theorem remains unproved in this formal development despite its published mathematical proof.
The [topological two-disk gluing result](https://prove2.me/theorems/fe8e71c7-85fd-4392-8327-453dda13f24c) identifies the homeomorphism type of these quotients for every boundary homeomorphism and every disk dimension at least one. The accepted formalization supplies a global topological comparison for this explicit quotient. It does not resolve the comparison with a prescribed smooth structure or recognition of general smooth four-manifolds.
Four supporting algebraic tracks concern orbit coinvariants, homology dimension budgets, finite-support shift rigidity, and Laurent-polynomial positivity. Their source results arose in route-specific obstruction studies. As of 6 September 2026, all eleven theorem targets in these algebraic tracks have accepted Lean proofs. The five additional formal proofs were contributed by [wamlart](https://prove2.me/users/70d2064f-6b47-4a3f-bb90-74e71a55cbb7): [orbit augmentation](https://prove2.me/theorems/85478003-b7db-44ef-be81-1c0fc5d7a8b4), [region homology budgets](https://prove2.me/theorems/e3d78c98-ef71-4b2a-a04a-7fd93fe9246f), [two-corner homology budgets](https://prove2.me/theorems/f6cc0221-29eb-4e8a-9649-8856b2954f2a), [the Laurent mass threshold](https://prove2.me/theorems/2d22450e-c4ce-4a0c-8829-b51d65e80eb5), and [mass-two positivity](https://prove2.me/theorems/988bc029-7a8a-43d7-9413-9e9cc3f86c24). No theorem currently connects their completion to a proof or disproof of $\mathsf{SPC4}$. They are exploratory tools, not established milestones in a proof of the main goal.
## Difficulty
A homeomorphism can transport the standard atlas, but that observation does not compare the transported atlas with the one already specified on the manifold. Treating those two atlases as equal would remove the central mathematical question by changing its hypotheses.
Likewise, topological recognition does not supply a smooth recognition theorem. Standard disk and collar constructions establish local models; they do not establish a smooth gluing or recognition theorem for an arbitrary prescribed smooth structure, a recognition theorem for arbitrary smooth balls, or a smooth Schoenflies theorem. The missing global comparison cannot be replaced by successful finite algebraic tests or by constructing a standard local chart.
## Formalization scope
The sphere goal quantifies over `Type` in universe zero, exactly as in the source. It uses real four-dimensional Euclidean chart models, compactness, the Hausdorff condition, and smoothness of order $\infty$. Boundaryless manifolds are built into that model. No orientation, fixed parametrization, or identity-map uniqueness is imposed.
The geometric foundations use charted spaces, structure groupoids, models with corners, homotopy equivalences and diffeomorphisms. Disk results include every $m\geq0$, so their dimensions are $m+1\geq1$. The boundary-set identification does not by itself construct a general induced smooth boundary structure. Nor is smoothness asserted for a radial clamp across its nonsmooth locus.
The separate source assertion `SPC4Ball` is not treated as equivalent to the sphere goal: the required formal boundary, capping and gluing bridge is absent. The transported-annulus product diffeomorphism is not a current target; its chart instances serve only as constructor support. No unconditional implication is taken through the source's admitted Freedman declaration. Gaussian coupling, transport defects, partition incidence and merge-score results remain outside this mission because no mathematical dependency on them has been established.
## Selected references
- R. İnanç Baykur, Robion C. Kirby and Daniel Ruberman, eds., *K3 — A New Problem List in Low-Dimensional Topology*, Mathematical Surveys and Monographs 295, American Mathematical Society, 2026, Problem 4.1, pp. 191–192. [Author PDF](https://math.berkeley.edu/sites/default/files/surv-295-ruberman-watermarked-author-pdf.pdf).
- Michael Hartley Freedman, *The topology of four-dimensional manifolds*, Journal of Differential Geometry 17 (1982), 357–453, Theorem 1.6, p. 371. [DOI](https://doi.org/10.4310/jdg/1214437136); [primary-article scan](https://www.maths.gla.ac.uk/~mpowell/1982_The%20topology%20of%20four-dimensional%20manifolds.pdf).
- Stephen Smale, *Generalized Poincaré's Conjecture in Dimensions Greater Than Four*, Annals of Mathematics 74 (1961), 391–406, Theorem A. [DOI](https://doi.org/10.2307/1970239); [primary-article scan](https://www.math.uchicago.edu/~shmuel/tom-readings/Smale,%20PC.pdf).
- Ryan Shin, *SPC4.lean*, *Bridge.lean* and *Disk.lean*, unpublished source files, 2026; no public manuscript URL available. SHA-256, respectively: `b17fdb932034e5211d0db8171c08e2b3a182016bceaecdd2deb49c39d6bfd5cc`, `e8ea6b66f6bd675ca272e862e0825ab2db1f8bb792eaffe1b9e8f5d89024d302`, `889a9eccf9d2350aee7051ab7b6895e565f9f1a0c84e7120fb45c15acae0097e`.
- Ryan Shin, *Hemisphere.lean*, unpublished Lean source file, 2026, declaration `twistedSphereHomeoSphere`; source SHA-256 `c48843d2c4ec6987acfd7f7ab3a92bfed990376206142e74712795b4e9399828`. [Published topological two-disk gluing target](https://prove2.me/theorems/fe8e71c7-85fd-4392-8327-453dda13f24c); the recovered local construction is checked; the accepted proof and its two supporting lemmas were contributed by carlok.
60 thms5 active usersReviewed
🏆Completed
Captain: korbonits
Hatcher Algebraic Topology I: The Fundamental Group of the CircleTextbook
## 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](https://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 `Path`s; 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](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](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](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](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](https://github.com/leanprover-community/mathlib4/blob/0df444a360eaa60ab8c11dca51a86af692955474/Mathlib/AlgebraicTopology/FundamentalGroupoid/FundamentalGroup.lean)