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