Decompositions into shifted standard-form representatives

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormGraded_shifted_exists_iso {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (M : Graded.FiniteGradedModule.ShiftedModule) (hM : CategoryTheory.Indecomposable M) : ∃ (i : Fin S.n) (s : ℤ), Nonempty (M ≅ { obj := S.standardFormGradedFamily i, degree := s })

Classification also applies when an arbitrary external shift is already present.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormGraded_decomposition {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (M : Graded.FiniteGradedModule.ShiftedModule) : ∃ (n : ℕ) (i : Fin n → Fin S.n) (s : Fin n → ℤ), Nonempty (M ≅ ⨁ fun (j : Fin n) => { obj := S.standardFormGradedFamily (i j), degree := s j })

Every graded module is a finite sum of the classified shifted vertex modules.