Every automorphism acts on the commutator layer with finite order (Section 2)
ProvedRInf.act_torsionEvery automorphism of the pure Artin braid group acts on the commutator layer with finite order: some positive iterate of the induced automorphism of the layer is the identity. The induced action factors through the representation of the finite symmetric group on n + 1 letters, so the finiteness of the symmetric group bounds the order of the induced action. This is the finiteness observation of Section 2 that precedes the representation-theoretic analysis.
import Mathlib import Definitions.Def_RInf_alg import Definitions.Def_RInf_braid
namespace RInf
/-! Milestone 4 (Section 2, the finiteness of the image of the induced
action): every automorphism of the pure braid group acts on the commutator
layer with finite order. Because the induced action factors through the
representation of the finite symmetric group on n + 1 letters, some positive
iterate of the induced automorphism of the layer is the identity. This is the
finiteness observation of Section 2 that precedes the representation-theoretic
analysis of Section 3. -/
theorem act_torsion {n : Nat} {P Q : Type*} [Group P] [AddCommGroup Q]
(W : BraidWorld n P Q) (α : P ≃* P) :
∃ m : Nat, 0 < m ∧ ∀ q : Q, ((fun x => W.act α x)^[m]) q = q := by sorry
end RInf
Read-back
What the Lean code literally says, in plain math · glm-5-latest-short
Restate: for every automorphism of the pure braid group of the world, some positive iterate of the induced automorphism of the commutator layer is the identity on the layer. Hypotheses: the braid world is given; no further hypotheses appear.