Alternating vertex functions

A function from the vertices of a quiver to a monoid with distributive negation alternates when it is negated by every arrow, c j = -c i for all a : i ⟶ j. This file records what such a function does along a path: it is multiplied by (-1)ⁿ over a path of length n, so it is unchanged along a path of even length and negated along one of odd length.

In particular, a closed walk of odd length forces an alternating function to satisfy c a = -c a. When the values lie in a ring, this gives 2 * c a = 0.

Main results

• TauCeti.eq_neg_one_pow_mul_of_path: an alternating vertex function changes by (-1)ⁿ along a path of length n.

theorem TauCeti.eq_neg_one_pow_mul_of_path {V : Type u} [Quiver V] (k : Type u_1) [Monoid k] [HasDistribNeg k] {c : V → k} (hc : ∀ ⦃i j : V⦄ (a : i ⟶ j), c j = -c i) {a b : V} (p : Quiver.Path a b) : c b = (-1) ^ p.length * c a

A sign-changing vertex function changes by (-1)ⁿ along a path. If c negates along every arrow of a quiver, then it is multiplied by (-1)ⁿ along every path of length n.