Prove2Me

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

Open
BurauFaithful.reducedBurau_spec_kernel_power

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=−1t=-1.

Let ρ3red\rho_3^{\mathrm{red}} be the reduced Burau representation of the three-strand braid group B3B_3 and let φ\varphi be its specialization at t=−1t=-1, the homomorphism φ:B3→SL(2,Z)\varphi : B_3 \to \mathrm{SL}(2,\mathbb{Z}) sending the Artin generators to

σ1↦(1−101),σ2↦(2−110).\sigma_1 \mapsto \begin{pmatrix} 1 & -1 \\ 0 & 1 \end{pmatrix}, \qquad \sigma_2 \mapsto \begin{pmatrix} 2 & -1 \\ 1 & 0 \end{pmatrix}.

The theorem describes the kernel of φ\varphi: every braid annihilated by it is an integral power of the full twist squared,

φ(β)=1  ⟹  ∃ k∈Z,β=(σ1σ2)6k.\varphi(\beta) = 1 \;\Longrightarrow\; \exists\, k \in \mathbb{Z},\quad \beta = (\sigma_1\sigma_2)^{6k}.

Since Δ4=(σ1σ2)6\Delta^4 = (\sigma_1\sigma_2)^6 is central in B3B_3, this is equivalent to the statement that the kernel is the normal closure of Δ4\Delta^4, i.e. that φ\varphi induces an injection B3/⟨ ⁣⟨Δ4⟩ ⁣⟩↪SL(2,Z)B_3/\langle\!\langle\Delta^4\rangle\!\rangle \hookrightarrow \mathrm{SL}(2,\mathbb{Z}). The kernel consists of the powers of the full twist squared because the image of the full twist squared in SL(2,Z)\mathrm{SL}(2,\mathbb{Z}) has infinite order, and because the quotient B3/⟨ ⁣⟨Δ4⟩ ⁣⟩B_3/\langle\!\langle\Delta^4\rangle\!\rangle is the amalgam C4∗C2C6C_4 *_{C_2} C_6, which is SL(2,Z)\mathrm{SL}(2,\mathbb{Z}) itself: it is generated by σ0σ1\sigma_0\sigma_1 and σ02σ1\sigma_0^2\sigma_1, whose images generate SL(2,Z)\mathrm{SL}(2,\mathbb{Z}), and the group is finitely generated and residually finite, hence Hopfian by Malcev's theorem, so that the surjection onto the modular group is an isomorphism.

Formalization Note. This is the power form of the kernel used by the mission's assembly: it is stated with the explicit generators BraidsLinksMCG.sigma and the specialization BurauFaithful.redHom3 of the preamble.

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 (beta : BraidsLinksMCG.ArtinBraidGroup 3) : BurauFaithful.redHom3 beta = 1 -> (exists k : Int, beta = (BraidsLinksMCG.sigma (n := 3) (0 : Fin 2) * BraidsLinksMCG.sigma (n := 3) (1 : Fin 2)) ^ (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 (the presentation ⟨S,R∣S4=1,R3=S2⟩\langle S,R \mid S^4 = 1, R^3 = S^2\rangle of SL(2,Z)\mathrm{SL}(2,\mathbb{Z})); Malcev, A. I., *On the faithful representation of infinite groups by matrices*, Mat. Sb. 8 (1940) (finitely generated residually finite groups are Hopfian).

View graph