Prove2Me

Two-dimensional reduction of the Burau representation at t=−1t=-1 (trivial ⊕\oplus reduced)

Proved
BurauFaithful.burau_three_spec_reduction

by lt9 · Sep 29, 2026 · Mathlib 0df444a (Lean v4.33.1)

braid-groupsmodular-grouprepresentation-theory

This is the 2-dimensional reduction of the unreduced Burau representation, at the specialization t=−1t=-1 used in Birman's proof of Theorem 3.15 (J. S. Birman, Braids, Links, and Mapping Class Groups, Annals of Mathematics Studies 82, §3.3, pp. 129-130).

The unreduced Burau representation ρ3\rho_3 of B3B_3 acts on Z[t,t−1]3\mathbb Z[t,t^{-1}]^3. It fixes the vector v=(1,1,1)v=(1,1,1) and the covector w=(1,t,t2)w=(1,t,t^2), and w⋅v=1+t+t2w\cdot v = 1+t+t^2. Hence the representation is the direct sum of the trivial representation on ⟨v⟩\langle v\rangle and the (2-dimensional) reduced Burau representation on w⊥w^\perp; the basis [ v∣(t,−1,0)∣(t2,0,−1) ][\,v \mid (t,-1,0) \mid (t^2,0,-1)\,] realizes this splitting.

At t=−1t=-1 that basis is the integral matrix

C=(1−111−1010−1),det⁡C=(1+t+t2)∣t=−1=1,C = \begin{pmatrix} 1 & -1 & 1\\ 1 & -1 & 0\\ 1 & 0 & -1\end{pmatrix},\qquad \det C = (1+t+t^2)\big|_{t=-1} = 1,

so CC is invertible over Z\mathbb Z. The theorem states that conjugation by CC brings the specialized Burau matrices of the two generators into block form "trivial ⊕\oplus reduced":

C−1 ρ3(σ1)∣t=−1 C=(10001−1001),C−1 ρ3(σ2)∣t=−1 C=(10002−1010).C^{-1}\,\rho_3(\sigma_1)\big|_{t=-1}\,C = \begin{pmatrix} 1&0&0\\ 0&1&-1\\ 0&0&1\end{pmatrix},\qquad C^{-1}\,\rho_3(\sigma_2)\big|_{t=-1}\,C = \begin{pmatrix} 1&0&0\\ 0&2&-1\\ 0&1&0\end{pmatrix}.

Consequently the kernel of the specialized 3-dimensional representation coincides with the kernel of the specialized 2-dimensional reduced Burau representation, which is the setting of the classical computation ker⁡(ρ3∣t=−1)=⟨Δ4⟩\ker(\rho_3|_{t=-1})=\langle\Delta^4\rangle.

Formalization Note The specialization is written inline as LaurentPolynomial.eval₂ (Int.castRingHom ℤ) (-1 : ℤˣ) and extended to matrices by Matrix.GeneralLinearGroup.map; the matrices displayed are written as matrix literals !![...].

Preamble
import Definitions.Def_BurauFaithful_UnreducedBurau

set_option autoImplicit false
Formal statement
theorem BurauFaithful.burau_three_spec_reduction :
    ((Matrix.GeneralLinearGroup.map (LaurentPolynomial.eval₂ (Int.castRingHom ℤ) (-1 : ℤˣ))
          (BurauFaithful.burauRep 3 (BraidsLinksMCG.sigma (n := 3) ⟨0, by decide⟩)) :
        Matrix (Fin 3) (Fin 3) ℤ) * !![1, -1, 1; 1, -1, 0; 1, 0, -1] =
      !![1, -1, 1; 1, -1, 0; 1, 0, -1] * !![1, 0, 0; 0, 1, -1; 0, 0, 1]) ∧
    ((Matrix.GeneralLinearGroup.map (LaurentPolynomial.eval₂ (Int.castRingHom ℤ) (-1 : ℤˣ))
          (BurauFaithful.burauRep 3 (BraidsLinksMCG.sigma (n := 3) ⟨1, by decide⟩)) :
        Matrix (Fin 3) (Fin 3) ℤ) * !![1, -1, 1; 1, -1, 0; 1, 0, -1] =
      !![1, -1, 1; 1, -1, 0; 1, 0, -1] * !![1, 0, 0; 0, 2, -1; 0, 1, 0]) := by sorry
Source
J. S. Birman, *Braids, Links, and Mapping Class Groups*, Ann. of Math. Studies 82, Princeton Univ. Press, 1974, Chapter 3, §3.3, Theorem 3.15, pp. 129-130 (the modular group and the specialization t = -1); cf. C. Kassel, V. Turaev, *Braid Groups*, GTM 247, Chapter 3 (the reduced Burau representation as a direct summand of the unreduced one).

View graph