Hall's verbal conjectures

DefinitionRelatively free group#✓fully proved

A group \(G\) is relatively free if it has a family \((x_i)_{i \in I}\) of elements that generates \(G\) such that for every family \((y_i)_{i \in I}\) of elements of \(G\) there is an endomorphism \(\varphi\) of \(G\) with \(\varphi(x_i) = y_i\) for all \(i \in I\).

Equivalently, \(G\) is free on \((x_i)\) in the variety of groups it generates.

def IsRelativelyFree (G : Type*) [Group G] : Prop :=
  ∃ (ι : Type) (x : ι → G), Subgroup.closure (Set.range x) = ⊤ ∧
    ∀ y : ι → G, ∃ φ : G →* G, ∀ i, φ (x i) = y i
Used by 1

DefinitionValues of a word#✓fully proved

For a word \(v\) in the free group on \(n\) generators and a group \(G\), the set of values of \(v\) on \(G\) is the set of elements \(v(g_1, \dots, g_n)\) obtained by substituting elements \(g_1, \dots, g_n \in G\) for the generators, that is, the set of images of \(v\) under all homomorphisms from that free group to \(G\).

def wordValues {n : ℕ} (v : FreeGroup (Fin n)) (G : Type*) [Group G] : Set G :=
  Set.range fun g : Fin n → G => FreeGroup.lift g v
Used by 1

DefinitionHall's verbal finiteness conjecture for relatively free groups (Kourovka 12.31)#✓fully proved

The statement that for every relatively free group \(G\), every \(n \in \mathbb{N}\) and every word \(v\) in the free group on \(n\) generators, if \(v\) takes only finitely many values on \(G\), then the verbal subgroup \(v(G)\) of \(G\) generated by these values is finite.

def relativelyFreeFiniteWordValuesFiniteVerbal : Prop :=
  ∀ (G : Type) [Group G], IsRelativelyFree G → ∀ (n : ℕ) (v : FreeGroup (Fin n)),
    (wordValues v G).Finite → (Subgroup.closure (wordValues v G) : Set G).Finite
Uses 2 · Used by 1

TheoremHall's conjecture fails for relatively free groups#●ready to prove

Hall's verbal finiteness conjecture for relatively free groups is false: there are a relatively free group \(G\), a natural number \(n\) and a word \(v\) in the free group on \(n\) generators such that \(v\) takes only finitely many values on \(G\) but the verbal subgroup \(v(G)\) of \(G\) generated by these values is infinite.

public theorem_wanted relativelyFreeFiniteWordValuesFiniteVerbal_refuted :
    ¬ relativelyFreeFiniteWordValuesFiniteVerbal
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 12.31 (S. V. Ivanov); resolution: A. Storozhev, Proc. Amer. Math. Soc. 124 (1996), no. 10, 2953-2954, Kourovka Archive, Problem 12.31: the conjecture is disproved.
Uses 1
3 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.