Normal closures in free groups

DefinitionShortest elements of normal closures in free groups (Kourovka 11.82, Remeslennikov)#✓fully proved

The statement that for every free group \(F\) and every \(r \ne 1\) in \(F\), if \(s\) is a nontrivial element of the normal closure \(R\) of \(r\) in \(F\) whose reduced word length is minimal among the nontrivial elements of \(R\), then \(s\) is conjugate to \(r\), to \(r^{-1}\), or, for some \(f \in F\), to \([r, f] = r^{-1} f^{-1} r f\) or to \([r^{-1}, f] = r f^{-1} r^{-1} f\).

def minimalNormalClosureElementConj : Prop :=
  ∀ (α : Type) [DecidableEq α] (r : FreeGroup α), r ≠ 1 →
    ∀ s ∈ Subgroup.normalClosure {r}, s ≠ 1 →
    (∀ t ∈ Subgroup.normalClosure {r}, t ≠ 1 → s.norm ≤ t.norm) →
    IsConj s r ∨ IsConj s r⁻¹ ∨
      ∃ f : FreeGroup α, IsConj s (r⁻¹ * f⁻¹ * r * f) ∨ IsConj s (r * f⁻¹ * r⁻¹ * f)

Used by 1

Used byNegative answer to Kourovka 11.82 on shortest elements of normal closures

TheoremNegative answer to Kourovka 11.82 on shortest elements of normal closures#●ready to prove

There are a free group \(F\), an element \(r \ne 1\) of \(F\), and a nontrivial element \(s\) of the normal closure \(R\) of \(r\) in \(F\) whose reduced word length is minimal among the nontrivial elements of \(R\), such that \(s\) is conjugate neither to \(r\) nor to \(r^{-1}\), nor, for any \(f \in F\), to \([r, f] = r^{-1} f^{-1} r f\) or to \([r^{-1}, f] = r f^{-1} r^{-1} f\).

The Kourovka Archive answers 11.82 "No, not always" (McCool).

public theorem_wanted minimalNormalClosureElementConj_refuted : ¬ minimalNormalClosureElementConj

def minimalNormalClosureElementConj : Prop :=
  ∀ (α : Type) [DecidableEq α] (r : FreeGroup α), r ≠ 1 →
    ∀ s ∈ Subgroup.normalClosure {r}, s ≠ 1 →
    (∀ t ∈ Subgroup.normalClosure {r}, t ≠ 1 → s.norm ≤ t.norm) →
    IsConj s r ∨ IsConj s r⁻¹ ∨
      ∃ f : FreeGroup α, IsConj s (r⁻¹ * f⁻¹ * r * f) ∨ IsConj s (r * f⁻¹ * r⁻¹ * f)

WantedExt/GroupTheory/NormalClosureMinimalElementKourovka11Problem82Wanted.lean:42

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 11.82 (V. N. Remeslennikov); resolution: J. McCool, Glasgow Math. J. 43, no. 1 (2001), 123-124, Kourovka Archive, Problem 11.82: "No, not always", https://arxiv.org/abs/1401.0300v49.

Uses 1

Statement usesShortest elements of normal closures in free groups (Kourovka 11.82, Remeslennikov)

1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.