Elementary amenable groups (Day; Chou 1980)

Definition

Chou_ElementaryAmenable

by dbenbenn · Sep 17, 2026 · Mathlib 0df444a (Lean v4.33.1)

amenabilitygroup-theorypiecewise-linearthompsons-group

The class of elementary amenable groups, from Chou, Elementary amenable groups, Illinois J. Math. 24 (1980).

p. 396: “As in Day [3] let $EG$ be the smallest class of groups which contains all finite groups and all abelian groups and is closed under processes (I)–(IV).” The four processes are only named, without a defining sentence, in the sentence before: “(I) subgroups, (II) factor groups, (III) group extensions and (IV) direct unions”. Two sentences later: “We will call groups in $EG$ elementary amenable groups.” Formally, Chou.ElementaryAmenable G is an inductive predicate on groups $G$ (within one universe) generated by: every finite group; every abelian group; any group isomorphic to one already in the class; any subgroup $H \le G$ of a group in the class; any quotient $G/N$ by a normal subgroup of a group in the class; any group $G$ possessing a normal subgroup $N$ with $N$ and $G/N$ in the class; and any group $G$ that is the supremum $\bigsqcup_i H_i = G$ of a directed family of subgroups $H_i$ each in the class. Closure under isomorphism is made a clause because a class of groups is by convention isomorphism-closed, while a group merely isomorphic to a subgroup or quotient is not literally one.

The bundle defines the class only. Chou's Proposition 2.2, that the same class is obtained using only extensions and direct unions, is not stated or proved here; the mission's Theorem 4.10 argues by induction over the predicate directly and does not need it.

Definition code

import Mathlib

/-!
# Elementary amenable groups

The class of **elementary amenable** groups, as in Chou, *Elementary amenable groups*,
Illinois J. Math. 24 (1980) 396–407, p. 396, following Day: "let EG be the smallest class of
groups which contains all finite groups and all abelian groups and is closed under processes
(I)–(IV)", the processes being (I) subgroups, (II) factor groups, (III) group extensions and
(IV) direct unions.  Cannon–Floyd–Parry, *Introductory notes on Richard Thompson's groups*,
L'Enseignement Math. (2) 42 (1996), Theorem 4.10, p. 233, cite Chou for the notion; the namespace is Chou's because the class is his paper's subject, not theirs.

The class is realised as an inductive predicate on groups within one universe.  A class of
groups is closed under isomorphism by convention; that closure is a constructor here, since a
group merely isomorphic to a subgroup or quotient is not literally one.  The directed-union
clause is stated for a directed family of subgroups whose supremum is the whole group.
-/

universe u

namespace Chou

/-- `ElementaryAmenable G`: `G` lies in the smallest class of groups containing all finite
groups and all abelian groups and closed under isomorphism, subgroups, quotients, extensions
and directed unions of subgroups. -/
inductive ElementaryAmenable : (G : Type u) → [Group G] → Prop
  /-- Every finite group is elementary amenable. -/
  | of_finite (G : Type u) [Group G] [Finite G] : ElementaryAmenable G
  /-- Every abelian group is elementary amenable. -/
  | of_commGroup (G : Type u) [CommGroup G] : ElementaryAmenable G
  /-- The class is closed under isomorphism. -/
  | of_mulEquiv {G H : Type u} [Group G] [Group H] (e : G ≃* H) :
      ElementaryAmenable G → ElementaryAmenable H
  /-- A subgroup of an elementary amenable group is elementary amenable. -/
  | subgroup {G : Type u} [Group G] (H : Subgroup G) :
      ElementaryAmenable G → ElementaryAmenable H
  /-- A quotient of an elementary amenable group is elementary amenable. -/
  | quotient {G : Type u} [Group G] (N : Subgroup G) [N.Normal] :
      ElementaryAmenable G → ElementaryAmenable (G ⧸ N)
  /-- An extension of an elementary amenable group by an elementary amenable group is
  elementary amenable: if `N` is normal in `G` with `N` and `G ⧸ N` in the class, so is `G`. -/
  | extension {G : Type u} [Group G] (N : Subgroup G) [N.Normal] :
      ElementaryAmenable N → ElementaryAmenable (G ⧸ N) → ElementaryAmenable G
  /-- A directed union of elementary amenable subgroups is elementary amenable. -/
  | directedUnion {G : Type u} [Group G] {ι : Type u} (H : ι → Subgroup G)
      (hdir : Directed (· ≤ ·) H) (hsup : ⨆ i, H i = ⊤) :
      (∀ i, ElementaryAmenable (H i)) → ElementaryAmenable G

end Chou

Source

Chou, C., Elementary amenable groups, Illinois J. Math. 24 (1980) 396–407, https://projecteuclid.org/euclid.ijm/1256047608, p. 396 (definition of EG); cited by Cannon–Floyd–Parry, Introductory notes on Richard Thompson's groups, L'Enseignement Math. (2) 42 (1996), https://doi.org/10.5169/seals-87877, Theorem 4.10, p. 233.

Human review

Endorsed by Shuze Chen · Sep 19, 2026
Endorsed by dbenbenn · Sep 19, 2026
Confirmed by the mission captain (proposal self-audit).

View graph