Classification of the graded indecomposables of the standard form

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormGraded_shift_indecomposable {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (i : Fin S.n) (s : ℤ) : CategoryTheory.Indecomposable { obj := S.standardFormGradedFamily i, degree := s }

Every listed shift is a graded indecomposable.

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

Every graded indecomposable is a shift of a standard-form vertex module.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormGraded_label_shift_unique {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {i j : Fin S.n} {s t : ℤ} (e : { obj := S.standardFormGradedFamily i, degree := s } ≅ { obj := S.standardFormGradedFamily j, degree := t }) : i = j ∧ s = t

An isomorphism between two shifted representatives determines both labels.