Finitely generated recovery of the actual graded standard form

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormGradedUnderlyingFGNatIso {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : S.standardFormGradedFunctor.comp Graded.FiniteGradedModule.underlyingFG ≅ S.standardGradedRecovery.comp S.standardFormProjectiveVertexModuleAlgebraEquivalence.functor

The graded realization recovers the established standard-form functor already in the finitely generated module category.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardGradedRawRecoveryIso {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : S.standardFormMeshRawFunctor.mapMat_.comp S.standardGradedRecovery ≅ S.standardFormAdditiveRestrictedYonedaFunctor

Entrywise passage from the induced vertex model to the raw mesh gives the same recovered finite module, including its chosen biproduct coordinates.