An explicit positive-path basis for the incoming-arrow product

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

The single-coordinate continuation vector belonging to a positive path.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.positiveIncomingVector_equiv_apply {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) (t : (a : DisplayedIncomingArrow y) × P.LeftContinuationPath a.snd) : P.positiveIncomingVector y ((P.incomingContinuationEquivPositiveVertexPath y) t) = piBasisVector (P.incomingArrowModuleBasisFamily y) t

After a positive path is presented by its final arrow and continuation, its named vector is the corresponding product-basis vector.

noncomputable def MagnitudeConjecture.BoundQuiver.StringPresentation.incomingArrowRangePositiveRawBasis {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) : Module.Basis (P.PositiveVertexPath y) k ((a : DisplayedIncomingArrow y) → ↥(P.representedArrowLinearMap a.snd).range)

The incoming-arrow product basis reindexed by positive paths.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.incomingArrowRangePositiveRawBasis_apply {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.incomingArrowRangePositiveRawBasis y) q = P.positiveIncomingVector y q

The raw reindexed product basis has the named positive-path vector as its value.

noncomputable def MagnitudeConjecture.BoundQuiver.StringPresentation.incomingArrowRangePositiveBasis {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) : Module.Basis (P.PositiveVertexPath y) k ((a : DisplayedIncomingArrow y) → ↥(P.representedArrowLinearMap a.snd).range)

A positive-path-indexed basis whose coefficient function is definitionally the named positive incoming vector.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.incomingArrowRangePositiveBasis_apply {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.incomingArrowRangePositiveBasis y) q = P.positiveIncomingVector y q