Two-sided ideals of a representation-finite algebra

Every finite-dimensional right module over a representation-finite algebra is a finite direct sum of members of one fixed finite indecomposable family. Annihilators turn direct sums into intersections, and every two-sided ideal is the annihilator of the corresponding regular quotient. Consequently the two-sided ideal lattice is finite.

The proof is the right-module migration of the Jans finite-ideal argument formalized in CartanDeterminant.Algebra.RepresentationFiniteIdeals at homological-conjectures commit 60736a0a. It is reproduced here so the magnitude package remains Mathlib-only.

theorem MagnitudeConjecture.RightModule.IsRepresentationFinite.finite_twoSidedIdeal {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (hA : IsRepresentationFinite k A) : Finite (TwoSidedIdeal A)

A finite-dimensional representation-finite algebra has only finitely many two-sided ideals. The decomposition argument is first run on the literal left-module model over Aᵐᵒᵖ; the final statement is transported back along the order isomorphism between ideals of a ring and its opposite.