Evaluating an arrow-branch coordinate in the projective radical

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.incomingArrowRangeFamilyRadicalLinearEquiv_single_coe {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) {y : Q} [DecidableEq (DisplayedIncomingArrow y)] (a : DisplayedIncomingArrow y) (z : ↥(P.representedArrowLinearMap a.snd).range) : ↑((P.incomingArrowRangeFamilyRadicalLinearEquiv y) ((LinearMap.single P.quotientCategoryAlgebraᵐᵒᵖ (fun (b : DisplayedIncomingArrow y) => ↥(P.representedArrowLinearMap b.snd).range) a) z)) = ↑z

The radical decomposition includes a single arrow coordinate by its ambient submodule inclusion.