Prove2Me

A braid automorphism sends xjx_j to a conjugate of xμ(j)x_{\mu(j)}

Proved
BraidsLinksMCG.artin_action_conj_perm

by Gabewhigham · Sep 14, 2026 · Mathlib 0df444a (Lean v4.33.1)

algebraic-topologybraid-groupsgroup-theory

This is the first of the two conditions in Artin's characterization of braid automorphisms.

Let Fn=⟨x1,…,xn⟩F_n = \langle x_1,\dots,x_n\rangle be the free group of rank nn, let ξ:Bn→Aut⁡(Fn)\xi : B_n \to \operatorname{Aut}(F_n) be the Artin representation, determined by its values on the generators by equation (1-14),

ξ(σi):xi↦xixi+1xi−1,xi+1↦xi,xk↦xk (k≠i,i+1),\xi(\sigma_i) : x_i \mapsto x_i x_{i+1} x_i^{-1}, \qquad x_{i+1} \mapsto x_i, \qquad x_k \mapsto x_k\ (k \neq i, i+1),

and let π:Bn→Σn\pi : B_n \to \Sigma_n be the homomorphism sending σi\sigma_i to the transposition (i,i+1)(i,i+1). Then for every braid β∈Bn\beta \in B_n and every index jj there is a word A∈FnA \in F_n with

ξ(β)(xj)=A xπ(β)(j) A−1.\xi(\beta)(x_j) = A\, x_{\pi(\beta)(j)}\, A^{-1}.

In words: a braid automorphism permutes the conjugacy classes of the free generators, and the induced permutation of the indices is exactly the underlying permutation of the braid. This is condition (i) of Theorem 1.9 (with μ=π(β)\mu = \pi(\beta)), and it is the statement that lets one read the strand permutation of a braid off its action on FnF_n; in particular a braid acting trivially on FnF_n must be a pure braid.

Formalization Note The representation ξ\xi and the permutation homomorphism π\pi are supplied as hypotheses together with their values on the Artin generators, which determine them uniquely. Free generators are indexed by Fin n\mathrm{Fin}\,n and braid generators by Fin(n−1)\mathrm{Fin}(n-1).

Preamble
import Definitions.Def_BraidsLinksMCG_ArtinBraidGroup
import Definitions.Def_BraidsLinksMCG_ArtinEndo
Formal statement
namespace BraidsLinksMCG

theorem artin_action_conj_perm (n : ℕ)
    (xi : ArtinBraidGroup n →* MulAut (FreeGroup (Fin n)))
    (hxi : ∀ i : Fin (n - 1), ∀ w : FreeGroup (Fin n), xi (sigma i) w = artinEndo n i w)
    (pi : ArtinBraidGroup n →* Equiv.Perm (Fin n))
    (hpi : ∀ i : Fin (n - 1), pi (sigma i) = Equiv.swap (strandIdx i) (strandIdxSucc i))
    (b : ArtinBraidGroup n) (j : Fin n) :
    ∃ A : FreeGroup (Fin n),
      xi b (FreeGroup.of j) = A * FreeGroup.of (pi b j) * A⁻¹ := by sorry

end BraidsLinksMCG
Source
Joan S. Birman, *Braids, Links, and Mapping Class Groups*, Annals of Mathematics Studies 82, Princeton University Press, 1974, Chapter 1, equation (1-14), p. 25, and Theorem 1.9, condition (i), p. 30

View graph