Path grading for numerical graph words #
For a finite simple graph with vertices labelled by natural numbers, every numerical
TauCeti.signlessArrow is homogeneous of degree one. Consequently, a valley word made from
these arrows is homogeneous in its word length. This packages the graph-word interface to the
path grading of the signless preprojective algebra. For an arbitrary simple graph, a product of
n backtracks at a common vertex has path degree 2 * n.
theorem
TauCeti.signlessArrow_mem_grade_one
(k : Type u)
[CommRing k]
{n : ℕ}
(G : SimpleGraph (Fin n))
[(i : Fin n) → Fintype ↑(G.neighborSet i)]
(i j : ℕ)
:
Every numerical graph arrow is homogeneous of degree one, including the zero returned for nonadjacent or out-of-range endpoints.
theorem
TauCeti.ladderValley_mem_grade
(k : Type u)
[CommRing k]
{n : ℕ}
(G : SimpleGraph (Fin n))
[(i : Fin n) → Fintype ↑(G.neighborSet i)]
(m s r : ℕ)
:
ladderValley (fun (w : ℕ) => signlessArrow k G w (w + 1)) (fun (w : ℕ) => signlessArrow k G (w + 1) w) m s r ∈ signlessPreprojectiveGrade k (DoubledQuiver G) (s + r)
A valley word of numerical graph arrows with s descents and r climbs is homogeneous of
degree s + r.
theorem
TauCeti.list_prod_signlessPreprojectiveMk_backtrackElem_mem_signlessPreprojectiveGrade
(k : Type u)
[CommRing k]
{V : Type u_1}
{G : SimpleGraph V}
[Fintype V]
[DecidableRel G.Adj]
{v : V}
(l : List { w : V // G.Adj v w })
:
(List.map
(fun (w : { w : V // G.Adj v w }) =>
(signlessPreprojectiveMk k (DoubledQuiver G)) (DoubledQuiver.backtrackElem G k ⋯))
l).prod ∈ signlessPreprojectiveGrade k (DoubledQuiver G) (2 * l.length)
A product of backtracks v → w → v at a common vertex v has path degree twice the number of
backtracks.