The graded irreducible quotient dimension in every degree

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormGraded_radical_bot_of_le {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 : ℤ) (hst : s ≤ t) : CategoricalIrreducible.radical k { obj := S.standardFormGradedVertexFunctor.obj X, degree := s } { obj := S.standardFormGradedVertexFunctor.obj Y, degree := t } = ⊥

Nonpositive degree has no nonzero radical morphisms between the representatives.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormGraded_irreducible_finrank {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 : ℤ) : Module.finrank k (CategoricalIrreducible.Space k { obj := S.standardFormGradedVertexFunctor.obj X, degree := s } { obj := S.standardFormGradedVertexFunctor.obj Y, degree := t }) = if s = t + 1 then Module.finrank k ↥(S.standardFormIntegerHomGrading.component X Y 1) else 0

Only degree one contributes to the intrinsic irreducible quotient dimension.