← All papers
First page of Amenability of Lie, Group and Hopf algebras

Amenability of Lie, Group and Hopf algebras

Laurent Bartholdi

math.RA Sep 9, 2026 · v1 math.GR
All main results on amenability of Hopf algebras were formalized in Lean/Mathlib (generated with ChatGPT), with a public GitHub repository.
We propose to define amenability of a Lie algebra by the existence of almost-invariant finite-dimensional subcoalgebras of its universal enveloping algebra. More generally, a module coalgebra of a cocommutative Hopf algebra is amenable if it admits almost-invariant finite-dimensional subcoalgebras. We prove a coalgebraic rounding theorem: almost-invariant finite-dimensional subspaces can be replaced, without loss in the Følner constant, by almost-invariant finite-dimensional subcoalgebras. For Lie algebras this implies that our definition is equivalent to Elek's amenability of the left regular module of the universal enveloping algebra seen merely as an associative algebra. For groups this recovers the result that a group is amenable if and only if its group ring is algebraically amenable. It furthermore shows that, for every amenable group, all its nonzero modules are amenable, thus proving an assertion by Gromov. We prove that amenable Hopf algebras are closed under taking subalgebras, quotients, cleft extensions, and directed unions, and that every Hopf algebra locally of subexponential growth is amenable. We give examples of amenable Lie algebras which are not elementarily amenable. Finally, we show that amenability passes to the associated graded Hopf-module coalgebra.

The paper seeks a notion of amenability for Lie algebras, and more generally for cocommutative Hopf algebras and their module coalgebras, that is compatible with Elek's algebraic amenability and with classical group amenability.

Amenability is defined by the existence of almost-invariant finite-dimensional subcoalgebras. The central tool is a coalgebraic rounding theorem, proved via density filtrations inspired by Harder-Narasimhan theory and submodular optimization. It replaces almost-invariant subspaces by subcoalgebras with no loss in the Følner constant. The main results were formalized in Lean/Mathlib, with the formalization produced by ChatGPT.

The definition is equivalent to algebraic amenability of the universal enveloping algebra, and it recovers the group-ring characterization of amenable groups. It also proves Gromov's assertion that all nonzero modules of amenable groups are amenable. Amenability is shown to be closed under subalgebras, quotients, cleft extensions and directed unions, and to pass to the associated graded Hopf-module coalgebra. An amenable Lie algebra of exponential growth that is not elementarily amenable is constructed.