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