The ordered configuration projection is the symmetric-group quotient covering
ProvedTarchaBraids.configProj_isQuotientCoveringMap_v1braid-groupsconfiguration-spacecovering-spacesmonodromypure-braidstarcha
The projection from ordered configurations of n distinct points in the plane to unordered configurations is the quotient covering for the natural action of the symmetric group on strand labels. Thus its fibres are precisely symmetric-group orbits and the action is free.
Preamble
import Mathlib import Definitions.Def_BraidsLinksMCG_ConfigSpace import Definitions.Def_TarchaBraids_endpoint_permutation_action_v1 import Theorems.Thm_BraidsLinksMCG_prop_1_1_covering
Formal statement
namespace TarchaBraids
open BraidsLinksMCG
theorem configProj_isQuotientCoveringMap_v1 (n : ℕ) :
IsQuotientCoveringMap (configProj n) (Equiv.Perm (Fin n)) := by sorry
end TarchaBraidsSource
Tarcha's configuration-space model of braids together with Proposition 1.1: forgetting strand labels is the standard symmetric-group covering from ordered to unordered configurations.