Graded classification from a complete gradable representative family

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

Forget the grading while retaining all ambient module maps.

instance MagnitudeConjecture.Graded.FiniteGradedModule.instFullModuleCatUnderlying {k A : Type u} [Field k] [Ring A] [Algebra k A] {R : VectorGrading k A} : underlying.Full

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

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

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

Ungraded indecomposability gives local ambient endomorphisms.

theorem MagnitudeConjecture.Graded.FiniteGradedModule.exists_iso_shift_of_complete_family {k A : Type u} [Field k] [Ring A] [Algebra k A] {R : VectorGrading k A} [FiniteDimensional k A] {ι : Type w} (Y : ι → FiniteGradedModule R) (hY : ∀ (i : ι), CategoryTheory.Indecomposable (Y i).module) (hcomplete : ∀ (M : ModuleCat A), Module.Finite k ↑M → CategoryTheory.Indecomposable M → ∃ (i : ι), Nonempty (M ≅ (Y i).module)) (X : FiniteGradedModule R) (hX : CategoryTheory.Indecomposable { obj := X, degree := 0 }) : ∃ (i : ι) (s : ℤ), Nonempty ({ obj := X, degree := 0 } ≅ { obj := Y i, degree := s })

If every ungraded indecomposable has a graded representative, every graded indecomposable is a shift of one of those representatives. The finite identity decomposition is constructed from ordinary module decomposition.

theorem MagnitudeConjecture.Graded.FiniteGradedModule.label_shift_eq_of_iso {k A : Type u} [Field k] [Ring A] [Algebra k A] {R : VectorGrading k A} {ι : Type w} (Y : ι → FiniteGradedModule R) (hY : ∀ (i : ι), CategoryTheory.Indecomposable (Y i).module) (hinj : ∀ (i j : ι), Nonempty ((Y i).module ≅ (Y j).module) → i = j) {i j : ι} {s t : ℤ} (e : { obj := Y i, degree := s } ≅ { obj := Y j, degree := t }) : i = j ∧ s = t

For distinct ungraded representatives, a shifted isomorphism determines both the representative label and the shift.