Groups with unique ordered-product normal forms

DefinitionPolycyclic groups (Kourovka Problem 13.11)#✓fully proved

A group \(G\) is polycyclic if it has a finite series of subgroups \(1 = H_0 \le H_1 \le \cdots \le H_n = G\) in which each \(H_i\) is normal in \(H_{i+1}\) and each quotient \(H_{i+1} / H_i\) is cyclic.

def IsPolycyclic (G : Type*) [Group G] : Prop :=
  ∃ (n : ℕ) (H : Fin (n + 1) → Subgroup G), H 0 = ⊥ ∧ H (Fin.last n) = ⊤ ∧
    ∀ i : Fin n, H i.castSucc ≤ H i.succ ∧
      ∃ _ : ((H i.castSucc).subgroupOf (H i.succ)).Normal,
        IsCyclic (H i.succ ⧸ (H i.castSucc).subgroupOf (H i.succ))

Used by 1

Used byAlmost polycyclic groups (Kourovka Problem 13.11)

DefinitionAlmost polycyclic groups (Kourovka Problem 13.11)#✓fully proved

A group \(G\) is almost polycyclic, or virtually polycyclic, if some subgroup of finite index in \(G\) is polycyclic.

def IsAlmostPolycyclic (G : Type*) [Group G] : Prop :=
  ∃ H : Subgroup G, H.FiniteIndex ∧ IsPolycyclic H

Uses 1 · Used by 1

Statement usesPolycyclic groups (Kourovka Problem 13.11)

Used byKourovka Problem 13.11 (torsion-free groups with a unique product presentation)

DefinitionGroups with a unique product presentation#✓fully proved

A group \(G\) has a unique product presentation if there are \(n \in \mathbb{N}\) and elements \(a_0, \dots, a_{n-1} \in G\) such that every element of \(G\) equals \(a_0^{k_0} a_1^{k_1} \cdots a_{n-1}^{k_{n-1}}\) for exactly one tuple \((k_0, \dots, k_{n-1}) \in \mathbb{Z}^n\).

def HasUniqueProductPresentation (G : Type*) [Group G] : Prop :=
  ∃ (n : ℕ) (a : Fin n → G),
    Function.Bijective fun k : Fin n → ℤ => (List.ofFn fun i => a i ^ k i).prod

Used by 1

Used byKourovka Problem 13.11 (torsion-free groups with a unique product presentation)

DefinitionKourovka Problem 13.11 (torsion-free groups with a unique product presentation)#✓fully proved

The statement, asked by V. V. Bludov, that every group \(G\) which is torsion-free (no element of \(G\) other than \(1\) has finite order) and has a unique product presentation is almost polycyclic.

def torsionFreeUniqueProductAlmostPolycyclic : Prop :=
  ∀ (G : Type) [Group G], (∀ g : G, g ≠ 1 → ¬ IsOfFinOrder g) →
    HasUniqueProductPresentation G → IsAlmostPolycyclic G

Uses 2 · Used by 1

Statement usesGroups with a unique product presentation · Almost polycyclic groups (Kourovka Problem 13.11)

Used byA torsion-free group with a unique product presentation need not be almost polycyclic

TheoremA torsion-free group with a unique product presentation need not be almost polycyclic#●ready to prove

Not every torsion-free group with a unique product presentation is almost polycyclic: there is a group \(G\) in which no element other than \(1\) has finite order, which has a unique product presentation, and which is not almost polycyclic.

Muranov's theorem gives such a group with \(n\) generators for every \(n \ge 63\).

public theorem_wanted torsionFreeUniqueProductAlmostPolycyclic_refuted :
    ¬ torsionFreeUniqueProductAlmostPolycyclic

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 13.11 (V. V. Bludov); resolution: A. Muranov, On torsion-free groups with finite regular file bases, Trans. Amer. Math. Soc. 359 (2007), 3609-3645, Theorem (Section 1, proved at the end of Section 5), https://doi.org/10.1090/S0002-9947-07-04256-0.

Uses 1

Statement usesKourovka Problem 13.11 (torsion-free groups with a unique product presentation)

4 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.