# A counterexample to finitistic-dimension finiteness

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

- [An algebra of infinite little finitistic dimension](../../preprints/An-algebra-of-infinite-little-finitistic-dimension-September-23-2026/paper.pdf)

## Scope

The little finitistic-dimension conjecture predicts that finitely generated modules of finite projective dimension over a fixed finite-dimensional algebra have bounded projective dimensions. The formalized counterexample is a finite-dimensional complex algebra with a finitely generated module of projective dimension at least $2m-2$ and still finite for every $m\ge1$.

A separate formalized result gives a finite-dimensional complex algebra whose little and big finitistic dimensions are infinite on the left and zero on the right. Injectives fail to generate its unbounded derived category on the left and generate it on the right.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Infinite little finitistic dimension | [LittleFinitistic.lean](../ComparatorChallenges/LittleFinitistic.lean) |
| Left/right finitistic-dimension asymmetry | [FinitisticAsymmetry.lean](../ComparatorChallenges/FinitisticAsymmetry.lean) |