The global range of a represented string-arrow map #
The represented arrow range is identified with the product of its vertexwise left-composition ranges.
noncomputable def
MagnitudeConjecture.BoundQuiver.StringPresentation.representedArrowRangeCoordinateLinearEquiv
{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)
:
↥(P.representedArrowKLinearMap a).range ≃ₗ[k] (X : Category P.relations) → ↥(P.leftArrowCompositionLinearMapObj a X).range
The global represented arrow range is the product of its vertexwise left-composition ranges.