Graded generator modules for the standard-form mesh category

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormIntegerHomGrading {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : GradedCategory.HomGrading k S.StandardFormMeshCategory

The actual mesh Hom grading supplied by the standard-form translation quiver.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardGradedProjectiveFamily {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (p : S.StandardFormProjectiveMeshCategory) : CategoryTheory.Mat_ S.StandardFormMeshCategory

The projective vertices, viewed in the additive envelope of the mesh category.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormAdditiveHomGrading {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (hfinite : S.StandardFormMeshHomFinite) : GradedCategory.HomGrading k (CategoryTheory.Mat_ S.StandardFormMeshCategory)

The mesh grading extended to the additive envelope.

@[reducible, inline]

abbrev MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.StandardGradedGeneratorAlgebra {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : Type u

The opposite endomorphism algebra of the projective sum in the mesh additive envelope.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardGradedGeneratorAlgebraGrading {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (hfinite : S.StandardFormMeshHomFinite) : Graded.VectorGrading k S.StandardGradedGeneratorAlgebra

The internal algebra grading for the standard-form projective generator.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardGradedGeneratorModule {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (hfinite : S.StandardFormMeshHomFinite) (X : CategoryTheory.Mat_ S.StandardFormMeshCategory) : Graded.ModuleGrading (S.standardGradedGeneratorAlgebraGrading hfinite)

Every object of the mesh additive envelope yields an actual graded right module.