Finite decompositions in the category of graded modules

def MagnitudeConjecture.Graded.FiniteGradedModule.zeroObject {k A : Type u} [Field k] [Ring A] [Algebra k A] {R : VectorGrading k A} : FiniteGradedModule R

The zero graded module.

instance MagnitudeConjecture.Graded.FiniteGradedModule.instHasZeroObjectShiftedModule {k A : Type u} [Field k] [Ring A] [Algebra k A] {R : VectorGrading k A} : CategoryTheory.Limits.HasZeroObject ShiftedModule

instance MagnitudeConjecture.Graded.FiniteGradedModule.instHasFiniteBiproductsShiftedModule {k A : Type u} [Field k] [Ring A] [Algebra k A] {R : VectorGrading k A} : CategoryTheory.Limits.HasFiniteBiproducts ShiftedModule

def MagnitudeConjecture.Graded.FiniteGradedModule.shiftedUnderlying {k A : Type u} [Field k] [Ring A] [Algebra k A] {R : VectorGrading k A} : CategoryTheory.Functor ShiftedModule (ModuleCat A)

Forget both the grading and the external shift label.

instance MagnitudeConjecture.Graded.FiniteGradedModule.instFaithfulShiftedModuleModuleCatShiftedUnderlying {k A : Type u} [Field k] [Ring A] [Algebra k A] {R : VectorGrading k A} : shiftedUnderlying.Faithful

instance MagnitudeConjecture.Graded.FiniteGradedModule.instAdditiveShiftedModuleModuleCatShiftedUnderlying {k A : Type u} [Field k] [Ring A] [Algebra k A] {R : VectorGrading k A} : shiftedUnderlying.Additive

theorem MagnitudeConjecture.Graded.FiniteGradedModule.isZero_of_underlying {k A : Type u} [Field k] [Ring A] [Algebra k A] {R : VectorGrading k A} (X : ShiftedModule) (h : CategoryTheory.Limits.IsZero X.obj.module) : CategoryTheory.Limits.IsZero X

theorem MagnitudeConjecture.Graded.FiniteGradedModule.finiteDecomposition {k A : Type u} [Field k] [Ring A] [Algebra k A] {R : VectorGrading k A} (M : ShiftedModule) : Nonempty (CategoryTheory.FiniteIndecomposableDecomposition M)

Every finite-dimensional graded module has a finite graded indecomposable decomposition.