Equationally Noetherian groups

DefinitionEvaluation of an equation at an assignment (Kourovka 14.20)#✓fully proved

For a group \(G\), let \(F_n\) be the free group on the unknowns \(t_0, \dots, t_{n-1}\). For an assignment \(x = (x_0, \dots, x_{n-1}) \in G^n\), evaluation at \(x\) is the group homomorphism \(G * F_n \to G\) from the free product of \(G\) and \(F_n\) that is the identity on \(G\) and sends \(t_i\) to \(x_i\) for each \(i < n\); it sends an equation \(w \in G * F_n\) over \(G\) to its value \(w(x)\) at \(x\).

def evalEquation {G : Type*} [Group G] {n : ℕ} (x : Fin n → G) :
    Monoid.Coprod G (FreeGroup (Fin n)) →* G :=
  Monoid.Coprod.lift (MonoidHom.id G) (FreeGroup.lift x)

Used by 1

Used bySolution set of a system of equations (Kourovka 14.20)

DefinitionSolution set of a system of equations (Kourovka 14.20)#✓fully proved

For a group \(G\), let \(F_n\) be the free group on the unknowns \(t_0, \dots, t_{n-1}\). The solution set of a set \(S \subseteq G * F_n\) of equations over \(G\) is the set of assignments \(x = (x_0, \dots, x_{n-1}) \in G^n\) such that \(w(x) = 1\) for every \(w \in S\), where \(w(x)\) is the image of \(w\) under the homomorphism \(G * F_n \to G\) that is the identity on \(G\) and sends \(t_i\) to \(x_i\).

def solutions {G : Type*} [Group G] {n : ℕ} (S : Set (Monoid.Coprod G (FreeGroup (Fin n)))) :
    Set (Fin n → G) :=
  {x | ∀ w ∈ S, evalEquation x w = 1}

Uses 1 · Used by 1

Statement usesEvaluation of an equation at an assignment (Kourovka 14.20)

Used byEquationally Noetherian groups (Kourovka 14.20)

DefinitionEquationally Noetherian groups (Kourovka 14.20)#✓fully proved

A group \(G\) is equationally Noetherian (has the Noetherian Equation Property) if for every \(n \in \mathbb{N}\) and every set \(S\) of equations over \(G\) in the unknowns \(t_0, \dots, t_{n-1}\), that is, every subset \(S\) of the free product \(G * F_n\) of \(G\) with the free group \(F_n\) on \(t_0, \dots, t_{n-1}\), there is a finite subset \(S_0 \subseteq S\) with the same solution set as \(S\). Here the solution set of a set of equations is the set of assignments \(x = (x_0, \dots, x_{n-1}) \in G^n\) at which every equation in it evaluates to \(1\).

def EquationallyNoetherian (G : Type*) [Group G] : Prop :=
  ∀ (n : ℕ) (S : Set (Monoid.Coprod G (FreeGroup (Fin n)))),
    ∃ S₀ ⊆ S, S₀.Finite ∧ solutions S₀ = solutions S

Uses 1 · Used by 1

Statement usesSolution set of a system of equations (Kourovka 14.20)

Used byKourovka Problem 14.20 (free products of equationally Noetherian groups)

DefinitionKourovka Problem 14.20 (free products of equationally Noetherian groups)#✓fully proved

The statement that for all groups \(G\) and \(H\), if \(G\) and \(H\) are equationally Noetherian (have the Noetherian Equation Property), then their free product \(G * H\) is equationally Noetherian.

Kourovka Notebook Problem 14.20 is due to G. Baumslag, A. G. Myasnikov and V. N. Remeslennikov.

def freeProductEquationallyNoetherian : Prop :=
  ∀ (G H : Type) [Group G] [Group H], EquationallyNoetherian G → EquationallyNoetherian H →
    EquationallyNoetherian (Monoid.Coprod G H)

Uses 1 · Used by 1

Statement usesEquationally Noetherian groups (Kourovka 14.20)

Used byFree products of equationally Noetherian groups are equationally Noetherian

TheoremFree products of equationally Noetherian groups are equationally Noetherian#●ready to prove

Resolved true: the Kourovka Notebook (21st issue) answers 14.20 "Yes, it does", citing Sela's preprint (Theorem 9.1): the free product of two equationally Noetherian groups is equationally Noetherian. Source: E. I. Khukhro and V. D. Mazurov (eds.), Unsolved Problems in Group Theory: The Kourovka Notebook, 21st issue, arXiv:1401.0300v49 (2026), Problem 14.20 (G. Baumslag, A. G. Myasnikov, V. N. Remeslennikov); resolution: Z. Sela, Diophantine geometry over groups X: The elementary theory of free products of groups, preprint, arXiv:1012.0044 (2010), Section 9, Theorem 9.1: the free product of two equationally Noetherian groups is equationally Noetherian; the Kourovka Notebook (21st issue) marks 14.20 solved (Yes, it does), citing this preprint, https://arxiv.org/abs/1012.0044.

