← All papers
First page of A counterexample to the pure semisimplicity conjecture

A counterexample to the pure semisimplicity conjecture

Junpeng Ren

math.RA Oct 29, 2026 · v1
The main theorem, a counterexample to the pure semisimplicity conjecture, is fully formalized in Lean 4 with Mathlib, and a public repository is provided.
A ring is right pure semisimple if every right module is a direct sum of finitely generated modules, and the pure semisimplicity conjecture asserts that every such ring is of finite representation type. In this article, a division ring extension $H\subseteq T$ is constructed such that the bimodule ${}_HT_T$ has right dimension sequence $(1,2,2,2,\dots)$ and $T$ is infinite-dimensional as a left $H$-space. The division ring $T$ is the union of the fraction division rings of the nearest-neighbour quantum Laurent algebras with parameter $1/2$, and $H$ is the image of $T$ under a compatible family of conjugations. The extension is controlled by right bases of every length and by two-sided flags of adjacent division subrings, which identify all iterated right duals up to explicit twists. It follows that the triangular ring $\left(\begin{smallmatrix}H&T\\0&T\end{smallmatrix}\right)$ is right pure semisimple but neither left pure semisimple nor of finite representation type, so that the pure semisimplicity conjecture fails.

The pure semisimplicity conjecture asserts that every right pure semisimple ring is of finite representation type. Simson reduced the question to a generalized Artin problem about division ring extensions with controlled dimensions of iterated dual bimodules.

A division ring T is built as the union of fraction division rings of nearest-neighbour quantum Laurent algebras with parameter 1/2. Subrings H_r are defined as images of T under compatible conjugations, and they satisfy a basis condition (B) and a flag condition (F). These conditions determine all iterated right duals of the bimodule _H T_T. The main theorem is formalized in Lean 4 with Mathlib and replayed by the Lean kernel.

The bimodule _H T_T has right dimension sequence (1,2,2,2,...), and T is infinite-dimensional as a left H-space. The triangular ring [[H,T],[0,T]] is therefore right pure semisimple but neither left pure semisimple nor of finite representation type, which disproves the conjecture. The Lean formalization is available on GitHub.