Locality and homogeneous splitting for graded indecomposable modules

theorem MagnitudeConjecture.Graded.FiniteGradedModule.localEnd_of_indecomposable {k A : Type u} [Field k] [Ring A] [Algebra k A] {R : VectorGrading k A} (X : ShiftedModule) (hX : CategoryTheory.Indecomposable X) : IsLocalRing (CategoryTheory.End X)

Graded indecomposability gives local graded endomorphisms without requiring indecomposability of the underlying ungraded module.

theorem MagnitudeConjecture.Graded.FiniteGradedModule.exists_iso_shift_of_decomposition {k A : Type u} [Field k] [Ring A] [Algebra k A] {R : VectorGrading k A} {ι : Type w} (s : Finset ι) (X : FiniteGradedModule R) (Y : ι → FiniteGradedModule R) (f : (j : ι) → X ⟶ Y j) (g : (j : ι) → Y j ⟶ X) (hsum : ∑ j ∈ s, CategoryTheory.CategoryStruct.comp (f j) (g j) = CategoryTheory.CategoryStruct.id X) (hX : CategoryTheory.Indecomposable { obj := X, degree := 0 }) (hY : ∀ j ∈ s, IsLocalRing (CategoryTheory.End (Y j))) : ∃ j ∈ s, ∃ (d : ℤ), Nonempty ({ obj := X, degree := 0 } ≅ { obj := Y j, degree := -d })

Given a finite ungraded decomposition into modules with local endomorphisms, a graded indecomposable is isomorphic to a shift of one of those modules.