public theorem_wanted freeProductEquationallyNoetherian_holds : freeProductEquationallyNoetherian

Uses 1

Statement usesKourovka Problem 14.20 (free products of equationally Noetherian groups)

DefinitionEvaluating an equation at an assignment#✓fully proved

Let \(G\) be a group and \(n\) a natural number. An equation over \(G\) in the unknowns \(x_0, \dots, x_{n-1}\) is an element of the free product \(G * F(x_0, \dots, x_{n-1})\) of \(G\) with the free group on \(x_0, \dots, x_{n-1}\). For an assignment \(a = (a_0, \dots, a_{n-1}) \in G^n\), evaluation at \(a\) is the group homomorphism \(G * F(x_0, \dots, x_{n-1}) \to G\) that is the identity on \(G\) and sends each unknown \(x_i\) to \(a_i\).

def evalEquation {G : Type*} [Group G] {n : ℕ} (x : Fin n → G) :
    Monoid.Coprod G (FreeGroup (Fin n)) →* G :=
  Monoid.Coprod.lift (MonoidHom.id G) (FreeGroup.lift x)

Used by 1

Used bySolution set of a system of equations

DefinitionSolution set of a system of equations#✓fully proved

Let \(G\) be a group, \(n\) a natural number and \(S\) a set of equations over \(G\) in the unknowns \(x_0, \dots, x_{n-1}\), that is, a subset of the free product \(G * F(x_0, \dots, x_{n-1})\) of \(G\) with the free group on \(x_0, \dots, x_{n-1}\). The solution set of \(S\) is the set of assignments \(a \in G^n\) at which every \(w \in S\) evaluates to \(1\).

def solutions {G : Type*} [Group G] {n : ℕ} (S : Set (Monoid.Coprod G (FreeGroup (Fin n)))) :
    Set (Fin n → G) :=
  {x | ∀ w ∈ S, evalEquation x w = 1}

Uses 1 · Used by 1

Statement usesEvaluating an equation at an assignment

Used byThe Noetherian Equation Property

DefinitionThe Noetherian Equation Property#✓fully proved

A group \(G\) has the Noetherian Equation Property (is equationally Noetherian) if for every natural number \(n\) and every system \(S\) of equations over \(G\) in the unknowns \(x_0, \dots, x_{n-1}\), that is, every subset \(S\) of the free product \(G * F(x_0, \dots, x_{n-1})\) of \(G\) with the free group on \(x_0, \dots, x_{n-1}\), there is a finite subset \(S_0 \subseteq S\) whose solution set in \(G^n\) equals the solution set of \(S\).

def EquationallyNoetherian (G : Type*) [Group G] : Prop :=
  ∀ (n : ℕ) (S : Set (Monoid.Coprod G (FreeGroup (Fin n)))),
    ∃ S₀ ⊆ S, S₀.Finite ∧ solutions S₀ = solutions S

Uses 1 · Used by 1

Statement usesSolution set of a system of equations

Used byKourovka Problem 14.19 (hyperbolic groups and the Noetherian Equation Property)

DefinitionKourovka Problem 14.19 (hyperbolic groups and the Noetherian Equation Property)#✓fully proved

Every word-hyperbolic group \(G\) has the Noetherian Equation Property: for every natural number \(n\), every system of equations over \(G\) in the unknowns \(x_0, \dots, x_{n-1}\) has the same solution set in \(G^n\) as some finite subsystem.

The problem is due to G. Baumslag, A. G. Myasnikov and V. N. Remeslennikov.

def hyperbolicGroupEquationallyNoetherian : Prop :=
  ∀ (G : Type) [Group G], Group.IsHyperbolic G → EquationallyNoetherian G

Uses 2 · Used by 1

Statement usesWord-hyperbolic groups · The Noetherian Equation Property

Used byHyperbolic groups are equationally Noetherian

TheoremHyperbolic groups are equationally Noetherian#●ready to prove

Every word-hyperbolic group \(G\) has the Noetherian Equation Property: for every natural number \(n\), every system of equations over \(G\) in the unknowns \(x_0, \dots, x_{n-1}\) has the same solution set in \(G^n\) as some finite subsystem.

This answers Kourovka Problem 14.19 ("Yes, it does"): Weidmann and Reinfeldt prove it for all hyperbolic groups, and Sela had proved the torsion-free case.

public theorem_wanted hyperbolicGroupEquationallyNoetherian_holds :
    hyperbolicGroupEquationallyNoetherian

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.19 (G. Baumslag, A. G. Myasnikov, V. N. Remeslennikov); resolution: R. Weidmann and C. Reinfeldt, Ann. Math. Blaise Pascal 26 (2019), no. 2, 125-214, the Kourovka Notebook (21st issue) marks 14.19 solved (Yes); the torsion-free case is due to Z. Sela, Proc. London Math. Soc. 99 (2009), 217-273.

Uses 1

Statement usesKourovka Problem 14.19 (hyperbolic groups and the Noetherian Equation Property)

8 fully proved2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.