Additive path weights

Mathlib's Quiver.Path.addWeight w p sums the weights w e of the arrows along a path p. This file records its evaluation at a constant weight: a constant weight c sums to p.length • c. This identifies the path-length grading of a path algebra as the grading by the constant weight one. It also records that pushing a path along a prefunctor sums the pulled-back arrow weight.

Main results

• Quiver.Path.addWeight_const: the constant weight c gives a path the weight p.length • c.
• Prefunctor.addWeight_mapPath: the weight of a pushed path is the pulled-back weight of the original path.

@[simp]

theorem Quiver.Path.addWeight_const {V : Type u} [Quiver V] {M : Type u_1} [AddMonoid M] (c : M) {a b : V} (p : Path a b) : addWeight (fun {i j : V} (x : i ⟶ j) => c) p = p.length • c

A constant weight counts arrows: with every arrow of weight c, a path has weight p.length • c.

@[simp]

theorem Prefunctor.addWeight_mapPath {V : Type u} [Quiver V] {M : Type u_1} [AddMonoid M] {W : Type u_2} [Quiver W] (φ : V ⥤q W) (wt : {a b : W} → (a ⟶ b) → M) {a b : V} (p : Quiver.Path a b) : Quiver.Path.addWeight (fun {i j : W} => wt) (φ.mapPath p) = Quiver.Path.addWeight (fun {i j : V} (e : i ⟶ j) => wt (φ.map e)) p

Pushing a path pulls back its arrow weight: the weight of the image path is the sum of the image-arrow weights along the original path.