Prove2Me

Corollary 1.8.3: BnB_n acts faithfully on the free group FnF_n

Proved
BraidsLinksMCG.cor_1_8_3_artin_representation_faithful

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

braid-groupsfree-groupsgroup-theoryrepresentation

Corollary 1.8.3 (Artin's representation). The braid group BnB_n has a faithful representation as a group of automorphisms of a free group Fn=⟨x1,…,xn⟩F_n = \langle x_1, \dots, x_n\rangle of rank nn, induced by the assignment (1-14)

σi:xi↦xixi+1xi−1,xi+1↦xi,xj↦xj(j≠i,i+1).\sigma_i : \quad x_i \mapsto x_i x_{i+1} x_i^{-1}, \qquad x_{i+1} \mapsto x_i, \qquad x_j \mapsto x_j \quad (j \neq i, i+1).

Formally: there is a group homomorphism ξ\xi from BnB_n to the automorphism group of FnF_n whose value at each generator σi\sigma_i acts on FnF_n exactly as the endomorphism (1-14), and ξ\xi is injective. The first half is the well-definedness of ξ\xi — the braid relations must be respected — and the second half is faithfulness, so that a braid is completely determined by the automorphism it induces.

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

theorem cor_1_8_3_artin_representation_faithful (n : ℕ) :
    ∃ xi : ArtinBraidGroup n →* MulAut (FreeGroup (Fin n)),
      (∀ i : Fin (n - 1), ∀ w : FreeGroup (Fin n), xi (sigma i) w = artinEndo n i w) ∧
        Function.Injective xi := 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. 25, Corollary 1.8.3 with equation (1-14)
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≥0n \ge 0. Let FnF_n be the free group on generators x0,…,xn−1x_0, \dots, x_{n-1}, let Aut(Fn)\mathrm{Aut}(F_n) be its group of group automorphisms, and let BnB_n be the presented group with generators σi\sigma_i, i∈{0,…,n−2}i \in \{0,\dots,n-2\}, and the braid relations.

The statement asserts: there exists a group homomorphism

ξ:Bn⟶Aut(Fn)\xi : B_n \longrightarrow \mathrm{Aut}(F_n)

with the following two properties.

(a) Prescribed values on the generators. For every braid index ii and every element w∈Fnw \in F_n,

ξ(σi)(w)  =  αi(w),\xi(\sigma_i)(w) \;=\; \alpha_i(w),

where αi\alpha_i is the endomorphism of FnF_n determined by

xi↦xixi+1xi−1,xi+1↦xi,xj↦xj (j≠i,i+1).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).

So the automorphism ξ(σi)\xi(\sigma_i) agrees, as a function on FnF_n, with that endomorphism; in particular the endomorphism is thereby bijective.

(b) Faithfulness. ξ\xi is injective as a function: distinct elements of BnB_n give distinct automorphisms of FnF_n.

Exact logical strength. The existence of ξ\xi carries the well-definedness of the assignment (that the braid relations are preserved). Injectivity is asserted for ξ\xi itself, so BnB_n embeds in Aut(Fn)\mathrm{Aut}(F_n); no description of the image is claimed. Which composition convention the automorphism group uses is not visible in the statement, since only the values on generators and injectivity are constrained; existence is asserted for some homomorphism with these properties, so the reader should not assume the map is canonical or unique — though (a) determines it on generators and hence on all of BnB_n.

Degenerate cases. For n≤1n \le 1 there are no braid generators, BnB_n is trivial, condition (a) is vacuous, and injectivity holds automatically; those values of nn are included in the quantifier.

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