FiniteGenerationOfCohomology.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 7190 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

7 declarations, 5 contain sorry, 0 declared as axioms

Finite generation of the cohomology of finite-dimensional Hopf algebras

Let $A$ be a finite-dimensional Hopf algebra over a field $k$, and view $k$ as an $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. The finite generation conjecture asserts that it is a finitely generated $k$-algebra, and that $\mathrm{Ext}^*_A(k, M)$ is a finitely generated module over it for every finite-dimensional $A$-module $M$. Etingof and Ostrik state it for every finite tensor category; the finite-dimensional modules over a finite-dimensional Hopf algebra form the main class of examples, and the conjecture is open already in this case.

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". What Etingof and Ostrik contribute is that explicit statement, together with its extension from Hopf algebras to every finite tensor category; it is their Conjecture 2.18 that is formalised here.

The conjecture holds when $A$ is cocommutative, that is, when $A$ is the group algebra of a finite group scheme (Friedlander–Suslin). For the group algebra $k[G]$ of a finite group $G$ it is the theorem of Evens and Venkov, proved for a $p$-group by Golod. Etingof and Ostrik note that it also holds when $A$ is commutative.

Etingof and Ostrik work throughout the section containing the conjecture under the standing assumption that $k$ is algebraically closed, whereas the statements below are for an arbitrary field. The generalisation is valid. For a field extension $K/k$ one has $\mathrm{Ext}^*_{A \otimes_k K}(K, K) \cong \mathrm{Ext}^*_A(k, k) \otimes_k K$, because $k$ admits a resolution by finitely generated free $A$-modules and $K$ is flat over $k$; and finite generation descends, because the finitely many elements of $R = \mathrm{Ext}^*_A(k, k)$ occurring in a finite set of $K$-algebra generators of $R \otimes_k K$ generate a $k$-subalgebra $R'$ with $R' \otimes_k K = R \otimes_k K$, whence $R' = R$ by faithful flatness. The same argument applies to the module statement. The theorems of Friedlander–Suslin and of Evens–Venkov are stated below over an arbitrary field because that is the generality in which they are proved.

$\mathrm{Ext}$ is taken in the category of all $A$-modules rather than in the finite tensor category of finite-dimensional ones. For finite-dimensional $A$ the two agree on finite-dimensional modules, as the module docstring of FormalConjecturesForMathlib.RingTheory.Bialgebra.Cohomology explains.

References:

arXiv:math/0301027 P. Etingof, V. Ostrik, Finite tensor categories, Mosc. Math. J. 4 (2004), no. 3, 627–654; Conjecture 2.18.
Friedlander–Suslin E. M. Friedlander, A. Suslin, Cohomology of finite group schemes over a field, Invent. Math. 127 (1997), 209–270.
Evens L. Evens, The cohomology ring of a finite group, Trans. Amer. Math. Soc. 101 (1961), 224–239.
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.
Friedlander–Negron E. M. Friedlander, C. Negron, Cohomology for Drinfeld doubles of some infinitesimal group schemes, Algebra Number Theory 12 (2018), 1281–1309; the conjecture and its history, p. 1281.
Oberwolfach H. Krause, S. Witherspoon, J. J. Zhang (organisers), Mini-Workshop: Cohomology of Hopf Algebras and Tensor Categories, Oberwolfach Rep. (2019), 663–693; "asked by a number of mathematicians", p. 664.

Imports (1)

FormalConjecturesUtil

theorem HopfAlgebraCohomology.cohomologyRing_finiteType Finite generation conjecture (Etingof–Ostrik, Conjecture 2.18, algebra part) sorry line 96 source
Source documentation
Finite generation conjecture (Etingof–Ostrik, Conjecture 2.18, algebra part). For every finite-dimensional Hopf algebra $A$ over a field $k$, the cohomology ring $H^*(A, k) = \mathrm{Ext}^*_A(k, k)$ is a finitely generated $k$-algebra.

