Prove2Me

Theorem 1.9, sufficiency: an endomorphism satisfying (i) and (ii) is a braid automorphism

Open
BraidsLinksMCG.thm_1_9_sufficiency

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

algebraic-topologybraid-groupsgroup-theory

This is the substantive half of Theorem 1.9, Artin's algebraic characterization of the braid automorphisms.

Let Fn=⟨x1,…,xn⟩F_n = \langle x_1,\dots,x_n\rangle and let ξ:Bn→Aut⁡(Fn)\xi : B_n \to \operatorname{Aut}(F_n) be the Artin representation given on the generators by equation (1-14). Let β\beta be an endomorphism of FnF_n satisfying the two Artin conditions:

  1. there are a permutation μ\mu of {1,…,n}\{1,\dots,n\} and words A1,…,An∈FnA_1,\dots,A_n \in F_n with
β(xi)=Ai xμ(i) Ai−1(1≤i≤n);\beta(x_i) = A_i\, x_{\mu(i)}\, A_i^{-1} \qquad (1 \le i \le n);
  1. β\beta fixes the product of all the generators,
β(x1x2⋯xn)=x1x2⋯xn.\beta(x_1x_2\cdots x_n) = x_1x_2\cdots x_n .

Then β\beta is induced by a braid: there is β′∈Bn\beta' \in B_n with ξ(β′)=β\xi(\beta') = \beta as maps on FnF_n.

Together with the necessity of the two conditions this identifies the image of ξ\xi exactly, and hence describes the braid group as a concrete subgroup of Aut⁡(Fn)\operatorname{Aut}(F_n). It is the algebraic engine behind the treatment of the conjugacy problem and of the Magnus representations.

Formalization Note The representation ξ\xi is supplied as a hypothesis together with its values on the Artin generators, which determine it uniquely. The conclusion asserts the existence of a braid whose associated automorphism agrees with β\beta on every word; no injectivity is claimed here.

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

theorem thm_1_9_sufficiency (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)
    (beta : FreeGroup (Fin n) →* FreeGroup (Fin n))
    (hconj : ∃ mu : Equiv.Perm (Fin n), ∃ A : Fin n → FreeGroup (Fin n),
        ∀ i : Fin n, beta (FreeGroup.of i) = A i * FreeGroup.of (mu i) * (A i)⁻¹)
    (hword : beta (freeWordProd n) = freeWordProd n) :
    ∃ b : ArtinBraidGroup n, ∀ w : FreeGroup (Fin n), xi b w = beta w := 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, Theorem 1.9, p. 30 (Artin, 1925), sufficiency direction; equation (1-14), p. 25

View graph