Prove2Me

B3B_3 in the generators of its amalgam decomposition: s2=u3s^2=u^3

Proved
BurauFaithful.braid_three_amalgam_dictionary

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

amalgamated-productbraid-groupsmodular-group

The braid group B3B_3 in the generators of its amalgam decomposition B3=⟨x⟩∗⟨x2⟩⟨y⟩B_3=\langle x\rangle *_{\langle x^2\rangle}\langle y\rangle with x=σ1σ2σ1x=\sigma_1\sigma_2\sigma_1, y=σ1σ2y=\sigma_1\sigma_2.

Writing

u=σ1σ2,s=σ12σ2=σ1u,u = \sigma_1\sigma_2,\qquad s = \sigma_1^2\sigma_2 = \sigma_1 u,

the two Artin generators are recovered by pure group algebra,

σ1=s u−1,σ2=u s−1 u,\sigma_1 = s\,u^{-1},\qquad \sigma_2 = u\,s^{-1}\,u,

while the defining relation of the amalgam is the braid identity

s2=(σ12σ2)2=(σ1σ2)3=u3,s^2 = (\sigma_1^2\sigma_2)^2 = (\sigma_1\sigma_2)^3 = u^3,

which is Δ2\Delta^2, the full twist, and is proved here by a single use of σ1σ2σ1=σ2σ1σ2\sigma_1\sigma_2\sigma_1=\sigma_2\sigma_1\sigma_2.

Together with Δ4=(σ1σ2)6\Delta^4=(\sigma_1\sigma_2)^6 (the Garside identity BurauFaithful.braid_three_garside_pow) and the centrality of Δ2\Delta^2 (BurauFaithful.braid_three_fullTwist_central) this exhibits the quotient B3/⟨Δ4⟩B_3/\langle\Delta^4\rangle as the amalgam Z/4∗Z/2Z/6\mathbb Z/4 *_{\mathbb Z/2}\mathbb Z/6 generated by the images of ss and uu; the faithfulness theorem for three strands is then exactly the statement that this amalgam embeds into SL(2,Z)\mathrm{SL}(2,\mathbb Z) (Coxeter-Moser; Birman, Braids, Links, and Mapping Class Groups, Ann. of Math. Studies 82, §3.3, pp. 129-130).

Formalization Note The elements ss and uu are introduced as BurauFaithful.sLift and BurauFaithful.uLift in the preamble; the braid relation is extracted from the relator σ1σ2σ1(σ2σ1σ2)−1\sigma_1\sigma_2\sigma_1(\sigma_2\sigma_1\sigma_2)^{-1} of the presented group, and the four identities are then formal group algebra together with one rewrite by that relation.

Preamble
/-
`BurauFaithful.braid_three_amalgam_dictionary`: `B₃` in the generators of the amalgam
`B₃ = ⟨x⟩ *_{⟨x²⟩} ⟨y⟩` with `x = σ₀σ₁σ₀`, `y = σ₀σ₁`.

The two elements used by the amalgam decomposition of `B₃/⟨Δ⁴⟩` are

```
uLift := σ₀ · σ₁                -- image of U = S·T in SL(2,ℤ)
sLift := σ₀² · σ₁ = σ₀ · uLift   -- image of S      in SL(2,ℤ)
```

which formally satisfy `σ₀ = sLift · uLift⁻¹` and `σ₁ = uLift · sLift⁻¹ · uLift` (pure group
algebra, no braid relation), while the defining relation of the amalgam is the braid identity

```
sLift² = (σ₀²σ₁)² = (σ₀σ₁)³ = uLift³      (= Δ², the full twist),
```

verified by a single use of `σ₀σ₁σ₀ = σ₁σ₀σ₁`. In `B₃/⟨Δ⁴⟩` one also has `sLift⁴ = uLift⁶ = 1`
(Proved separately as the Garside identity and centrality of the full twist); hence `B₃/⟨Δ⁴⟩` is
the amalgam `ℤ/4 *_{ℤ/2} ℤ/6`, and `spec_reduced_kernel_le` is the statement that this amalgam
maps injectively into `SL(2,ℤ)` (Coxeter–Moser; Birman, *Braids, Links, and Mapping Class Groups*,
Ann. of Math. Studies 82, §3.3, pp. 129-130).
-/
import Definitions.Def_BurauFaithful_UnreducedBurau

set_option autoImplicit false

namespace BurauFaithful

/-- `σ₀²σ₁`, the braid mapping to the order-`4` element `S = !![0,-1;1,0]`. -/
noncomputable def sLift : PresentedGroup (BraidsLinksMCG.braidRels 3) :=
  PresentedGroup.of (rels := BraidsLinksMCG.braidRels 3) (0 : Fin 2) ^ 2 *
    PresentedGroup.of (rels := BraidsLinksMCG.braidRels 3) 1

/-- `σ₀σ₁`, the braid mapping to the order-`6` element `U = S·T = !![0,-1;1,1]`. -/
noncomputable def uLift : PresentedGroup (BraidsLinksMCG.braidRels 3) :=
  PresentedGroup.of (rels := BraidsLinksMCG.braidRels 3) (0 : Fin 2) *
    PresentedGroup.of (rels := BraidsLinksMCG.braidRels 3) 1

end BurauFaithful
Formal statement
theorem BurauFaithful.braid_three_amalgam_dictionary :
    ((PresentedGroup.of (rels := BraidsLinksMCG.braidRels 3) (0 : Fin 2) =
        BurauFaithful.sLift * BurauFaithful.uLift⁻¹) ∧
      (PresentedGroup.of (rels := BraidsLinksMCG.braidRels 3) (1 : Fin 2) =
        BurauFaithful.uLift * BurauFaithful.sLift⁻¹ * BurauFaithful.uLift) ∧
      (BurauFaithful.sLift ^ 2 = BurauFaithful.uLift ^ 3) ∧
      (BurauFaithful.sLift =
        PresentedGroup.of (rels := BraidsLinksMCG.braidRels 3) (0 : Fin 2) *
          BurauFaithful.uLift)) := by sorry
Source
J. S. Birman, *Braids, Links, and Mapping Class Groups*, Ann. of Math. Studies 82, Princeton Univ. Press, 1974, §3.3, pp. 129-130; C. Moser, H. S. M. Coxeter, *Generators and relations for discrete groups*, 2nd ed., Springer 1964, p. 85.

View graph