Representation theory · Lean 4

Multiplicative bases and deformations

A new proof of two classical theorems on representation-finite algebras, checked in Lean.

Let k be an algebraically closed field and A a finite-dimensional k-algebra with finitely many isomorphism classes of indecomposable finite-dimensional modules.

Theorem A. In every characteristic, A has a normed multiplicative basis: a basis containing a complete set of primitive orthogonal idempotents, closed under products up to zero, and meeting every power of the radical in a basis of that power.
Theorem B. If A is basic and the characteristic of k is not two, then A is standard: the mesh category k(ΓA) of its Auslander–Reiten quiver is equivalent to the category of indecomposable A-modules.
Read the statementFollow the proofPaper PDFGitHub

The classical results

Both theorems are due to Bautista, Gabriel, Roiter and Salmerón, building on the standard form of Bretscher and Gabriel. Their original proof uses an intricate combinatorial case analysis. Haruhisa Enomoto’s Multiplicative bases and deformations of representation-finite algebras gives a self-contained alternative proof. It passes to the radical grading of the module category to build the standard form A0, and then treats A as a filtered deformation of A0.

This repository formalizes the whole paper: Theorems A and B and every numbered theorem, proposition, lemma, corollary, remark and definition (the three examples are not formalized). It also proves the Auslander–Reiten theory the paper assumes. The correspondence record maps each numbered statement to its Lean declarations.

A guide to the development

Readable definitions

A Mathlib-only file states both theorems: normed multiplicative bases, almost split sequences, the Auslander–Reiten quiver and its mesh category. The library proves the connection with its own definitions.

Definitions and theorems

From the standard form to deformations

The radical grading gives the standard form and Theorem B. In characteristic two, a Bockstein argument over ℤ/4 and an associative family of multiplication tables give Theorem A.

Mathematical proof guide