Power form of the kernel of the reduced Burau specialization at t = -1

Open

BurauFaithful.reducedBurau_spec_kernel_power_v2

by lt9 · Oct 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

algebraic-topologybraid-groupsgroup-theory

Power form of the kernel of the reduced Burau specialization at $t=-1$ .

Let $\varphi : B_3 \to \mathrm{SL}(2,\mathbb{Z})$ be the specialization at $t=-1$ of the reduced Burau representation of the three-strand braid group, sending the Artin generators to

\sigma_1 \mapsto \begin{pmatrix} 1 & -1 \\ 0 & 1 \end{pmatrix}, \qquad \sigma_2 \mapsto \begin{pmatrix} 2 & -1 \\ 1 & 0 \end{pmatrix}.

The kernel of $\varphi$ consists of the integral powers of the full twist squared:

\varphi(\beta) = 1 \;\Longrightarrow\; \exists\, k \in \mathbb{Z},\quad \beta = (\sigma_1\sigma_2)^{6k}.

Since $\Delta^4 = (\sigma_1\sigma_2)^6$ is central in $B_3$ , this is the explicit form of the statement that $\varphi$ induces an injection $B_3/\langle\!\langle\Delta^4\rangle\!\rangle \hookrightarrow \mathrm{SL}(2,\mathbb{Z})$ . The quotient is the amalgam $C_4 *_{C_2} C_6$ obtained by adjoining $x^4 = 1$ to the trefoil group $\langle x, y \mid x^2 = y^3\rangle$ ; it is generated by the classes of $\sigma_0^2\sigma_1$ and $\sigma_0\sigma_1$ , whose images $A^2B$ and $AB$ generate $\mathrm{SL}(2,\mathbb{Z})$ , and being finitely generated and residually finite it is Hopfian by Malcev's theorem, so that surjection onto the modular group is an isomorphism and the kernel is exactly $\langle\!\langle\Delta^4\rangle\!\rangle$ .

Preamble

import Definitions.Def_BurauFaithful_UnreducedBurau

set_option autoImplicit false

open Matrix BraidsLinksMCG

/-- The images of the two Artin generators under the `t = -1` specialization of the reduced
Burau representation (the two integral matrices of `BurauFaithful.burau_three_spec_reduction`). -/
noncomputable def BurauFaithful.redGen : Fin 2 → Matrix.SpecialLinearGroup (Fin 2) ℤ :=
  fun i => if (i : ℕ) = 0 then ⟨!![1, -1; 0, 1], by decide⟩ else ⟨!![2, -1; 1, 0], by decide⟩

lemma BurauFaithful.redGen_braid :
    ∀ r ∈ braidRels 3, FreeGroup.lift BurauFaithful.redGen r = 1 := by
  intro r hr
  simp only [braidRels, Set.mem_union] at hr
  rcases hr with ⟨i, j, h, rfl⟩ | ⟨i, j, h, rfl⟩
  · exfalso
    fin_cases i <;> fin_cases j <;> norm_num at h
  · simp only [map_mul, map_inv, FreeGroup.lift_apply_of]
    rw [mul_inv_eq_one]
    fin_cases i <;> fin_cases j <;>
      first
        | (exfalso; omega)
        | (ext a b; fin_cases a <;> fin_cases b <;> decide)

/-- The `t = -1` specialization of the reduced Burau representation of `B₃`, as a homomorphism
sending the generators to `!![1, -1; 0, 1]` and `!![2, -1; 1, 0]`. -/
noncomputable def BurauFaithful.redHom3 :
    BraidsLinksMCG.ArtinBraidGroup 3 →* Matrix.SpecialLinearGroup (Fin 2) ℤ :=
  PresentedGroup.toGroup BurauFaithful.redGen_braid

Formal statement

namespace BurauFaithful

theorem reducedBurau_spec_kernel_power_v2 (β : BraidsLinksMCG.ArtinBraidGroup 3) : BurauFaithful.redHom3 β = 1 → (∃ k : ℤ, β = (BraidsLinksMCG.sigma ⟨0, by decide⟩ * BraidsLinksMCG.sigma ⟨1, by decide⟩) ^ (6 * k)) := by sorry

end BurauFaithful

Source

Birman, J. S., *Braids, Links, and Mapping Class Groups*, Ann. of Math. Studies 82, 1974, Sec. 3.3, pp. 129-130 (Theorem 3.15, attributed to Magnus-Peluso 1969); Coxeter, H. S. M. and Moser, W. O. J., *Generators and Relations for Discrete Groups*, 4th ed., Sec. 7.2; Malcev, A. I., *On the faithful representation of infinite groups by matrices*, Mat. Sb. 8 (1940).

View graph