The surviving incoming-arrow family of an arrow cokernel

noncomputable def MagnitudeConjecture.BoundQuiver.StringPresentation.incomingArrowRangeFamilySingle {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} (a : DisplayedIncomingArrow y) (z : ↥(P.representedArrowLinearMap a.snd).range) (b : DisplayedIncomingArrow y) : ↥(P.representedArrowLinearMap b.snd).range

A vector in one incoming-arrow range, inserted in the corresponding coordinate of the full branch family.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.incomingArrowRangeFamilyRadicalLinearEquiv_symm_branchInclusion {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} (a : DisplayedIncomingArrow y) (z : ↥(P.representedArrowLinearMap a.snd).range) : (P.incomingArrowRangeFamilyRadicalLinearEquiv y).symm ((P.arrowBranchRadicalInclusionLinearMap a) z) = P.incomingArrowRangeFamilySingle a z

The selected branch inclusion is the corresponding single-coordinate vector under the radical decomposition.

noncomputable def MagnitudeConjecture.BoundQuiver.StringPresentation.otherIncomingFamilyToCokernelRadical {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) : ((b : OtherIncomingArrow ⟨x, a⟩) → ↥(P.representedArrowLinearMap (↑b).snd).range) →ₗ[P.quotientCategoryAlgebraᵐᵒᵖ] ↥(Module.jacobson P.quotientCategoryAlgebraᵐᵒᵖ ↑(P.arrowCokernelFGObj a))

Deleting the selected coordinate and then passing to the arrow cokernel identifies the remaining branch family with the radical of V(a).