Determinant of the degree-3 Burau representation is an integer power of det ρ₃(σ₁)

Proved

BurauFaithful.burauRep3_det_pow

by junyihjy · Sep 25, 2026 · Mathlib 0df444a (Lean v4.33.1)

For the unreduced Burau representation ρ₃ of the braid group B₃ over the Laurent polynomial ring ℤ[t,t⁻¹], the determinant of ρ₃(β), as a unit of ℤ[t,t⁻¹], is an integer power of the determinant of ρ₃(σ₁) (which equals the unit -t).

Preamble

import Definitions.Def_BraidsLinksMCG_ArtinBraidGroup
import Definitions.Def_BurauFaithful_UnreducedBurau

Formal statement

namespace BurauFaithful

theorem burauRep3_det_pow (β : BraidsLinksMCG.ArtinBraidGroup 3) :
    ∃ k : ℤ, Matrix.GeneralLinearGroup.det (BurauFaithful.burauRep 3 β) =
      (Matrix.GeneralLinearGroup.det (BurauFaithful.burauRep 3
        (BraidsLinksMCG.sigma ⟨0, by decide⟩))) ^ k := by sorry

end BurauFaithful

View graph