Theorem 1.9 (Artin, 1925): which endomorphisms of $F_n$ are braid automorphisms

Proved

BraidsLinksMCG.thm_1_9_artin_characterization

by Lucas · Sep 13, 2026 · Mathlib 0df444a (Lean v4.33.1)

braid-groupsfree-groupsgroup-theory

Theorem 1.9 (Artin, 1925). Let $F_n = \langle x_1, \dots, x_n \rangle$ be free of rank $n$ and let $\beta$ be an endomorphism of $F_n$ . Then $\beta$ belongs to $B_n \subset \mathrm{Aut}\,F_n$ — that is, $\beta$ is the automorphism induced by some braid under the Artin representation — if and only if

(x_i)\beta = A_i\, x_{\mu_i}\, A_i^{-1} \quad (1 \le i \le n), \qquad (x_1x_2\cdots x_n)\beta = x_1x_2\cdots x_n,

where $(\mu_1, \dots, \mu_n)$ is a permutation of $(1, \dots, n)$ and each $A_i$ is a word in the generators. In words: an endomorphism is a braid automorphism exactly when it permutes the generators up to conjugacy and fixes the product $x_1x_2\cdots x_n$ .

The representation $\xi$ is taken as a hypothesis: the statement is made for any homomorphism from $B_n$ to $\mathrm{Aut}\,F_n$ whose value on each $\sigma_i$ is the endomorphism (1-14). Corollary 1.8.3 guarantees that at least one such $\xi$ exists, so the statement is not vacuous.

Preamble

import Mathlib
import Definitions.Def_BraidsLinksMCG_ArtinBraidGroup
import Definitions.Def_BraidsLinksMCG_ArtinEndo

Formal statement

namespace BraidsLinksMCG

theorem thm_1_9_artin_characterization (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)) :
    (∃ b : ArtinBraidGroup n, ∀ w : FreeGroup (Fin n), xi b w = beta w) ↔
      ((∃ 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)⁻¹) ∧
        beta (freeWordProd n) = freeWordProd n) := 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, p. 30, Theorem 1.9 [Artin, 1925], conditions (1-22) and (1-23)

Read-back

What the Lean code literally says, in plain math · self-authored-by-drafting-agent (non-blind)

Provenance: non-blind read-back. This read-back was written by the same agent that drafted the Lean statements in this proposal, not by an independent auditor with a fresh context. It is therefore not independent testimony and must not be treated as such: it cannot be relied on to catch an unfaithful formalization, because any misunderstanding in the draft is reproduced here. Please audit the Lean text directly, or obtain a genuinely blind read-back, before confirming the item.

Fix a natural number $n \ge 0$ , let $F_n$ be the free group on $x_0, \dots, x_{n-1}$ , and let $B_n$ be the presented group with generators $\sigma_i$ and the braid relations.

Hypotheses. The statement is made for a given group homomorphism $\xi : B_n \to \mathrm{Aut}(F_n)$ that satisfies, for every braid index $i$ and every $w \in F_n$ , $\xi(\sigma_i)(w) = \alpha_i(w)$ , where $\alpha_i$ is Artin's endomorphism

x_i \mapsto x_i x_{i+1} x_i^{-1}, \qquad x_{i+1} \mapsto x_i, \qquad x_j \mapsto x_j \ (j \neq i, i+1);

and for a given group endomorphism $\beta : F_n \to F_n$ (a homomorphism, not assumed bijective).

Conclusion. The following two statements are equivalent.

Left side. There exists $b \in B_n$ such that $\xi(b)$ and $\beta$ agree at every element of $F_n$ .

Right side. Both of the following hold:

there exist a permutation $\mu$ of $\{0, \dots, n-1\}$ and a family of words $A_0, \dots, A_{n-1} \in F_n$ such that for every $i$ ,

\beta(x_i) \;=\; A_i\, x_{\mu(i)}\, A_i^{-1};

$\beta$ fixes the ordered product of all generators:

\beta\bigl(x_0 x_1 \cdots x_{n-1}\bigr) \;=\; x_0 x_1 \cdots x_{n-1}.

Exact logical strength. The equivalence is stated for the given $\xi$ , which is a hypothesis of the statement rather than a constructed object: if no homomorphism with the displayed values on the generators existed, the statement would be vacuously true. The conjugators $A_i$ in (1) are arbitrary elements of $F_n$ and may depend on $i$ ; the permutation $\mu$ is arbitrary. Membership in the image of $\xi$ is expressed as pointwise agreement of functions on $F_n$ , not as equality of automorphisms in some quotient. No uniqueness of $b$ , $\mu$ or the $A_i$ is asserted.

Degenerate cases. $n \le 1$ is included: then $B_n$ is trivial and the equivalence reduces to a statement about the identity endomorphism of a free group of rank at most one.

Human review

Endorsed by Shuze Chen · Sep 13, 2026
Endorsed by Lucas · Sep 13, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Theorem 1.9 (Artin, 1925): which endomorphisms of FnF_nFn​ are braid automorphisms

Theorem 1.9 (Artin, 1925): which endomorphisms of $F_n$ are braid automorphisms