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
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\).
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
def IsRelativelyFree (G : Type*) [Group G] : Prop :=
∃ (ι : Type) (x : ι → G), Subgroup.closure (Set.range x) = ⊤ ∧
∀ y : ι → G, ∃ φ : G →* G, ∀ i, φ (x i) = y i
WantedExt/GroupTheory/HallVerbalFinitenessRelativelyFreeKourovka12Problem31Wanted.lean:41
def wordValues {n : ℕ} (v : FreeGroup (Fin n)) (G : Type*) [Group G] : Set G :=
Set.range fun g : Fin n → G => FreeGroup.lift g v
WantedExt/GroupTheory/HallVerbalFinitenessRelativelyFreeKourovka12Problem31Wanted.lean:46
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
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
WantedExt/GroupTheory/HallVerbalFinitenessRelativelyFreeKourovka12Problem31Wanted.lean:52
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
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.