Single-coordinate vectors for incoming-arrow sums

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

@[instance_reducible]

noncomputable def MagnitudeConjecture.BoundQuiver.StringPresentation.displayedIncomingArrowDecidableEq {Q : Type u} [Quiver Q] (y : Q) : DecidableEq (DisplayedIncomingArrow y)

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

Insert one incoming-arrow range element in its coordinate of the finite dependent product.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.incomingArrowRangeSumKLinearMap_single {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) (g : ↥(P.representedArrowLinearMap a.snd).range) : (P.incomingArrowRangeSumKLinearMap y) (P.incomingArrowRangeSingle y a g) = ↑g

The incoming-range sum sends a vector supported in one arrow coordinate to that coordinate's underlying represented morphism.