Prove2Me

The deck-permutation kernel is the image of the pure braid group

Proved
TarchaBraids.deck_kernel_eq_pure_range_v1

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

braid-groupscovering-spaceskernelmonodromypure-braidstarcha

For the ordered-to-unordered configuration quotient covering, the kernel of the strand-permutation homomorphism is exactly the range of the fundamental-group map from the ordered configuration space, hence the image of the pure braid group.

Preamble
import Mathlib
import Definitions.Def_BraidsLinksMCG_ConfigSpace
import Definitions.Def_TarchaBraids_endpoint_permutation_action_v1
Formal statement
namespace TarchaBraids

open BraidsLinksMCG

theorem deck_kernel_eq_pure_range_v1 (n : ℕ)
    (hp : IsQuotientCoveringMap (configProj n) (Equiv.Perm (Fin n))) :
    (hp.fundamentalGroupToMulOpposite
      (⟨baseOrdered n, rfl⟩ : (configProj n) ⁻¹' {baseUnordered n})).ker =
    (FundamentalGroup.mapOfEq
      ⟨configProj n, hp.continuous⟩
      (show configProj n (baseOrdered n) = baseUnordered n from rfl)).range := by sorry

end TarchaBraids
Source
The standard covering-space exact sequence for ordered and unordered configuration spaces, specialised using Mathlib's quotient-covering monodromy kernel theorem.

View graph