Nilpotence of the radical of a representation-finite module category

The biproduct of the chosen indecomposable representatives is a finite additive generator of FGModuleCat Aᵐᵒᵖ. Its endomorphism ring is finite-dimensional over the coefficient field and hence Artinian. The generic finite-generator theorem therefore supplies the canonical nilpotent categorical radical required by the tau-category interface.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.additiveGenerator {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : FinitelyGeneratedCategory A

The finite biproduct of all chosen indecomposable right modules.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.additiveGenerator_isFiniteAddGenerator {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : CategoryTheory.IsFiniteAddGenerator S.additiveGenerator

Every finitely generated right module is a retract of a finite biproduct of copies of the chosen additive generator.

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.additiveGeneratorEndArtinian {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : IsArtinianRing (CategoryTheory.End S.additiveGenerator)

The additive generator's endomorphism ring is Artinian because its Hom space is finite-dimensional over the coefficient field.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.fgNilpotentRadicalData {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : QuotientSubmoduleEquidistribution.CategoricalRadical.NilpotentRadicalData (FinitelyGeneratedCategory A)

The canonical categorical radical of the literal finitely generated right-module category is nilpotent in finite representation type.