Standard-form modules as objects of the finite graded category

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormGradedObject {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.FiniteGradedModule (S.standardFormOppositeAlgebraGrading hfinite)

Bundle the transported generator module with its canonical field action.

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

The graded object attached to a single mesh vertex.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormGradedMap {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 Y : CategoryTheory.Mat_ S.StandardFormMeshCategory} (f : X ⟶ Y) : S.standardFormGradedObject hfinite X ⟶ S.standardFormGradedObject hfinite Y

The map of bundled graded objects induced by any ambient morphism.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormGradedMap_homogeneous {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 Y : CategoryTheory.Mat_ S.StandardFormMeshCategory} {d : ℤ} {f : X ⟶ Y} (hf : f ∈ (S.standardFormAdditiveHomGrading hfinite).component X Y d) : (S.standardFormGradedObject hfinite X).grading.Homogeneous (S.standardFormGradedObject hfinite Y).grading d (S.standardFormGradedMap hfinite f)

Bundling and scalar transport preserve the degree of a represented map.