Homogeneous mesh maps are exactly the graded module maps

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormMeshEmbeddingLinear {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : CategoryTheory.Functor.Linear k (CategoryTheory.Mat_.embedding S.StandardFormMeshCategory)

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormGradedVertexFunctor {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : CategoryTheory.Functor S.StandardFormMeshCategory (Graded.FiniteGradedModule (S.standardFormOppositeAlgebraGrading ⋯))

The vertex realization by graded modules, with all underlying maps retained.

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

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

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

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.instLinearStandardFormMeshCategoryFiniteGradedModuleMulOppositeStandardFormAlgebraStandardFormOppositeAlgebraGradingStandardFormGradedVertexFunctor {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : CategoryTheory.Functor.Linear k S.standardFormGradedVertexFunctor

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormGradedVertexFunctor_homogeneous {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {X Y : S.StandardFormMeshCategory} {d : ℤ} {f : X ⟶ Y} (hf : f ∈ S.standardFormIntegerHomGrading.component X Y d) : S.standardFormGradedVertexFunctor.map f ∈ Graded.FiniteGradedModule.homGrading.component (S.standardFormGradedVertexFunctor.obj X) (S.standardFormGradedVertexFunctor.obj Y) d

The vertex realization preserves each degree.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormGradedHomEquiv {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (X Y : S.StandardFormMeshCategory) (s t : ℤ) : ↥(S.standardFormIntegerHomGrading.component X Y (s - t)) ≃ₗ[k] { obj := S.standardFormGradedVertexFunctor.obj X, degree := s } ⟶ { obj := S.standardFormGradedVertexFunctor.obj Y, degree := t }

The manuscript's graded Hom identification, with degree equal to source shift minus target shift.