Every geometric braid is a free word in the elementary half-twists
OpenTarchaBraids.halfTwist_free_lift_surjective_v1algebraic-topologybraid-groupsfree-groupsgenerationtarcha
Every geometric braid is represented by a finite word in the elementary half-twists and their inverses. Equivalently, the homomorphism from the free group on the Artin generator indices to the geometric braid group, sending each free generator to its explicit half-twist class, is surjective.
Preamble
import Mathlib import Definitions.Def_BraidsLinksMCG_ConfigSpace import Definitions.Def_TarchaBraids_HalfTwist
Formal statement
namespace TarchaBraids
open BraidsLinksMCG
theorem halfTwist_free_lift_surjective_v1 (n : ℕ) :
Function.Surjective
(FreeGroup.lift (fun i : Fin (n - 1) => halfTwistBraid n i)) := by sorry
end TarchaBraidsSource
Tarcha Teorema 3.11: partition a geometric braid into finitely many one-crossing slabs, each equivalent to an Artin generator or its inverse.