Algebraic Topology

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

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

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:

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

Formalization targets

Goal — Teorema 3.15, with the isomorphism pinned on generators

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

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

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

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

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

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)

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

Motivation

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

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

Setting

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

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

is Hatcher.circleCover. The loops

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:

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)

Significance

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

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

Difficulty

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

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

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

Formalization scope

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

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

Selected references

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

Motivation

How many ways can a closed orientable surface of genus $g$ be "coloured" by a finite group $G$? Precisely: how many group homomorphisms $\pi_1(\Sigma_g)\to G$ are there? The answer is the partition function of two-dimensional Dijkgraaf–Witten theory with gauge group $G$. That theory is the simplest topological quantum field theory (TQFT) in the sense of Atiyah and Segal, and the standard test case for gauge theory with a finite gauge group (Dijkgraaf–Witten 1990, Freed–Quinn 1993). The count has a closed form in terms of the dimensions of the irreducible representations of $G$ alone. It is known as Mednykh's formula.

Timeline. Frobenius (1896) counted pairs with a prescribed commutator, $\#\{(a,b):[a,b]=z\}$, in terms of characters, which is the genus-one case. Frobenius and Schur (1906) treated the non-orientable analogue. Mednykh (1978) proved the formula for every genus using character theory and the standard presentation of $\pi_1(\Sigma_g)$. It was rediscovered in physics as the partition function of 2D and 3D finite-gauge-group TQFTs (Freed–Quinn 1993), and reproved with matrix integrals (Mulase–Yu 2005) and with lattice TQFTs (Snyder 2007). The last paper fixes the form of the statement used here.

Setting

Let $G$ be a finite group. A surface tuple of genus $g$ in $G$ is a family $x=((x_1,y_1),\dots,(x_g,y_g))\in(G\times G)^g$. Its commutator product is

multiplied left to right. For $z\in G$ let $N_g(z)=\#\{x\in(G\times G)^g:\mathrm{commProd}(x)=z\}$ (commCount G g z). The surface group $\Gamma_g$ (SurfaceGroup g) is the presented group

the standard presentation of the fundamental group of the closed orientable surface $\Sigma_g$ of genus $g$, whose Euler characteristic is $\chi(\Sigma_g)=2-2g$.

A complete irreducible family (IrrepFamily G ι) is a finite family $(V_i)_{i\in\iota}$ of finite-dimensional complex representations of $G$ that are irreducible, pairwise non-isomorphic, and such that every irreducible finite-dimensional complex representation is isomorphic to some $V_i$. Write $d_i=\dim_{\mathbb C}V_i$ and $\chi_i(g)=\operatorname{tr}V_i(g)$ for the character.

Formalization targets

Goal: Mednykh's formula

For every finite group $G$, every complete irreducible family and every $g\ge 0$,

which is Mulase–Yu, Thm. 1.1 and Snyder, eq. (1) with $\chi(S)=2-2g$. Equivalently, $\#\operatorname{Hom}(\Gamma_g,G)=|G|\sum_i(|G|/d_i)^{2g-2}$. Exponents are integers: at $g=0$ the formula reads $\sum_i d_i^2=|G|$.

Milestones

The milestones follow the algebraic proof of the counting formula recorded in Mulase–Yu 2002, §4, which goes back to Frobenius and Mednykh. Write $(x\star y)(w)=\sum_{\sigma\in G}x(w\sigma^{-1})\,y(\sigma)$ for the convolution of functions on $G$.

• M0. A complete irreducible family exists, with finite index type.
• M1. $\#\operatorname{Hom}(\Gamma_g,G)=N_g(1)$.
• M2. $\sum_i d_i\,\chi_i(z)=|G|$ if $z=1$ and $0$ otherwise.
• M3. For irreducible $V$ of dimension $d$: \sum_{a\in G}\chi_V(axa^{-1}y)=rac{|G|}{d}\chi_V(x)\chi_V(y).
• M4 (Mulase–Yu eq. (4.2)). For irreducible $V,W$: $\chi_V\star\chi_W$ equals rac{|G|}{d_V}\chi_V if $V\cong W$ and $0$ otherwise.
• M5 (Frobenius). $N_1(z)=|G|\sum_i\chi_i(z)/d_i$.
• M6. $N_{g_1+g_2}=N_{g_1}\star N_{g_2}$.
• M7 (Mulase–Yu Thm. 4.1). $N_g(z)=|G|^{2g-1}\sum_i\chi_i(z)\,d_i^{\,1-2g}$ for all $g\ge0$, $z\in G$. Mulase–Yu state it for $g\ge1$; the case $g=0$ is M2.

Significance

The result. The formula says that the number of $G$-coloured genus-$g$ surfaces is a function of the multiset of irreducible dimensions alone. Two groups with the same character degrees (for example $D_4$ and $Q_8$, both with degrees $1,1,1,1,2$) have equally many homomorphisms from every surface group, even though the groups are not isomorphic. In TQFT language the left side is the evaluation $\varepsilon(h^{g})$ of the Frobenius algebra $Z(\mathbb C[G])$, where $h$ is its handle element. The right side is the gauge-theoretic state sum. The identity is the two-dimensional instance of the agreement between the Atiyah–Segal gluing description and the path-integral description of a TQFT. It also gives the volume of the moduli space of flat $G$-bundles on $\Sigma_g$, and it underlies counts of covering spaces of surfaces.

Formalizing it. The theorem is classical and fully proved; to our knowledge it has no machine-checked proof. Mathlib has characters of finite-dimensional representations, their orthonormality (FDRep.char_orthonormal) and Maschke's theorem. It lacks the completeness of irreducible characters, the column orthogonality relation (M2), and any statement linking class sums to characters (M3). These are reusable well beyond this mission. The mission also produces the first formal link between a surface-group presentation and representation theory.

