Incoming-arrow sums in represented string projectives

The explicit path-basis calculation proves that the sum of the incoming-arrow ranges is internal.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.incomingArrowRangeSumLinearMap_injective {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) : Function.Injective ⇑(P.incomingArrowRangeSumLinearMap y)

The represented incoming-arrow ranges form an internal direct sum.