Readable definitions
A small independent file states the complete result using Mathlib. The library proves the connection with every production definition.
Definitions and theoremRepresentation theory · Lean 4
The magnitude conjecture
A lower bound for the magnitude of a module category, with an exact characterization of equality.
Let A be a finite-dimensional algebra of finite representation type over an algebraically closed field k. Choose one representative of every indecomposable finite-dimensional right A-module. Their Hom dimensions form a matrix H.
The matrix H is invertible. The sum of the entries of H−1 is at least the number of simple-module isomorphism classes. Equality holds exactly when the basic algebra of A is special biserial.
The theorem has no restriction on the characteristic of k, and A need not be basic.
What is magnitude?
For indecomposable representatives M1, …, Mn, the entry Hij is dimk HomA(Mi, Mj). Magnitude is the sum of all entries of its inverse, viewed over the rational numbers. The formal theorem also proves that this inverse is well defined.
The original conjecture appears in Børve, Horiatakis, and Kalck’s Magnitude of module categories. This formalization proves the main theorem of Haruhisa Enomoto’s Magnitude of module categories and special biserial algebras; the correspondence record maps the paper to the Lean proof.
A guide to the development
From deletion to equality
Finite graded intervals and a uniform surplus bound give the inequality. Separated intervals, almost-split transfer and socle reduction determine the equality case.
Mathematical proof guide