A geometric braid loop lifts to labelled strands with a permutation endpoint

Proved

TarchaBraids.braid_loop_ordered_lift_v1

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

braid-groupsconfiguration-spacecovering-spacespath-liftingtarcha

Every based loop in the unordered configuration space lifts, from the standard ordered base configuration, to a continuous path of labelled configurations. Because the original path is a loop, the lifted endpoint differs from the ordered base configuration only by a permutation of the strand labels.

Preamble

import Mathlib
import Definitions.Def_BraidsLinksMCG_ConfigSpace
import Theorems.Thm_BraidsLinksMCG_prop_1_1_covering

Formal statement

namespace TarchaBraids

open BraidsLinksMCG unitInterval

theorem braid_loop_ordered_lift_v1 (n : ℕ)
    (γ : Path (baseUnordered n) (baseUnordered n)) :
    ∃ Γ : C(I, OrderedConfig n),
      (configProj n : OrderedConfig n → UnorderedConfig n) ∘ Γ = γ ∧
      Γ 0 = baseOrdered n ∧
      ∃ g : Equiv.Perm (Fin n), (Γ 1).1 = (baseOrdered n).1 ∘ g := by sorry

end TarchaBraids

Source

Tarcha Teorema 3.11 and the standard covering-space model of braids: an unordered braid loop is represented by labelled strand paths whose endpoints are permuted.

View graph