Elementary amenable groups

InductiveElementary amenable groups#✓fully proved

The class of elementary amenable groups is the smallest class of groups that contains every finite group and every abelian group and is closed under isomorphisms, subgroups, quotients, extensions and directed unions. Closure under extensions means that a group \(G\) with a normal subgroup \(N\) is elementary amenable whenever \(N\) and \(G/N\) are; closure under directed unions means that \(G\) is elementary amenable whenever it is the union of a family of elementary amenable subgroups that is directed under inclusion.

inductive IsElementaryAmenable : (G : Type) → [Group G] → Prop
  | of_finite (G : Type) [Group G] [Finite G] : IsElementaryAmenable G
  | of_comm (G : Type) [Group G] (h : ∀ a b : G, a * b = b * a) : IsElementaryAmenable G
  | of_mulEquiv {G H : Type} [Group G] [Group H] (e : G ≃* H) :
      IsElementaryAmenable G → IsElementaryAmenable H
  | subgroup {G : Type} [Group G] (K : Subgroup G) : IsElementaryAmenable G → IsElementaryAmenable K
  | quotient {G : Type} [Group G] (N : Subgroup G) [N.Normal] :
      IsElementaryAmenable G → IsElementaryAmenable (G ⧸ N)
  | extension {G : Type} [Group G] (N : Subgroup G) [N.Normal] :
      IsElementaryAmenable N → IsElementaryAmenable (G ⧸ N) → IsElementaryAmenable G
  | directedUnion {G : Type} [Group G] (S : Set (Subgroup G)) :
      DirectedOn (· ≤ ·) S → (∀ K ∈ S, IsElementaryAmenable K) → (∀ g : G, ∃ K ∈ S, g ∈ K) →
      IsElementaryAmenable G

Used by 1

Used byKourovka Problem 16.52 (Linnell–Schick)

DefinitionKourovka Problem 16.52 (Linnell–Schick)#✓fully proved

The statement that every finitely presented elementary amenable group \(G\) is solvable-by-finite, that is, \(G\) has a solvable subgroup of finite index.

def finitelyPresentedElementaryAmenableVirtuallySolvable : Prop :=
  ∀ (G : Type) [Group G], Group.IsFinitelyPresented G → IsElementaryAmenable G →
    ∃ N : Subgroup G, N.FiniteIndex ∧ Group.IsSolvable N

Uses 1 · Used by 1

Statement usesElementary amenable groups

Used byFinitely presented elementary amenable groups need not be virtually solvable

TheoremFinitely presented elementary amenable groups need not be virtually solvable#●ready to prove

There is a finitely presented elementary amenable group \(G\) that is not solvable-by-finite: no subgroup of finite index in \(G\) is solvable. This answers Kourovka Problem 16.52 (P. Linnell, T. Schick) in the negative.

As Belegradek and Cornulier observed, Houghton's groups \(H_n\), finitely presented for \(n \ge 3\) by Brown, are elementary amenable (the locally finite group of finitary permutations extended by \(\mathbb{Z}^{n-1}\)) but not virtually solvable.

public theorem_wanted finitelyPresentedElementaryAmenableVirtuallySolvable_refuted :
    ¬ finitelyPresentedElementaryAmenableVirtuallySolvable

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 16.52 (P. Linnell, T. Schick); resolution: C. H. Houghton, Arch. Math. (Basel) 31 (1978/79), 254-258; K. S. Brown, J. Pure Appl. Algebra 44 (1987), 45-75; observation of I. Belegradek and Y. Cornulier, MathOverflow question 107996, Kourovka Archive, Problem 16.52 (No, not every: Houghton's groups are finitely presented (Brown) and elementary amenable, but not virtually solvable), https://mathoverflow.net/questions/107996.

Uses 1

Statement usesKourovka Problem 16.52 (Linnell–Schick)

2 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.