The canonical arrow-cokernel radical section on images

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.arrowCokernelRadicalSection_apply_map {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) (z : ↥(Module.jacobson P.quotientCategoryAlgebraᵐᵒᵖ ↑(P.representedVertexModule y))) : (P.arrowCokernelRadicalSection a) ((P.arrowCokernelRadicalLinearMap a) z) = (P.arrowRadicalComplementProjection a) z

Applying the canonical radical section to the image of a projective- radical vector discards exactly its selected-arrow coordinate.