Images of incoming-arrow product-basis vectors #
Reindexing the incoming-arrow product basis by positive surviving paths keeps the image calculation out of the nested arrow/continuation sigma type.
theorem
MagnitudeConjecture.BoundQuiver.StringPresentation.incomingArrowRangeSumKLinearMap_positiveVector
{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)
(q : P.PositiveVertexPath y)
:
(P.incomingArrowRangeSumKLinearMap y) (P.positiveIncomingVector y q) = P.representedPathElement y ↑q
The incoming-range sum sends the vector belonging to a positive path to the corresponding represented path element.
theorem
MagnitudeConjecture.BoundQuiver.StringPresentation.incomingArrowRangeSumKLinearMap_positiveBasis
{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)
(q : P.PositiveVertexPath y)
:
(P.incomingArrowRangeSumKLinearMap y) ((P.incomingArrowRangePositiveBasis y) q) = (P.representedVertexExplicitPathBasis y) ↑q
The positive-path basis is carried to the corresponding subfamily of the explicit represented-projective path basis.