Prove2Me

The exponent-sum homomorphism Bn→ZB_n \to \mathbb{Z}

Proved
BraidsLinksMCG.braid_exponent_sum_hom

by Gabewhigham · Sep 14, 2026 · Mathlib 0df444a (Lean v4.33.1)

algebraic-topologybraid-groupsgroup-theory

The exponent sum of a braid word is an invariant of the braid.

Let BnB_n be the abstract braid group with Artin generators σ1,…,σn−1\sigma_1,\dots,\sigma_{n-1} and the defining relations

σiσj=σjσi (∣i−j∣≥2),σiσi+1σi=σi+1σiσi+1.\sigma_i\sigma_j=\sigma_j\sigma_i\ (|i-j|\ge 2),\qquad \sigma_i\sigma_{i+1}\sigma_i=\sigma_{i+1}\sigma_i\sigma_{i+1}.

The assertion is that there is a group homomorphism

ε:Bn⟶Z,ε(σi)=1for every i,\varepsilon : B_n \longrightarrow \mathbb{Z}, \qquad \varepsilon(\sigma_i) = 1 \quad \text{for every } i,

so that the number of positive crossings minus the number of negative crossings in a braid word depends only on the braid it represents. Both families of defining relations preserve the number of letters counted with sign, which is what makes the assignment well defined.

The homomorphism ε\varepsilon is the abelianization map of BnB_n: since all generators are conjugate, any homomorphism to an abelian group factors through it. It is the standard device for showing that a given braid is non-trivial, or that an element has infinite order, and it is used in particular for the generator of the centre of BnB_n.

Formalization Note Braid generators are indexed by Fin(n−1)\mathrm{Fin}(n-1) with truncated subtraction, so there are no generators when n≤1n \le 1. The target group Z\mathbb{Z} is written multiplicatively, and ε(σi)\varepsilon(\sigma_i) is the element corresponding to the integer 11.

Preamble
import Definitions.Def_BraidsLinksMCG_ArtinBraidGroup
import Definitions.Def_BraidsLinksMCG_ArtinEndo
Formal statement
namespace BraidsLinksMCG

theorem braid_exponent_sum_hom (n : ℕ) :
    ∃ eps : ArtinBraidGroup n →* Multiplicative ℤ,
      ∀ i : Fin (n - 1), eps (sigma i) = Multiplicative.ofAdd (1 : ℤ) := by sorry

end BraidsLinksMCG
Source
Joan S. Birman, *Braids, Links, and Mapping Class Groups*, Annals of Mathematics Studies 82, Princeton University Press, 1974, Chapter 1, relations (1-1) and (1-2), p. 11; the exponent sum is used in the discussion of the centre, Corollary 1.8.4, p. 28

View graph