@[reducible, inline]

abbrev MagnitudeConjecture.BoundQuiver.StringPresentation.representedVertexCoordinateFamily {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 : Q) (X : Category P.relations) : Type u

The Hom-space family indexed by objects of the quotient path category.

@[reducible, inline]

abbrev MagnitudeConjecture.BoundQuiver.StringPresentation.representedVertexDisplayedCoordinateFamily {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 z : Q) : Type u

The same Hom-space family indexed by displayed quiver vertices.

noncomputable def MagnitudeConjecture.BoundQuiver.StringPresentation.representedVertexBiproductLinearEquiv {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 : Q) : P.representedVertexHom x ≃ₗ[k] (X : Category P.relations) → P.representedVertexCoordinateFamily x X

Restriction to biproduct summands gives the first stage of the displayed coordinates of a represented vertex module.