Commutator width

DefinitionProducts of at most \(n\) commutators (Kourovka 14.15)#✓fully proved

Let \(G\) be a group and \(n\) a natural number. An element \(z \in G\) is a product of at most \(n\) commutators when there are \(m \le n\) and elements \(x_1, y_1, \dots, x_m, y_m \in G\) with \(z = [x_1, y_1] \cdots [x_m, y_m]\), where \([x, y] = xyx^{-1}y^{-1}\); for \(m = 0\) the empty product is the identity.

def IsProductOfCommutators {G : Type*} [Group G] (n : ℕ) (z : G) : Prop :=
  ∃ l : List (G × G), l.length ≤ n ∧ (l.map fun p => p.1 * p.2 * p.1⁻¹ * p.2⁻¹).prod = z

Used by 1

Used byUnbounded commutator length in Aut(Fₙ) (Kourovka 14.15)

DefinitionUnbounded commutator length in Aut(Fₙ) (Kourovka 14.15)#✓fully proved

The proposition that for every \(n \ge 3\), writing \(F_n\) for the free group on \(n\) generators, and for every natural number \(k\), some element of the derived subgroup of \(\operatorname{Aut}(F_n)\) is not a product of at most \(k\) commutators \(xyx^{-1}y^{-1}\) of elements of \(\operatorname{Aut}(F_n)\). This is the answer \(k_n = \infty\) to Bardakov's question, which asks for the supremum \(k_n\) of the commutator lengths of the elements of the derived subgroup of \(\operatorname{Aut}(F_n)\).

def autFreeGroupCommutatorLengthUnbounded : Prop :=
  ∀ n : ℕ, 3 ≤ n → ∀ k : ℕ, ∃ z ∈ commutator (MulAut (FreeGroup (Fin n))),
    ¬ IsProductOfCommutators k z

Uses 1 · Used by 1

Statement usesProducts of at most \(n\) commutators (Kourovka 14.15)

Used byCommutator length in Aut(Fₙ) is unbounded

TheoremCommutator length in Aut(Fₙ) is unbounded#●ready to prove

Let \(n \ge 3\) and let \(F_n\) be the free group on \(n\) generators. For every natural number \(k\) there is an element of the derived subgroup of \(\operatorname{Aut}(F_n)\) that is not a product of at most \(k\) commutators \(xyx^{-1}y^{-1}\) with \(x, y \in \operatorname{Aut}(F_n)\). Equivalently, the supremum \(k_n\) of the commutator lengths of the elements of the derived subgroup of \(\operatorname{Aut}(F_n)\) is infinite.

This answers Kourovka Problem 14.15 (V. G. Bardakov): \(\operatorname{Aut}(F_n)\) is acylindrically hyperbolic (Genevois–Horbez), and acylindrically hyperbolic groups have infinite commutator width (Bestvina–Bromberg–Fujiwara).

public theorem_wanted autFreeGroupCommutatorLengthUnbounded_holds :
    autFreeGroupCommutatorLengthUnbounded

Sources

• E. I. Khukhro and V. D. Mazurov (eds.), Unsolved Problems in Group Theory: The Kourovka Notebook, 21st issue, arXiv:1401.0300v49 (2026), Problem 14.15 (V. G. Bardakov); resolution: A. Genevois and C. Horbez, J. Topology 14 (2021), 963-991 (Aut F_n is acylindrically hyperbolic); M. Bestvina, K. Bromberg and K. Fujiwara, Algebr. Geom. Topol. 19 (2019), 477-489 (acylindrically hyperbolic groups have infinite commutator width), the Kourovka Notebook (21st issue) marks 14.15 solved: k_n = ∞ for n ≥ 3.

Uses 1

Statement usesUnbounded commutator length in Aut(Fₙ) (Kourovka 14.15)

DefinitionProducts of a bounded number of commutators#✓fully proved

For a group \(G\), a natural number \(m\) and \(g \in G\), \(g\) is a product of at most \(m\) commutators when there are \(k \le m\) and \(a_1, b_1, \dots, a_k, b_k \in G\) with \(g = [a_1, b_1] \cdots [a_k, b_k]\), where \([a, b] = aba^{-1}b^{-1}\); for \(k = 0\) the empty product is the identity.

