Prove2Me

Kernel of the reduced Burau specialization at t=−1t = -1 is the normal closure of the full twist squared

Open
BurauFaithful.reducedBurau_kernel_normalClosure

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

algebraic-topologybraid-groupsgroup-theory

The kernel of the reduced Burau specialization at t=−1t=-1 is the normal closure of the full twist squared.

Let φ:B3→SL(2,Z)\varphi : B_3 \to \mathrm{SL}(2,\mathbb{Z}) be the specialization at t=−1t=-1 of the reduced Burau representation of the three-strand braid group and let Δ4=(σ1σ2)6\Delta^4 = (\sigma_1\sigma_2)^6. The theorem states

φ(β)=1  ⟹  β∈⟨ ⁣⟨Δ4⟩ ⁣⟩,\varphi(\beta) = 1 \;\Longrightarrow\; \beta \in \langle\!\langle \Delta^4 \rangle\!\rangle,

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 quotient Q=B3/⟨ ⁣⟨Δ4⟩ ⁣⟩Q = B_3/\langle\!\langle\Delta^4\rangle\!\rangle is the amalgam C4∗C2C6C_4 *_{C_2} C_6 generated by the classes of σ02σ1\sigma_0^2\sigma_1 and σ0σ1\sigma_0\sigma_1, whose images A2BA^2B and ABAB generate SL(2,Z)\mathrm{SL}(2,\mathbb{Z}); since SL(2,Z)\mathrm{SL}(2,\mathbb{Z}) is finitely generated and residually finite, Malcev's theorem makes it Hopfian, so the induced surjection Q↠SL(2,Z)Q \twoheadrightarrow \mathrm{SL}(2,\mathbb{Z}) is an isomorphism. This is the substantive half of the description of the kernel; the passage from the normal closure to explicit powers uses that Δ4\Delta^4 is central.

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
theorem BurauFaithful.reducedBurau_kernel_normalClosure (β : BraidsLinksMCG.ArtinBraidGroup 3) : BurauFaithful.redHom3 β = 1 → β ∈ Subgroup.normalClosure ({(BraidsLinksMCG.sigma ⟨0, by decide⟩ * BraidsLinksMCG.sigma ⟨1, by decide⟩) ^ 6} : Set (BraidsLinksMCG.ArtinBraidGroup 3)) := by sorry
Source
Birman, J. S., *Braids, Links, and Mapping Class Groups*, Ann. of Math. Studies 82, 1974, Sec. 3.3, pp. 129-130; 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