Identifying the surviving branch family with the cokernel radical #
noncomputable def
MagnitudeConjecture.BoundQuiver.StringPresentation.otherIncomingFamilyCokernelRadicalLinearEquiv
{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))
The radical of V(a) is linearly equivalent to the family of all
incoming-arrow ranges other than the range generated by a.