Path bases of represented string projectives

For a displayed vertex of a string presentation, the nontrivial surviving paths ending at that vertex split uniquely according to their final quiver arrow. This file packages that path partition as the direct sum of the represented string-arrow modules inside the corresponding canonical projective.

@[instance_reducible]

noncomputable instance MagnitudeConjecture.BoundQuiver.StringPresentation.representedVertexModuleKModule {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 k ↑(P.representedVertexModule y)

instance MagnitudeConjecture.BoundQuiver.StringPresentation.representedVertexModuleIsScalarTower {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) : IsScalarTower k P.quotientCategoryAlgebraᵐᵒᵖ ↑(P.representedVertexModule y)

def MagnitudeConjecture.BoundQuiver.StringPresentation.representedVertexKLinearEquiv {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.representedVertexModule y) ≃ₗ[k] P.representedVertexHom y

The coefficient-field structure obtained by restricting the category- algebra action agrees with the native coefficient-field structure on the represented Hom space.

noncomputable def MagnitudeConjecture.BoundQuiver.StringPresentation.representedVertexPathCoordinateLinearEquiv {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.representedVertexModule y) ≃ₗ[k] (X : Category P.relations) → obj P.relations y ⟶ X

Vertex coordinates as a coefficient-field linear equivalence on the represented category-algebra module.

@[reducible, inline]

abbrev MagnitudeConjecture.BoundQuiver.StringPresentation.DisplayedIncomingArrow {Q : Type u} [Quiver Q] (y : Q) : Type u

Displayed quiver arrows ending at a fixed vertex.

@[reducible, inline]

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

All surviving paths ending at a fixed displayed vertex, with their starting vertex retained.

instance MagnitudeConjecture.BoundQuiver.StringPresentation.vertexPathFinite {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) : Finite (P.VertexPath y)

The surviving paths ending at a vertex form a finite type.

noncomputable def MagnitudeConjecture.BoundQuiver.StringPresentation.survivingPathBasisObj {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) (X : Category P.relations) : Module.Basis (SurvivingPath P.relations (P.quotientObjectEquiv X) y) k (obj P.relations y ⟶ X)

The monomial path basis in a coordinate indexed by an arbitrary object of the quotient path category.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.survivingPathBasisObj_obj {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 z : Q) : P.survivingPathBasisObj y (obj P.relations z) = survivingPathBasis P.relations ⋯ z y

noncomputable def MagnitudeConjecture.BoundQuiver.StringPresentation.vertexPathObjectSigmaEquiv {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) : (X : Category P.relations) × SurvivingPath P.relations (P.quotientObjectEquiv X) y ≃ P.VertexPath y

Reindex the small family of path-basis indices from quotient-category objects to displayed vertices.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.vertexPathObjectSigmaEquiv_symm_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.vertexPathObjectSigmaEquiv y).symm p = ⟨obj P.relations p.fst, p.snd⟩

noncomputable def MagnitudeConjecture.BoundQuiver.StringPresentation.representedVertexPathBasis {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)

Vertex coordinates and the monomial path bases give the global path basis of a represented canonical projective.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.representedVertexPathBasis_coordinate_self {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.representedVertexPathCoordinateLinearEquiv y) ((P.representedVertexPathBasis y) p) (obj P.relations p.fst) = (survivingPathBasis P.relations ⋯ p.fst y) p.snd

In its starting-object coordinate, a global path-basis vector is the corresponding pointwise monomial path-basis vector.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.representedVertexPathBasis_coordinate_ne {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) (z : Q) (hz : z ≠ p.fst) : (P.representedVertexPathCoordinateLinearEquiv y) ((P.representedVertexPathBasis y) p) (obj P.relations z) = 0

A global path-basis vector vanishes in every other displayed starting object coordinate.

noncomputable def MagnitudeConjecture.BoundQuiver.StringPresentation.representedPathElement {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.representedVertexModule y)

A surviving path, viewed as the corresponding matrix-supported vector in the represented canonical projective.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.representedPathElement_coordinate_self {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.representedVertexPathCoordinateLinearEquiv y) (P.representedPathElement y p) (obj P.relations p.fst) = pathMap P.relations ↑p.snd

At its starting vertex, a represented path element has its literal path coordinate.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.representedPathElement_coordinate_ne {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) (z : Q) (hz : z ≠ p.fst) : (P.representedVertexPathCoordinateLinearEquiv y) (P.representedPathElement y p) (obj P.relations z) = 0

A represented path element vanishes in every other starting-vertex coordinate.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.representedVertexPathBasis_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.representedVertexPathBasis y) p = P.representedPathElement y p

The global represented-projective path basis is the explicit matrix-supported path family.