The irreducible maps between graded standard-form representatives

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormGraded_irreducible_iff {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 : ℤ) (f : { obj := S.standardFormGradedVertexFunctor.obj X, degree := s } ⟶ { obj := S.standardFormGradedVertexFunctor.obj Y, degree := t }) : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism f ↔ f ≠ 0 ∧ s = t + 1

Exactly the nonzero maps of degree one are irreducible in the full graded category.