Braid groups in automorphism groups of free groups

AbbreviationThe braid group \(B_4\)#✓fully proved

The braid group on four strands, given by Artin's presentation: the group generated by \(\sigma_1, \sigma_2, \sigma_3\) subject to the relations \(\sigma_1 \sigma_2 \sigma_1 = \sigma_2 \sigma_1 \sigma_2\), \(\sigma_2 \sigma_3 \sigma_2 = \sigma_3 \sigma_2 \sigma_3\) and \(\sigma_1 \sigma_3 = \sigma_3 \sigma_1\).

abbrev BraidGroupFour : Type :=
  PresentedGroup ({FreeGroup.of 0 * FreeGroup.of 1 * FreeGroup.of 0 *
      (FreeGroup.of 1 * FreeGroup.of 0 * FreeGroup.of 1)⁻¹,
    FreeGroup.of 1 * FreeGroup.of 2 * FreeGroup.of 1 *
      (FreeGroup.of 2 * FreeGroup.of 1 * FreeGroup.of 2)⁻¹,
    FreeGroup.of 0 * FreeGroup.of 2 * (FreeGroup.of 2 * FreeGroup.of 0)⁻¹} :
      Set (FreeGroup (Fin 3)))

Used by 1

Used byBardakov's question on embedding \(B_4\) in \(\operatorname{Aut}(F_2)\)

DefinitionBardakov's question on embedding \(B_4\) in \(\operatorname{Aut}(F_2)\)#✓fully proved

The statement that there is an injective group homomorphism from the braid group \(B_4\) on four strands to the automorphism group \(\operatorname{Aut}(F_2)\) of the free group \(F_2\) of rank \(2\). Kourovka Problem 17.14 (V. G. Bardakov) asks whether, for \(n \ge 4\), the braid group \(B_n\) embeds in the automorphism group of the free group \(F_{n-2}\) of rank \(n - 2\); this is the case \(n = 4\).

def braidGroupFourEmbedsInAutFreeGroupTwo : Prop :=
  ∃ f : BraidGroupFour →* MulAut (FreeGroup (Fin 2)), Function.Injective f

Uses 1 · Used by 1

Statement usesThe braid group \(B_4\)

Used byBardakov–Bellingeri: \(B_4\) does not embed in \(\operatorname{Aut}(F_2)\)

TheoremBardakov–Bellingeri: \(B_4\) does not embed in \(\operatorname{Aut}(F_2)\)#●ready to prove

There is no injective group homomorphism from the braid group \(B_4\) on four strands to the automorphism group \(\operatorname{Aut}(F_2)\) of the free group \(F_2\) of rank \(2\). Kourovka Problem 17.14 (V. G. Bardakov) asks whether, for \(n \ge 4\), the braid group \(B_n\) embeds in the automorphism group of the free group \(F_{n-2}\) of rank \(n - 2\); this answers the case \(n = 4\) negatively.

public theorem_wanted braidGroupFourEmbedsInAutFreeGroupTwo_refuted :
    ¬ braidGroupFourEmbedsInAutFreeGroupTwo

Sources

• E. I. Khukhro and V. D. Mazurov (eds.), Unsolved Problems in Group Theory: The Kourovka Notebook, 21st issue, arXiv:1401.0300v49 (2026), Archive of Solved Problems, Problem 17.14 (V. G. Bardakov); resolution: V. G. Bardakov and P. Bellingeri, in Knot theory and its applications (ICTS program KTH-2013, IISER Mohali), Contemp. Math. 670, Amer. Math. Soc., 2016, 285-298, Kourovka Archive, Problem 17.14 (No, it cannot for n = 4).

Uses 1

Statement usesBardakov's question on embedding \(B_4\) in \(\operatorname{Aut}(F_2)\)

2 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.