Teorema 3.15 (Artin): $\pi_1(B_{0,n}E^2) \cong \langle \sigma_i \mid \text{braid relations}\rangle$ , generator by generator

Open

TarchaBraids.thm_3_15_artin_presentation

by Lucas · Sep 19, 2026 · Mathlib 0df444a (Lean v4.33.1)

algebraic-topologybraid-groupsfundamental-groupgroup-theory

This is the capstone of the dissertation, Teorema 3.15: for $n \ge 1$ the braid group on $n$ strands admits the presentation

B_n = \bigl\langle \sigma_1,\dots,\sigma_{n-1} \;\bigm|\; \sigma_i\sigma_j = \sigma_j\sigma_i \ (|i-j| \ge 2), \quad \sigma_i\sigma_{i+1}\sigma_i = \sigma_{i+1}\sigma_i\sigma_{i+1} \bigr\rangle .

The proof in the dissertation constructs the map $\varphi$ from the presented group to the braid group determined on generators by $\varphi(x_i) = [\sigma_i]$ , checks that it is a well-defined homomorphism, that it is surjective (Teorema 3.11) and that it is injective (the analysis of elementary moves, Figuras 3.18–3.27).

Accordingly the statement formalized here is not merely that the two groups are abstractly isomorphic: it asserts the existence of a group isomorphism

\varphi : B_n \xrightarrow{\ \sim\ } \pi_1\bigl(B_{0,n}E^2, *\bigr)

from the presented group onto the fundamental group of the unordered configuration space of $n$ points of the plane, which sends each abstract generator $\sigma_{i+1}$ to the class of the elementary half-twist interchanging the base points $i+1$ and $i+2$ . Fixing the isomorphism on generators is what makes the presentation usable for computation with concrete braids.

The statement is asserted for every $n$ ; the degenerate cases $n = 0$ and $n = 1$ assert an isomorphism between two trivial groups.

Preamble

import Mathlib
import Definitions.Def_BraidsLinksMCG_ArtinBraidGroup
import Definitions.Def_BraidsLinksMCG_ConfigSpace
import Definitions.Def_TarchaBraids_HalfTwist

Formal statement

namespace TarchaBraids

open BraidsLinksMCG

theorem thm_3_15_artin_presentation (n : ℕ) :
    ∃ f : ArtinBraidGroup n ≃* GeomBraidGroup n,
      ∀ i : Fin (n - 1), f (sigma i) = halfTwistBraid n i := by sorry

end TarchaBraids

Source

Alexsander Andrey Gomes Tarcha, *Um Estudo Introdutório da Teoria de Tranças*, Dissertação (Mestrado Profissional em Matemática), IGCE, UNESP, Rio Claro, 2023, orientadora Alice Kimie Miwa Libardi, Teorema 3.15, p. 57 (demonstração pp. 57–62); a relação de trança impressa no enunciado do teorema contém uma errata tipográfica ("σ_i·σ_{i+1}·σ_{i+1} = σ_i·σ_{i+1}"), corrigida aqui para σ_i σ_{i+1} σ_i = σ_{i+1} σ_i σ_{i+1}, que é a relação usada na demonstração e na Proposição 3.14

Read-back

What the Lean code literally says, in plain math · aristotle-harmonic

Provenance — non-blind read-back. This read-back was written by the same agent that drafted the Lean statements of this proposal, at the explicit instruction of the mission owner, and not by an independent auditor working blind from the code alone. It is therefore not independent testimony: the author already knew what the code was intended to say, which is exactly the bias the read-back procedure is meant to exclude. Reviewers should treat it as the author's own restatement and check it against the Lean source directly.

Fix a natural number $n$ . Two groups are involved.

The first is the abstract group presented by generators indexed by $0, 1, \dots, n-2$ subject to Artin's relators: for indices $i, j$ whose difference has absolute value at least $2$ , the relator $\sigma_i\sigma_j\sigma_i^{-1}\sigma_j^{-1}$ ; and for indices $i, j$ with $j = i+1$ , the relator $\sigma_i\sigma_j\sigma_i(\sigma_j\sigma_i\sigma_j)^{-1}$ . Concretely this is the free group on the index set modulo the normal subgroup generated by those words.

The second is the fundamental group of the unordered configuration space of $n$ points of the plane — ordered $n$ -tuples of pairwise distinct complex numbers, modulo relabelling, with the quotient topology — based at the class of the configuration $(1, 2, \dots, n)$ .

The claim asserts the existence of a map $\varphi$ between them such that:

$\varphi$ is a multiplicative isomorphism from the presented group onto the fundamental group, that is, a bijection preserving products (and therefore the identity and inverses);
for every generator index $i \in \{0,\dots,n-2\}$ , $\varphi$ sends the image of the $i$ -th generator of the presentation to the homotopy class of the elementary half-twist loop with index $i$ : the loop that rotates the two base points $i+1$ and $i+2$ counterclockwise through the angle $\pi$ about their midpoint $i + \tfrac32$ , at distance $\tfrac12$ from it, while the remaining points stay fixed.

No uniqueness of $\varphi$ is claimed, and nothing is asserted about the images of elements other than the generators beyond what multiplicativity forces. For $n = 0$ and for $n = 1$ the index set is empty, the presented group is trivial, and the claim is that the fundamental group in question is trivial as well.

Human review

Endorsed by Shuze Chen · Sep 19, 2026
Endorsed by Lucas · Sep 19, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Teorema 3.15 (Artin): π1(B0,nE2)≅⟨σi∣braid relations⟩\pi_1(B_{0,n}E^2) \cong \langle \sigma_i \mid \text{braid relations}\rangleπ1​(B0,n​E2)≅⟨σi​∣braid relations⟩, generator by generator

Teorema 3.15 (Artin): $\pi_1(B_{0,n}E^2) \cong \langle \sigma_i \mid \text{braid relations}\rangle$ , generator by generator