depends on sorry what this means
Statement uses: Field, Ring, HopfAlgebra, FiniteDimensional, Algebra.FiniteType, Bialgebra.cohomologyRing, Nat, CategoryTheory.Abelian.Ext, ModuleCat, Bialgebra.trivialModuleCat, Int
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat
49 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem cohomologyRing_finiteType : Algebra.FiniteType k (cohomologyRing k A) := by
…
```
theorem HopfAlgebraCohomology.cohomology_finite Finite generation conjecture (Etingof–Ostrik, Conjecture 2.18, module part) sorry line 104 source
Source documentation
Finite generation conjecture (Etingof–Ostrik, Conjecture 2.18, module part). For every finite-dimensional Hopf algebra $A$ over a field $k$ and every finite-dimensional $A$-module $M$, the cohomology $H^*(A, M) = \mathrm{Ext}^*_A(k, M)$ is a finitely generated module over $H^*(A, k)$.

depends on sorry what this means
Statement uses: Field, Ring, HopfAlgebra, FiniteDimensional, ModuleCat, Module.Finite, Bialgebra.cohomologyRing, Bialgebra.cohomology, Nat, CategoryTheory.Abelian.Ext, Bialgebra.trivialModuleCat, Int
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat
57 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem cohomology_finite (M : ModuleCat.{u} A) [FiniteDimensional k M] :
    Module.Finite (cohomologyRing k A) (cohomology k A M) := by
…
```
theorem HopfAlgebraCohomology.cohomologyRing_finiteType_of_isCocomm Friedlander–Suslin sorry line 112 source
Source documentation
Friedlander–Suslin. If $A$ is a finite-dimensional cocommutative Hopf algebra over a field $k$, that is, the group algebra of a finite group scheme over $k$, then $H^*(A, k)$ is a finitely generated $k$-algebra.

depends on sorry what this means
Statement uses: Field, Ring, HopfAlgebra, FiniteDimensional, Coalgebra.IsCocomm, Algebra.FiniteType, Bialgebra.cohomologyRing, Nat, CategoryTheory.Abelian.Ext, ModuleCat, Bialgebra.trivialModuleCat, Int
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat
53 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem cohomologyRing_finiteType_of_isCocomm [Coalgebra.IsCocomm k A] :
    Algebra.FiniteType k (cohomologyRing k A) := by
…
```
theorem HopfAlgebraCohomology.cohomology_finite_of_isCocomm Friedlander–Suslin sorry line 120 source
Source documentation
Friedlander–Suslin. If $A$ is a finite-dimensional cocommutative Hopf algebra over a field $k$ and $M$ is a finite-dimensional $A$-module, then $H^*(A, M)$ is a finitely generated module over $H^*(A, k)$.

depends on sorry what this means
Statement uses: Field, Ring, HopfAlgebra, FiniteDimensional, Coalgebra.IsCocomm, ModuleCat, Module.Finite, Bialgebra.cohomologyRing, Bialgebra.cohomology, Nat, CategoryTheory.Abelian.Ext, Bialgebra.trivialModuleCat, Int
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat
61 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem cohomology_finite_of_isCocomm [Coalgebra.IsCocomm k A] (M : ModuleCat.{u} A)
    [FiniteDimensional k M] : Module.Finite (cohomologyRing k A) (cohomology k A M) := by
…
```
theorem HopfAlgebraCohomology.cohomologyRing_finiteType_monoidAlgebra Evens–Venkov sorry line 128 source
Source documentation
Evens–Venkov. For a finite group $G$ and a field $k$, the cohomology ring $H^*(G, k) = \mathrm{Ext}^*_{k[G]}(k, k)$ of the group algebra $k[G]$ is a finitely generated $k$-algebra.

depends on sorry what this means
Statement uses: Field, Group, Finite, Algebra.FiniteType, Bialgebra.cohomologyRing, MonoidAlgebra, Nat, CategoryTheory.Abelian.Ext, ModuleCat, Bialgebra.trivialModuleCat, Int
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat
57 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem cohomologyRing_finiteType_monoidAlgebra (G : Type u) [Group G] [Finite G] :
    Algebra.FiniteType k (cohomologyRing k (MonoidAlgebra k G)) := by
…
```
theorem HopfAlgebraCohomology.cohomology_trivialModuleCat Sanity check: taking the coefficient module M of the module statement to be k itself gives back the cohomology ring line 136 source
Source documentation
Sanity check: taking the coefficient module M of the module statement to be k itself gives back the cohomology ring.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Ring, HopfAlgebra, Eq, Bialgebra.cohomology, Bialgebra.trivialModuleCat, Bialgebra.cohomologyRing
Proof uses: rfl
14 instances, coercions and auxiliary constants left out.
```
theorem cohomology_trivialModuleCat :
    cohomology k A (trivialModuleCat k A) = cohomologyRing k A :=
…
```
theorem HopfAlgebraCohomology.cohomologyRing_nontrivial Sanity check: the cohomology ring is not the zero ring, over which every finiteness statement would hold trivially line 144 source
Source documentation
Sanity check: the cohomology ring is not the zero ring, over which every finiteness statement would hold trivially.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Ring, HopfAlgebra, Nontrivial, Bialgebra.cohomologyRing
Proof uses: Bialgebra.nontrivial_cohomologyRing
10 instances, coercions and auxiliary constants left out.
```
theorem cohomologyRing_nontrivial : Nontrivial (cohomologyRing k A) :=
…
```