Papers With

← All papers
First page of On extensive amenability of algebras

On extensive amenability of algebras

Laurent Bartholdi

math.RA Sep 30, 2026 · v1
formalization mathlib algebra
Read PDF arXiv abstract Code
TL;DR
The main results on extensive amenability of modules over Hopf algebras are formalized in Lean/Mathlib, with a public GitHub repository.
Abstract
For a module \(M\) over a cocommutative Hopf algebra \(\mathscr A\), we define extensive amenability by amenability of its symmetric algebra as a module over \(\operatorname{Sym}(M)\#\mathscr A\). Using the author's coalgebraic rounding and quotient theorems, we prove that nonzero extensively amenable modules are amenable, that every module over an amenable Hopf algebra is extensively amenable, and that extensive amenability is preserved and reflected by short exact sequences. For permutation modules this definition agrees, over every field, with extensive amenability of group actions. A final section gives the modifications for exterior algebras and establishes the comparison between the two definitions in several cases.
Problem

The paper extends the notion of extensive amenability from group actions to modules over cocommutative Hopf algebras. A module is defined to be extensively amenable when its symmetric algebra is amenable as a module over the smash product Sym(M)#A.

Approach

The proofs use the author's coalgebraic rounding and quotient theorems, a tensor-factor extraction lemma for Følner spaces, and filtration and associated-graded arguments. Permutation modules are compared with group actions through the augmentation filtration of a free abelian group algebra. An exterior-algebra variant is handled in the setting of Hopf superalgebras.

Results

Nonzero extensively amenable modules are amenable, and every module over an amenable Hopf algebra is extensively amenable. Extensive amenability is preserved and reflected by short exact sequences. For permutation modules, the definition agrees over every field with extensive amenability of the underlying G-set. The main results are formalized in Lean/Mathlib.