Torsion quotients of finitely presented groups

AbbreviationTorsion closure#✓fully proved

For a group \(G\), \(\mathrm{Tor}(G)\) is the normal closure in \(G\) of the set of elements of finite order of \(G\).

abbrev torsionClosure (G : Type*) [Group G] : Subgroup G :=
  Subgroup.normalClosure {g : G | IsOfFinOrder g}

Used by 1

Used byKourovka Problem 19.24 (torsion quotients of finitely presented groups)

DefinitionKourovka Problem 19.24 (torsion quotients of finitely presented groups)#✓fully proved

The statement, asked by M. Chiodo and R. Vyas, that there exists a finitely presented group \(G\) such that \(G / \mathrm{Tor}(G)\) is not finitely presented, where \(\mathrm{Tor}(G)\) is the normal closure of the set of elements of finite order of \(G\).

def existsFinitelyPresentedTorsionQuotientNotFinitelyPresented : Prop :=
  ∃ (G : Type) (_ : Group G), Group.IsFinitelyPresented G ∧
    ¬ Group.IsFinitelyPresented (G ⧸ torsionClosure G)

Uses 1 · Used by 1

Statement usesTorsion closure

Used byTorsion quotients of finitely presented groups need not be finitely presented

TheoremTorsion quotients of finitely presented groups need not be finitely presented#●ready to prove

There exists a finitely presented group \(G\) such that \(G / \mathrm{Tor}(G)\) is not finitely presented, where \(\mathrm{Tor}(G)\) is the normal closure of the set of elements of finite order of \(G\).

The Kourovka Archive answers Problem 19.24 "Yes, such groups exist": Leary and Minasyan (Constructions 3.1 and 3.2) give a soluble example and a virtually torsion-free example.

public theorem_wanted existsFinitelyPresentedTorsionQuotientNotFinitelyPresented_holds :
    existsFinitelyPresentedTorsionQuotientNotFinitelyPresented

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 19.24 (M. Chiodo, R. Vyas); resolution: I. J. Leary and A. Minasyan, A note on torsion length and torsion subgroups, J. Group Theory 26 (2023), no. 4, 741-750 (arXiv:2112.14546), Section 3, Construction 3.1 (Abels' finitely presented soluble group H modulo an infinite cyclic central subgroup C: G = H / C has G / Tor(G) ≅ H / Z(H), which is not finitely presented) and Construction 3.2 (a virtually torsion-free example built from Bestvina-Brady groups); Kourovka Archive, Problem 19.24: Yes, such groups exist, one soluble and one virtually torsion-free, https://arxiv.org/abs/2112.14546.

Uses 1

Statement usesKourovka Problem 19.24 (torsion quotients of finitely presented groups)

2 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.