Irreducible morphisms into string-arrow cokernels

For a displayed arrow a : x ⟶ y, its range is one direct summand of the radical of the represented projective P(y). Projection away from this summand gives a canonical linear section from the radical of V(a) back to the radical of P(y). Consequently every proper monomorphism into V(a) lifts through its projective cover. An irreducible monomorphism would then split on the left; indecomposability of P(y) forces the lift either to vanish or to split on the right, and both alternatives are impossible.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.arrowIrreducibleAlgebraFiniteDimensional {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.arrowIrreducibleAlgebraOppositeIsNoetherian {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.not_mono_of_isIrreducibleMorphism_to_arrowCokernel {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) {X : FGModuleCat P.quotientCategoryAlgebraᵐᵒᵖ} [Nontrivial ↑X] (f : X ⟶ P.arrowCokernelFGObj a) (hf : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism f) : ¬CategoryTheory.Mono f

No irreducible morphism from a nonzero finite module into V(a) can be monic. The complement of the killed branch lifts the whole radical of V(a) back to its indecomposable projective cover.