Every braid can be corrected by a half-twist word into the pure kernel

Proved

TarchaBraids.permutation_correction_to_kernel_v1

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

braid-groupsfree-groupshalf-twistskernelpermutationstarcha

If the quotient-covering deck homomorphism sends each explicit adjacent half-twist to its adjacent transposition and adjacent transpositions are generated by the free lift, then every geometric braid differs from a half-twist word by an element of the deck-permutation kernel.

Preamble

import Mathlib
import Definitions.Def_BraidsLinksMCG_ConfigSpace
import Definitions.Def_TarchaBraids_HalfTwist
import Definitions.Def_TarchaBraids_endpoint_permutation_action_v1

Formal statement

namespace TarchaBraids

open BraidsLinksMCG

theorem permutation_correction_to_kernel_v1 (n : ℕ)
    (hp : IsQuotientCoveringMap (configProj n) (Equiv.Perm (Fin n)))
    (hgen : ∀ i : Fin (n - 1),
      hp.fundamentalGroupToMulOpposite
        (⟨baseOrdered n, rfl⟩ : (configProj n) ⁻¹' {baseUnordered n})
        (halfTwistBraid n i) =
      MulOpposite.op (Equiv.swap (strandIdx i) (strandIdxSucc i)))
    (hswap : Function.Surjective
      (FreeGroup.lift (fun i : Fin (n - 1) =>
        Equiv.swap (strandIdx i) (strandIdxSucc i))))
    (β : GeomBraidGroup n) :
    ∃ w : FreeGroup (Fin (n - 1)),
      β * (FreeGroup.lift (fun i : Fin (n - 1) => halfTwistBraid n i) w)⁻¹ ∈
        (hp.fundamentalGroupToMulOpposite
          (⟨baseOrdered n, rfl⟩ : (configProj n) ⁻¹' {baseUnordered n})).ker := by sorry

end TarchaBraids

Source

Algebraic permutation-correction step in Tarcha Teorema 3.11: first match the strand permutation by a word in adjacent half-twists, leaving a pure braid.

View graph