Adjacent transpositions give a surjective free-group lift to the symmetric group

Proved

TarchaBraids.adjacent_swap_free_lift_surjective_v1

by WillR · Sep 21, 2026 · Mathlib 0df444a (Lean v4.33.1)

adjacent-transpositionsbraid-groupsfree-groupspermutationstarcha

For m + 1 labelled strands, every endpoint permutation is represented by a signed word in the m adjacent transpositions. Equivalently, the free-group homomorphism sending generator i to the adjacent swap of i and i+1 is surjective onto the full permutation group.

Preamble

import Mathlib

Formal statement

namespace TarchaBraids

theorem adjacent_swap_free_lift_surjective_v1 (m : ℕ) :
    Function.Surjective
      (FreeGroup.lift
        (fun i : Fin m =>
          (Equiv.swap i.castSucc i.succ : Equiv.Perm (Fin (m + 1))))) := by sorry

end TarchaBraids

Source

Tarcha Teorema 3.11 endpoint-permutation correction, together with the standard fact that adjacent transpositions generate the finite symmetric group.

View graph