Identifying the graded generator algebra with the standard form

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormGeneratorEndAlgEquiv {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) : S.standardFormAlgebra hfinite ≃ₐ[k] CategoryTheory.End (⨁ S.standardGradedProjectiveFamily)

The representable-model standard algebra and the actual mesh projective-sum endomorphism algebra are algebra-equivalent.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormOppositeGeneratorAlgEquiv {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) : (S.standardFormAlgebra hfinite)ᵐᵒᵖ ≃ₐ[k] S.StandardGradedGeneratorAlgebra

The comparison in the variance used for right modules.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormOppositeAlgebraGrading {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.standardFormAlgebra hfinite)ᵐᵒᵖ

The graded algebra structure transported to the existing standard-form algebra.