Papers With

← All papers
First page of Representation embeddings and the third Brauer–Thrall conjecture

Representation embeddings and the third Brauer–Thrall conjecture

Haruhisa Enomoto

math.RT Nov 4, 2026 · v1 math.RA
formalization mathlib algebra ai-agents
Read PDF arXiv abstract Code
TL;DR
The main theorem and corollary on large indecomposable modules are formalized in Lean 4 with Mathlib, largely produced by an AI model.
Abstract
Let $A$ be a representation-infinite finite-dimensional algebra over an algebraically closed field $k$. We prove that for every infinite cardinal $κ$ there is an indecomposable $A$-module $M$ with $\dim_k M=κ$. Over algebraically closed fields, this settles Simson's conjecture, also called the third Brauer–Thrall conjecture, that every representation-infinite finite-dimensional algebra has indecomposable modules of arbitrarily large cardinality. To construct these modules, we extend Bongartz's representation embedding from finite-dimensional Kronecker modules without a simple injective summand to such modules of arbitrary dimension. The extended functor commutes with direct sums and filtered colimits and preserves the dimension of infinite-dimensional modules. Applying it to the indecomposable Kronecker modules of every infinite dimension constructed by Göbel and Simson yields the required $A$-modules.
Problem

Simson's conjecture, also called the third Brauer–Thrall conjecture, asserts that every representation-infinite finite-dimensional algebra has indecomposable modules of arbitrarily large cardinality. The paper addresses this case over algebraically closed fields.

Approach

Bongartz's representation embedding is extended from finite-dimensional Kronecker modules without a simple injective summand to such modules of arbitrary dimension. The extended functor commutes with direct sums and filtered colimits and preserves the dimension of infinite-dimensional modules. Applying it to the Göbel–Simson indecomposable Kronecker modules of every infinite dimension gives the required A-modules. Theorem A and Corollary 1.1 were formalized in Lean 4 with Mathlib, mainly by Claude Opus. The formalization uses alternative arguments for parts of Theorem 3.14.

Results

For every infinite cardinal κ, every representation-infinite finite-dimensional algebra over an algebraically closed field has an indecomposable module of dimension κ. This settles Simson's conjecture over algebraically closed fields, and the result is machine-checked in Lean.