The surviving branch of a string-arrow cokernel

For a displayed arrow a : x ⟶ y, the radical of the Butler--Ringel module V(a) is obtained from the radical of the represented projective P(y) by deleting the coordinate indexed by a. Since a special-biserial vertex has at most two incoming arrows, at most one uniserial branch remains.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.isUniserialModule_pi_of_subsingleton {R : Type u} [Ring R] {I : Type u} [Subsingleton I] (M : I → Type u) [(i : I) → AddCommGroup (M i)] [(i : I) → Module R (M i)] (hM : ∀ (i : I), IsUniserialModule R (M i)) : IsUniserialModule R ((i : I) → M i)

A dependent family of uniserial modules indexed by a subsingleton type is uniserial.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.arrowCokernelFGObj_isUniserial {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) {x y : Q} (a : x ⟶ y) : IsUniserialModule P.quotientCategoryAlgebraᵐᵒᵖ ↑(P.arrowCokernelFGObj a)

Every Butler--Ringel arrow cokernel V(a) is uniserial: its radical has at most the one incoming branch different from a, and its top is simple.