The square of the lifted S-generator is central

Proved

burau_liftS_sq_central

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

braid-groupscentralitycoxeter

Centrality of $\mathrm{liftS}^2$ . In the reduced braid group $Q=B_3/\langle\!\langle\Delta^4\rangle\!\rangle$ the element $\mathrm{liftS}^2$ is central:

\mathrm{liftS}^2 \in Z(Q).

Its preimage is the square of the Garside element of $B_3$ , which is central there because it equals $(\sigma_0\sigma_1)^3$ ; centrality descends through the quotient map. This is what lets the conjugating moves in the Coxeter relation be performed inside a single flat product.

Preamble

import Definitions.Def_burau_reduced_braid_group
import Definitions.Def_BurauFaithful_UnreducedBurau
import Theorems.Thm_BurauFaithful_braid_three_amalgam_dictionary
import Theorems.Thm_BurauFaithful_braid_three_fullTwist_central

set_option autoImplicit false

Formal statement

theorem burau_liftS_sq_central :
    BurauNC.liftS ^ 2 ∈ Subgroup.center BurauNC.Q := by sorry

Source

C. Moser, H. S. M. Coxeter, *Generators and relations for discrete groups* (1964), Ch. 3.

View graph