The Artin generator assignment extends to the geometric braid group

Proved

TarchaBraids.exists_halfTwist_hom_v1

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

artin-presentationbraid-groupspresented-groupstarcha

The explicit elementary half-twists satisfy Artin's defining relations, so the assignment sending each abstract generator to its geometric half-twist extends to a group homomorphism from the presented Artin braid group to the geometric braid group.

Preamble

import Mathlib
import Definitions.Def_BraidsLinksMCG_ArtinBraidGroup
import Definitions.Def_BraidsLinksMCG_ConfigSpace
import Definitions.Def_TarchaBraids_HalfTwist
import Theorems.Thm_TarchaBraids_thm_3_15_half_twists_satisfy_relations

Formal statement

namespace TarchaBraids

open BraidsLinksMCG

theorem exists_halfTwist_hom_v1 (n : ℕ) :
    ∃ f : ArtinBraidGroup n →* GeomBraidGroup n,
      ∀ i : Fin (n - 1), f (sigma i) = halfTwistBraid n i := by sorry

end TarchaBraids

Source

Algebraic extension step in Tarcha Teorema 3.15, isolated from the accepted root proof sketch after the relations milestone was proved.

View graph