Prove2Me

An elementary half-twist has the adjacent strand permutation

Open
TarchaBraids.halfTwist_deck_permutation_v1

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

braid-groupscovering-spaceshalf-twistsmonodromypermutationstarcha

For the symmetric-group quotient covering from ordered to unordered configurations, the explicit geometric half-twist on adjacent strands has deck permutation equal to the corresponding adjacent transposition.

Preamble
import Mathlib
import Definitions.Def_BraidsLinksMCG_ConfigSpace
import Definitions.Def_TarchaBraids_HalfTwist
import Definitions.Def_TarchaBraids_endpoint_permutation_action_v1
import Theorems.Thm_TarchaBraids_configProj_isQuotientCoveringMap_v1
Formal statement
namespace TarchaBraids

open BraidsLinksMCG

theorem halfTwist_deck_permutation_v1 (n : ℕ) (i : Fin (n - 1)) :
    (configProj_isQuotientCoveringMap_v1 n).fundamentalGroupToMulOpposite
      (⟨baseOrdered n, rfl⟩ : (configProj n) ⁻¹' {baseUnordered n})
      (halfTwistBraid n i) =
    MulOpposite.op (Equiv.swap (strandIdx i) (strandIdxSucc i)) := by sorry

end TarchaBraids
Source
Tarcha Teorema 3.11 and the explicit half-twist construction: the elementary braid generator interchanges exactly the two adjacent strand endpoints.

View graph