Artin representation of the braid group is well-defined
ProvedBraidsLinksMCG.artin_representation_wellDefinedCorollary 1.8.3 (well-definedness part). Artin's assignment of an automorphism of the free group to each braid generator extends to a group homomorphism , where the generator acts by (1-14) of Birman p. 25: , , and otherwise. Two ingredients are needed: each such endomorphism is invertible (it is an automorphism), and the assignment respects the braid relations (1-1) and (1-2). The assertion is the existence of the homomorphism with those values on the generators.
Preamble
import Mathlib import Definitions.Def_BraidsLinksMCG_ArtinBraidGroup import Definitions.Def_BraidsLinksMCG_ArtinEndo
Formal statement
namespace BraidsLinksMCG
theorem artin_representation_wellDefined (n : ℕ) :
∃ xi : ArtinBraidGroup n →* MulAut (FreeGroup (Fin n)),
∀ i : Fin (n - 1), ∀ w : FreeGroup (Fin n), xi (sigma i) w = artinEndo n i w := by sorry
end BraidsLinksMCG