Artin representation is injective (faithfulness)

Proved

BraidsLinksMCG.artin_representation_injective

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

Corollary 1.8.3 (faithfulness part). The Artin representation is injective: if a braid acts trivially on the free group $F_n$ , i.e. $\xi(\beta) = \operatorname{id}_{F_n}$ , then the braid $\beta$ is the identity. This is the faithfulness of the Artin representation, the algebraic content of Corollary 1.8.3 of Birman p. 25.

Preamble

import Mathlib
import Definitions.Def_BraidsLinksMCG_ArtinBraidGroup
import Definitions.Def_BraidsLinksMCG_ArtinEndo

Formal statement

namespace BraidsLinksMCG

theorem artin_representation_injective (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

View graph