Pure-string classification of arrow cokernels

Every Butler--Ringel arrow cokernel is uniserial. Pulling its selected algebra-skeleton representative back through the finite-category projective-generator equivalence and then through coefficient duality shows that its literal classified string is uniserial as well. The mixed-sign obstruction therefore forces that word to be purely positive or purely negative.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.arrowPureAlgebraFiniteDimensional {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) : FiniteDimensional k P.quotientCategoryAlgebra

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.arrowPureAlgebraOppositeNoetherian {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) : IsNoetherianRing P.quotientCategoryAlgebraᵐᵒᵖ

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.arrowCokernelClassifiedWord_isPure {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) (S : P.ArrowPolarization) (T : RightModule.FiniteIndecomposableSkeleton k P.quotientCategoryAlgebra) {x y : Q} (a : x ⟶ y) : have i := P.arrowCokernelSkeletonIndex T a; have C := (P.algebraSkeletonDetectorIndex S T i).endpointWord.word; StringWord.Word.IsPurePositive ⋯ C ∨ StringWord.Word.IsPureNegative ⋯ C

The literal string selected by a complete algebra-module skeleton for an arrow cokernel has only one sign.