Higher-degree graded maps factor with neither factor split

@[instance_reducible]

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.rdGradedHigherDegreeQuiver {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : Quiver (Fin S.n)

@[instance_reducible]

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.rdGradedHigherDegreeArrowFintype {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x y : Fin S.n) : Fintype (x ⟶ y)

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormGraded_higherDegree_factorization {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) (t : ℤ) (n : ℕ) (hn : 0 < n) (f : { obj := S.standardFormGradedVertexFunctor.obj X, degree := t + ↑n + 1 } ⟶ { obj := S.standardFormGradedVertexFunctor.obj Y, degree := t }) : f ∈ CategoryTheory.noBackwardFactorizations { obj := S.standardFormGradedVertexFunctor.obj X, degree := t + ↑n + 1 } { obj := S.standardFormGradedVertexFunctor.obj Y, degree := t }

Every map of degree n+1, n positive, factors through intermediate shifted modules admitting no reverse maps to either endpoint.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormGraded_higherDegree_not_irreducible {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) (t : ℤ) (n : ℕ) (hn : 0 < n) (f : { obj := S.standardFormGradedVertexFunctor.obj X, degree := t + ↑n + 1 } ⟶ { obj := S.standardFormGradedVertexFunctor.obj Y, degree := t }) (hf : f ≠ 0) : ¬QuotientSubmoduleEquidistribution.IsIrreducibleMorphism f

Nonzero higher-degree maps are not irreducible.