Magnitude conjecture

MagnitudeConjecture.Algebra.StringProjectiveExplicitPathBasis

An explicit path-element basis of a represented string projective #

source
noncomputable def MagnitudeConjecture.BoundQuiver.StringPresentation.representedVertexExplicitPathBasis {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.VertexPath y) k ↑(P.representedVertexModule y)

The represented projective path basis rebuilt with the explicit matrix-supported path elements as its definitional coefficient family.

Instances For
    source
    @[simp]
    theorem MagnitudeConjecture.BoundQuiver.StringPresentation.representedVertexExplicitPathBasis_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) (p : P.VertexPath y) :
    (P.representedVertexExplicitPathBasis y) p = P.representedPathElement y p