Underlying representatives of the standard-form graded modules

@[instance_reducible]

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.rdGradedRepresentativesQuiver {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : Quiver (Fin S.n)

@[instance_reducible]

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.rdGradedRepresentativesArrowFintype {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x y : Fin S.n) : Fintype (x ⟶ y)

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormGradedObjectUnderlyingIso {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (X : CategoryTheory.Mat_ S.StandardFormMeshCategory) : (S.standardFormGradedObject ⋯ X).module ≅ (S.standardFormProjectiveVertexModuleAlgebraEquivalence.functor.obj (S.standardGradedRecovery.obj X)).obj

Forgetting the grading recovers the existing represented right module.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormGradedFamily {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) : Graded.FiniteGradedModule (S.standardFormOppositeAlgebraGrading ⋯)

The graded representatives, with the labels of the original finite skeleton.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormGradedFamilyIso {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.standardFormGradedFamily i).module ≅ S.standardFormAlgebraIndecomposableSkeleton.obj i

The underlying graded representatives are the existing algebra skeleton.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormGradedFamily_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) : CategoryTheory.Indecomposable (S.standardFormGradedFamily i).module

Each graded representative is indecomposable after forgetting its grading.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormGradedFamily_complete {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (M : Category (S.standardFormAlgebra ⋯)) (hfin : Module.Finite k ↑M) (hM : CategoryTheory.Indecomposable M) : ∃ (i : Fin S.n), Nonempty (M ≅ (S.standardFormGradedFamily i).module)

Every finite ungraded indecomposable has one of these gradings.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormGradedFamily_skeletal {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) (h : Nonempty ((S.standardFormGradedFamily i).module ≅ (S.standardFormGradedFamily j).module)) : i = j

The underlying representatives have no duplicate labels.