Homogeneous path maps are spanned by degree-one factorizations

def MagnitudeConjecture.LinearPathCategory.HomogeneousQuotient.firstDegreeComposites {k : Type u} [Field k] {Q : Type v} [Quiver Q] (R : (X Y : Category k Q) → Set (X ⟶ Y)) (x y : Q) (n : ℕ) : Set (obj R (LinearPathCategory.obj k Q x) ⟶ obj R (LinearPathCategory.obj k Q y))

Composites of a degree-one map and a degree-n map through a vertex.

theorem MagnitudeConjecture.LinearPathCategory.HomogeneousQuotient.lengthComponent_le_firstDegreeComposites {k : Type u} [Field k] {Q : Type v} [Quiver Q] (R : (X Y : Category k Q) → Set (X ⟶ Y)) (x y : Q) (n : ℕ) : lengthComponent R (LinearPathCategory.obj k Q x) (LinearPathCategory.obj k Q y) (n + 1) ≤ Submodule.span k (firstDegreeComposites R x y n)

Splitting the final quiver edge gives the first categorical factor, because the representable convention reverses paths.