Difficulty

The available orthogonality is the row relation between two irreducible characters. Every step here needs the column relation M2, $\sum_i d_i\chi_i(z)=|G|\delta_{z,1}$. That relation is equivalent to the decomposition of the regular representation $\mathbb C[G]\cong\bigoplus_i V_i^{\oplus d_i}$, and in particular to the finiteness and completeness of the irreducible family. Mathlib has no such decomposition. The convolution identity M4 must also be established in its non-isomorphic case, which the row relation alone does not give in convolution form. The passage from $\operatorname{Hom}(\Gamma_g,G)$ to tuples (M1) depends on the universal property of PresentedGroup and on using one ordering of the commutator product throughout. A proof that bypasses characters by brute counting is not available for general $G$.

Formalization scope

All representations are over $\mathbb C$: FDRep ℂ G with G : Type a Group with [Fintype G]. Characters are FDRep.character and $d_i$ is Module.finrank ℂ (V i). Counts are Nat.card. Powers with exponents depending on $g$ are integer powers (zpow) in $\mathbb C$, so $g=0$ is included and no natural-number truncation occurs. $\Gamma_g$ is PresentedGroup on generators Fin g × Bool, with $a_j=(j,\mathrm{false})$, $b_j=(j,\mathrm{true})$ and the single relator (List.ofFn fun j => ⁅a_j, b_j⁆).prod. This is the standard presentation and stands in for $\pi_1(\Sigma_g)$, since Mathlib has no fundamental groups of closed surfaces. The goal quantifies over every complete irreducible family. M0 shows that such families exist, so the goal is not vacuous. Because the family must be complete and pairwise non-isomorphic, it cannot be chosen to make the sums trivial.

Out of scope: the non-orientable formula of Frobenius–Schur (it needs Frobenius–Schur indicators), positive characteristic, and the bordism-category formulation of TQFTs. Reusable contributions are especially welcome: the decomposition of the regular representation, column orthogonality, and the class-sum Schur lemma.

Selected references

• N. Snyder, Mednykh's formula via lattice topological quantum field theories, arXiv:math/0703073 (2007). https://arxiv.org/abs/math/0703073
• A. D. Mednykh, Determination of the number of nonequivalent coverings over a compact Riemann surface, Dokl. Akad. Nauk SSSR 239 (1978) 269–271; English transl. Soviet Math. Dokl. 19 (1978) 318–320.
• R. Dijkgraaf, E. Witten, Topological gauge theories and group cohomology, Commun. Math. Phys. 129 (1990) 393–429. https://doi.org/10.1007/BF02096988
• D. S. Freed, F. Quinn, Chern–Simons theory with finite gauge group, Commun. Math. Phys. 156 (1993) 435–472. https://arxiv.org/abs/hep-th/9111004
• M. Mulase, J. T. Yu, A generating function of the number of homomorphisms from a surface group into a finite group, arXiv:math/0209008 (2002), §4 (algebraic proof). https://arxiv.org/abs/math/0209008
• M. Mulase, J. T. Yu, Non-commutative matrix integrals and representation varieties of surface groups in a finite group, Ann. Inst. Fourier 55 (2005) 1001–1036. https://arxiv.org/abs/math/0211127
• J. Kock, Frobenius Algebras and 2D Topological Quantum Field Theories, LMS Student Texts 59, Cambridge Univ. Press (2003). https://doi.org/10.1017/CBO9780511615443

Motivation

The Conley–Zehnder index assigns an integer to a path of symplectic matrices that starts at the identity and ends at a matrix without eigenvalue $1$. It is how periodic orbits of Hamiltonian and Reeb flows get graded. In Floer homology it gives the grading of the chain complex, generated by the $1$-periodic orbits of a nondegenerate Hamiltonian (Salamon–Zehnder 1992; Salamon 1999). In contact homology and symplectic field theory it grades Reeb orbits. In the analysis of pseudoholomorphic curves it enters the Fredholm index formula for the linearized Cauchy–Riemann operator through the asymptotic orbits. In three-dimensional Reeb dynamics it defines dynamical convexity (every periodic orbit has index at least $3$), the hypothesis of the Hofer–Wysocki–Zehnder theorem on disk-like global surfaces of section (HWZ 1998).

Timeline. Conley and Zehnder introduced the index in their Morse-type index theory for periodic solutions of Hamiltonian equations (Conley–Zehnder 1984). Salamon and Zehnder gave the definition through a rotation function $\rho : \mathrm{Sp}(2n) \to S^1$ and related it to the Maslov index (SZ92). Robbin and Salamon extended it to arbitrary paths as a half-integer Maslov-type index (Robbin–Salamon 1993). Gutt attributes the properties naturality, homotopy, zero, product, loop, signature, determinant and inverse, and the characterization of the index by homotopy, loop and signature alone, to Salamon's lecture notes (Sal99) and to Audin–Damian (AD14); the statements used here are those of Gutt, Propositions 8–9. Gutt gives a self-contained account with several equivalent formulas, including the normalized complex determinant of the complex-linear part used below (Gutt 2014, §2).

Setting

Write $\mathbb{R}^{2n}$ with coordinates $(q,p)$ and let

The symplectic group $\mathrm{Sp}(2n)$ is the set of real $2n\times 2n$ matrices $A$ with $A J_0 A^{\mathsf T} = J_0$. Let $\mathrm{Sp}^*(2n)$ be the set of $A \in \mathrm{Sp}(2n)$ with $\det(\mathrm{Id} - A) \neq 0$.