The actual graded direct-sum decomposition of each standard-form matrix object

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.gradedBiproductHomFinite {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) : FiniteDimensional k (X ⟶ Y)

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormGradedMatrixBicone {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (X : CategoryTheory.Mat_ S.StandardFormMeshCategory) (t : ℤ) : CategoryTheory.Limits.Bicone fun (i : X.ι) => { obj := S.standardFormGradedVertexFunctor.obj (X.X i), degree := t }

The actual matrix direct sum, with its degree-zero coordinate maps.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormGradedMatrixBicone_isBilimit {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (X : CategoryTheory.Mat_ S.StandardFormMeshCategory) (t : ℤ) : (S.standardFormGradedMatrixBicone X t).IsBilimit

The coordinate maps still sum to the identity after graded realization.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormGradedMatrixBiproductIso {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (X : CategoryTheory.Mat_ S.StandardFormMeshCategory) (t : ℤ) : { obj := S.standardFormGradedFunctor.obj X, degree := t } ≅ ⨁ fun (i : X.ι) => { obj := S.standardFormGradedVertexFunctor.obj (X.X i), degree := t }

The shift of an actual represented matrix object is the biproduct of its represented entries at that same shift, retaining every occurrence.