def IsProductOfCommutators {G : Type*} [Group G] (m : ℕ) (g : G) : Prop :=
  ∃ l : List (G × G), l.length ≤ m ∧ (l.map fun p => p.1 * p.2 * p.1⁻¹ * p.2⁻¹).prod = g

Used by 1

Used byCommutator width of the derived subgroup

DefinitionCommutator width of the derived subgroup#✓fully proved

For a group \(G\) with derived subgroup \(G'\), the commutator width \(w(G')\) is the least positive integer \(m\) such that every element of \(G'\) is a product of at most \(m\) commutators \(aba^{-1}b^{-1}\) with \(a, b \in G\); it is \(0\) when no such \(m\) exists.

noncomputable def commutatorWidth (G : Type*) [Group G] : ℕ :=
  sInf {m : ℕ | 0 < m ∧ ∀ g ∈ commutator G, IsProductOfCommutators m g}

Uses 1 · Used by 1

Statement usesProducts of a bounded number of commutators

Used byBardakov's commutator width ratio claim (Kourovka 16.8)

DefinitionBardakov's commutator width ratio claim (Kourovka 16.8)#✓fully proved

The proposition that for every finite non-abelian group \(G\) the commutator width \(w(G')\) of its derived subgroup \(G'\) satisfies \(w(G')/|G| \le 1/6\), and that for the symmetric group \(S_3\) equality holds: \(w(S_3')/|S_3| = 1/6\).

def maxCommutatorWidthRatioIsOneSixth : Prop :=
  (∀ (G : Type) [Group G] [Finite G], (∃ a b : G, a * b ≠ b * a) →
      (commutatorWidth G : ℚ) / Nat.card G ≤ 1 / 6) ∧
    (commutatorWidth (Equiv.Perm (Fin 3)) : ℚ) / Nat.card (Equiv.Perm (Fin 3)) = 1 / 6

Uses 1 · Used by 1

Statement usesCommutator width of the derived subgroup

Used byThe maximal commutator width ratio is one sixth

TheoremThe maximal commutator width ratio is one sixth#●ready to prove

For every finite non-abelian group \(G\), the commutator width \(w(G')\) of its derived subgroup satisfies \(w(G')/|G| \le 1/6\), and for the symmetric group \(S_3\) equality holds, \(w(S_3')/|S_3| = 1/6\); so Kourovka Problem 16.8 has a positive answer.

The Kourovka Archive answers 16.8 "Yes, it is", citing Bonner (2008) for the bound; \(S_3\) attains it because its derived subgroup \(A_3\) consists of commutators.

public theorem_wanted maxCommutatorWidthRatioIsOneSixth_holds : maxCommutatorWidthRatioIsOneSixth

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 16.8 (V. G. Bardakov); resolution: T. Bonner, J. Algebra 320 (2008), 3165-3171, Kourovka Archive, Problem 16.8 (Yes, it is).

Uses 1

Statement usesBardakov's commutator width ratio claim (Kourovka 16.8)

DefinitionProducts of at most \(n\) commutators#✓fully proved

An element \(z\) of a group \(G\) is a product of at most \(n\) commutators when \(z = [x_1, y_1] \cdots [x_k, y_k]\) for some \(k \le n\) and some \(x_1, y_1, \dots, x_k, y_k \in G\), where \([x, y] = x y x^{-1} y^{-1}\); for \(k = 0\) the product is the identity.

def IsProductOfCommutators {G : Type*} [Group G] (n : ℕ) (z : G) : Prop :=
  ∃ l : List (G × G), l.length ≤ n ∧ (l.map fun p => p.1 * p.2 * p.1⁻¹ * p.2⁻¹).prod = z

Used by 1

Used byUnbounded commutator length

DefinitionUnbounded commutator length#✓fully proved

A group \(G\) has unbounded commutator length when for every natural number \(n\) some element of the derived subgroup \([G, G]\) is not a product of at most \(n\) commutators \(x y x^{-1} y^{-1}\) with \(x, y \in G\).

def CommutatorLengthUnbounded (G : Type*) [Group G] : Prop :=
  ∀ n : ℕ, ∃ z ∈ commutator G, ¬ IsProductOfCommutators n z

Uses 1 · Used by 2

Statement usesProducts of at most \(n\) commutators

Used byKourovka Problem 14.13(b) (Bardakov) · Kourovka Problem 14.13(a) (Bardakov)

DefinitionKourovka Problem 14.13(a) (Bardakov)#✓fully proved

The statement that there is a simple group \(G\) such that for every natural number \(n\) some element of the derived subgroup \([G, G]\) is not a product of at most \(n\) commutators \(x y x^{-1} y^{-1}\) with \(x, y \in G\).

def simpleGroupUnboundedCommutatorLength : Prop :=
  ∃ (G : Type) (_ : Group G), IsSimpleGroup G ∧ CommutatorLengthUnbounded G

Uses 1 · Used by 1

Statement usesUnbounded commutator length

Used byA simple group with unbounded commutator length

DefinitionKourovka Problem 14.13(b) (Bardakov)#✓fully proved

The statement that there is a finitely presented simple group \(G\) such that for every natural number \(n\) some element of the derived subgroup \([G, G]\) is not a product of at most \(n\) commutators \(x y x^{-1} y^{-1}\) with \(x, y \in G\).

def finitelyPresentedSimpleGroupUnboundedCommutatorLength : Prop :=
  ∃ (G : Type) (_ : Group G), Group.IsFinitelyPresented G ∧ IsSimpleGroup G ∧
    CommutatorLengthUnbounded G

Uses 1 · Used by 1

Statement usesUnbounded commutator length

Used byA finitely presented simple group with unbounded commutator length

TheoremA simple group with unbounded commutator length#●ready to prove

There is a simple group \(G\) such that for every natural number \(n\) some element of the derived subgroup \([G, G]\) is not a product of at most \(n\) commutators \(x y x^{-1} y^{-1}\) with \(x, y \in G\). This answers Kourovka Problem 14.13(a) in the affirmative; the Kourovka Archive records examples constructed by Barge and Ghys, and finitely generated ones by Muranov.

public theorem_wanted simpleGroupUnboundedCommutatorLength_holds :
    simpleGroupUnboundedCommutatorLength

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 14.13 (V. G. Bardakov); resolution: (a) J. Barge and É. Ghys, Math. Ann. 294 (1992), 235-265, and A. Muranov, Int. J. Algebra Comput. 17 (2007), 607-659 (finitely generated examples); (b) P.-E. Caprace and K. Fujiwara, Geom. Funct. Anal. 19 (2010), 1296-1319, Kourovka Archive, Problem 14.13 (answers: a) constructed; b) Yes, there does).

Uses 1

Statement usesKourovka Problem 14.13(a) (Bardakov)

TheoremA finitely presented simple group with unbounded commutator length#●ready to prove

There is a finitely presented simple group \(G\) such that for every natural number \(n\) some element of the derived subgroup \([G, G]\) is not a product of at most \(n\) commutators \(x y x^{-1} y^{-1}\) with \(x, y \in G\). This answers Kourovka Problem 14.13(b) in the affirmative; the Kourovka Archive cites Caprace and Fujiwara.

public theorem_wanted finitelyPresentedSimpleGroupUnboundedCommutatorLength_holds :
    finitelyPresentedSimpleGroupUnboundedCommutatorLength

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 14.13 (V. G. Bardakov); resolution: (a) J. Barge and É. Ghys, Math. Ann. 294 (1992), 235-265, and A. Muranov, Int. J. Algebra Comput. 17 (2007), 607-659 (finitely generated examples); (b) P.-E. Caprace and K. Fujiwara, Geom. Funct. Anal. 19 (2010), 1296-1319, Kourovka Archive, Problem 14.13 (answers: a) constructed; b) Yes, there does).

Uses 1

Statement usesKourovka Problem 14.13(b) (Bardakov)

9 fully proved4 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.