Equations over free groups

DefinitionKourovka Problem 14.48 (equations over free groups in finite quotients)#✓fully proved

The statement that for every free group \(F\) on an arbitrary set of generators, every natural number \(n\) and every equation \(w\) over \(F\) in the unknowns \(x_0, \dots, x_{n-1}\) (an element of the free product of \(F\) with the free group on \(x_0, \dots, x_{n-1}\)): if no \(g_0, \dots, g_{n-1} \in F\) are such that substituting \(g_i\) for \(x_i\) sends \(w\) to \(1\), then there is a normal subgroup \(N\) of finite index in \(F\) such that no \(h_0, \dots, h_{n-1} \in F / N\) are such that substituting \(h_i\) for \(x_i\) and mapping the coefficients of \(w\) to their images in \(F / N\) sends \(w\) to \(1\).

def unsolvableEquationUnsolvableInFiniteQuotient : Prop :=
  ∀ (α : Type) (n : ℕ) (w : Monoid.Coprod (FreeGroup α) (FreeGroup (Fin n))),
    (∀ x : Fin n → FreeGroup α, Monoid.Coprod.lift (MonoidHom.id _) (FreeGroup.lift x) w ≠ 1) →
    ∃ (N : Subgroup (FreeGroup α)) (_ : N.Normal), N.FiniteIndex ∧
      ∀ x : Fin n → FreeGroup α ⧸ N,
        Monoid.Coprod.lift (QuotientGroup.mk' N) (FreeGroup.lift x) w ≠ 1
Used by 1

TheoremAn unsolvable equation over a free group that is solvable in every finite quotient#●ready to prove

There are a free group \(F\) on some set of generators, a natural number \(n\) and an equation \(w\) over \(F\) in the unknowns \(x_0, \dots, x_{n-1}\), that is, an element \(w\) of the free product of \(F\) with the free group on \(x_0, \dots, x_{n-1}\), such that no \(g_0, \dots, g_{n-1} \in F\) satisfy the equation (substituting \(g_i\) for \(x_i\) never sends \(w\) to \(1\)), but for every normal subgroup \(N\) of finite index in \(F\) there are \(h_0, \dots, h_{n-1} \in F / N\) such that substituting \(h_i\) for \(x_i\) and mapping the coefficients of \(w\) to their images in \(F / N\) sends \(w\) to \(1\).

Resolved false: the Kourovka Archive answers 14.48 "No, not always", citing Coulbois and Khelif: some equation over a free group has no solution in it but has a solution in every finite quotient.

public theorem_wanted unsolvableEquationUnsolvableInFiniteQuotient_refuted :
    ¬ unsolvableEquationUnsolvableInFiniteQuotient
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.48 (L. Comerford); resolution: T. Coulbois and A. Khelif, Proc. Amer. Math. Soc. 127 (1999), no. 4, 963-965, Kourovka Archive, Problem 14.48 (answer: No, not always).
Uses 1
1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.