google-deepmind / google-deepmind/formal-conjectures
Finite generation of the cohomology of finite-dimensional Hopf algebras
- Dominant language
- Lean
- Stars
- 1.3k
- Forks
- 485
- Avg merge
- 1d 20h
- Merged PRs (30d)
- 327
Description
### What is the conjecture
Let $A$ be a finite-dimensional Hopf algebra over a field $k$, and let $k$ be the trivial
$A$-module through the counit. The cohomology ring
$$H^*(A, k) = \mathrm{Ext}^*_A(k, k) = \bigoplus_{n \ge 0} \mathrm{Ext}^n_A(k, k)$$
is a graded-commutative $k$-algebra under the Yoneda product.
**Conjecture** (the finite generation conjecture): $H^*(A, k)$ is a finitely generated
$k$-algebra, and for every finite-dimensional $A$-module $M$ the module $\mathrm{Ext}^*_A(k, M)$
over $H^*(A, k)$ is finitely generated.
The conjecture is not due to any one author. The question for a finite-dimensional Hopf algebra was
asked by a number of mathematicians and had circulated since at least the 1990s: Friedlander and
Suslin record it while expressly declining to answer it ("We do not know whether it is reasonable
to expect finite generation of the cohomology of an arbitrary finite dimensional Hopf algebra"),
and Friedlander and Negron later describe the conjecture as having "existed as a question at least
since the 90's" and as "recently stated explicitly in the work of Etingof and Ostrik". The
Oberwolfach mini-workshop report on the subject likewise calls it a question "asked by a number of
mathematicians", which "is stated as a conjecture in a 2004 paper of Etingof and Ostrik in a more
general setting". What Etingof and Ostrik contribute is that explicit statement and its extension
from Hopf algebras to every finite tensor category
([arXiv:math/0301027](https://arxiv.org/abs/math/0301027), Conjecture 2.18); that is the form
formalised in the accompanying PR.
Known cases:
* $A$ cocommutative, that is, the group algebra of a finite group scheme: Friedlander–Suslin,
Theorem 1.1, which gives both the algebra and the module half.
* $A = k[G]$ for a finite group $G$: the theorem of Evens and Venkov, proved for a $p$-group by
Golod.
* $A$ commutative: noted by Etingof and Ostrik, and by Friedlander–Suslin (attributed there to
Avramov).
* Restricted Lie algebras (Friedlander–Parshall), Lusztig's small quantum groups
(Ginzburg–Kumar), and pointed Hopf algebras with abelian group of grouplikes
(Mastnak–Pevtsova–Schauenburg–Witherspoon).
The general case is open. Bergh ([arXiv:2604.20491](https://arxiv.org/abs/2604.20491), April 2026)
shows it is equivalent to finite generation of the Hochschild cohomology of the endomorphism
algebras of the projective generators.
**Sources:**
- P. Etingof, V. Ostrik, *Finite tensor categories*, Mosc. Math. J. 4 (2004), no. 3, 627–654,
Conjecture 2.18; https://arxiv.org/abs/math/0301027
- E. M. Friedlander, A. Suslin, *Cohomology of finite group schemes over a field*,
Invent. Math. 127 (1997), 209–270; https://doi.org/10.1007/s002220050119
- L. Evens, *The cohomology ring of a finite group*, Trans. Amer. Math. Soc. 101 (1961), 224–239;
https://doi.org/10.1090/S0002-9947-1961-0137742-1
- B. B. Venkov, *Cohomology algebras for some classifying spaces*, Dokl. Akad. Nauk SSSR 127
(1959), 943–944
- E. S. Golod, *The cohomology ring of a finite $p$-group*, Dokl. Akad. Nauk SSSR 125 (1959),
703–706
- E. M. Friedlander, C. Negron, *Cohomology for Drinfeld doubles of some infinitesimal group
schemes*, Algebra Number Theory 12 (2018), 1281–1309, p. 1281 for the conjecture and its
history; https://doi.org/10.2140/ant.2018.12.1281
- H. Krause, S. Witherspoon, J. J. Zhang (organisers), *Mini-Workshop: Cohomology of Hopf Algebras
and Tensor Categories*, Oberwolfach Rep. (2019), 663–693, p. 664;
https://doi.org/10.4171/OWR/2019/11
### Prerequisites needed
Mathlib has `HopfAlgebra`, `Bialgebra`, `Coalgebra.IsCocomm`, `ModuleCat` and the
derived-category `Ext` (`Mathlib.Algebra.Category.ModuleCat.Ext.HasExt`), but no Yoneda algebra:
nothing makes `⨁ n, Ext X X n` a ring. That has to be supplied before the conjecture can be
stated.
AMS: 16, 18.
Contributor guide
Research direction
Start by reading Mathlib's HopfAlgebra, Bialgebra, Coalgebra.IsCocomm, ModuleCat, and ModuleCat.Ext.HasExt APIs. The work is done when the Yoneda algebra structure on ⨁ n, Ext X X n is supplied and the finite-generation conjecture can be stated formally; no implementation files or tests are named.
Written by the indexing model from the issue text.
Assessment
- Domain
- tooling
- Issue type
- Feature
- Difficulty
- 5/5
- Estimated time
- Over a week
- Activity status
- Active
- Clarity
- Mostly clear
- Newbie friendliness
- 25/100