Path weights in a Quiver

This file defines the weight of a path in a quiver. The weight of a path is the product of the weights of its edges, where weights are taken from a monoid.

Main definitions

• Quiver.Path.weight: The weight of a path, defined as the multiplicative product of the weights of its constituent edges.
• Quiver.Path.weightOfEPs: A convenience version of weight where the weight of an edge is determined by a function of its source and target vertices.

Main results

• Quiver.Path.weight_comp: The weight of a composition of paths is the product of their weights.
• Quiver.Path.weight_pos: If all edge weights are positive, the path weight is positive.
• Quiver.Path.weightOfEPs_nonneg: If all edge weights are non-negative, so is the path weight.

@[irreducible]

def Quiver.Path.weight {V : Type u_1} [Quiver V] {R : Type u_2} [Monoid R] (w : {i j : V} → (i ⟶ j) → R) {i j : V} : Path i j → R

The weight of a path is the product of the weights of its edges.

@[irreducible]

def Quiver.Path.addWeight {V : Type u_1} [Quiver V] {R : Type u_3} [AddMonoid R] (w : {i j : V} → (i ⟶ j) → R) {i j : V} : Path i j → R

The additive weight of a path is the sum of the weights of its edges.

def Quiver.Path.weightOfEPs {V : Type u_1} [Quiver V] {R : Type u_2} [Monoid R] (w : V → V → R) {i j : V} : Path i j → R

The weight of a path, where the weight of an edge is defined by a function on its endpoints.

def Quiver.Path.addWeightOfEPs {V : Type u_1} [Quiver V] {R : Type u_2} [AddMonoid R] (w : V → V → R) {i j : V} : Path i j → R

The additive weight of a path, where the weight of an edge is defined by a function on its endpoints.

@[simp]

theorem Quiver.Path.weight_nil {V : Type u_1} [Quiver V] {R : Type u_2} [Monoid R] (w : {i j : V} → (i ⟶ j) → R) (a : V) : weight (fun {i j : V} => w) nil = 1

@[simp]

theorem Quiver.Path.addWeight_nil {V : Type u_1} [Quiver V] {R : Type u_2} [AddMonoid R] (w : {i j : V} → (i ⟶ j) → R) (a : V) : addWeight (fun {i j : V} => w) nil = 0

@[simp]

theorem Quiver.Path.weight_cons {V : Type u_1} [Quiver V] {R : Type u_2} [Monoid R] (w : {i j : V} → (i ⟶ j) → R) {a b c : V} (p : Path a b) (e : b ⟶ c) : weight (fun {i j : V} => w) (p.cons e) = weight (fun {i j : V} => w) p * w e

@[simp]

theorem Quiver.Path.addWeight_cons {V : Type u_1} [Quiver V] {R : Type u_2} [AddMonoid R] (w : {i j : V} → (i ⟶ j) → R) {a b c : V} (p : Path a b) (e : b ⟶ c) : addWeight (fun {i j : V} => w) (p.cons e) = addWeight (fun {i j : V} => w) p + w e

theorem Quiver.Path.weightOfEPs_nil {V : Type u_1} [Quiver V] {R : Type u_2} [Monoid R] (w : V → V → R) (a : V) : weightOfEPs w nil = 1

theorem Quiver.Path.addWeightOfEPs_nil {V : Type u_1} [Quiver V] {R : Type u_2} [AddMonoid R] (w : V → V → R) (a : V) : addWeightOfEPs w nil = 0

theorem Quiver.Path.weightOfEPs_cons {V : Type u_1} [Quiver V] {R : Type u_2} [Monoid R] (w : V → V → R) {a b c : V} (p : Path a b) (e : b ⟶ c) : weightOfEPs w (p.cons e) = weightOfEPs w p * w b c

theorem Quiver.Path.addWeightOfEPs_cons {V : Type u_1} [Quiver V] {R : Type u_2} [AddMonoid R] (w : V → V → R) {a b c : V} (p : Path a b) (e : b ⟶ c) : addWeightOfEPs w (p.cons e) = addWeightOfEPs w p + w b c

@[simp]

theorem Quiver.Path.weight_comp {V : Type u_1} [Quiver V] {R : Type u_2} [Monoid R] (w : {i j : V} → (i ⟶ j) → R) {a b c : V} (p : Path a b) (q : Path b c) : weight (fun {i j : V} => w) (p.comp q) = weight (fun {i j : V} => w) p * weight (fun {i j : V} => w) q

@[simp]

theorem Quiver.Path.addWeight_comp {V : Type u_1} [Quiver V] {R : Type u_2} [AddMonoid R] (w : {i j : V} → (i ⟶ j) → R) {a b c : V} (p : Path a b) (q : Path b c) : addWeight (fun {i j : V} => w) (p.comp q) = addWeight (fun {i j : V} => w) p + addWeight (fun {i j : V} => w) q

theorem Quiver.Path.weightOfEPs_comp {V : Type u_1} [Quiver V] {R : Type u_2} [Monoid R] (w : V → V → R) {a b c : V} (p : Path a b) (q : Path b c) : weightOfEPs w (p.comp q) = weightOfEPs w p * weightOfEPs w q

theorem Quiver.Path.addWeightOfEPs_comp {V : Type u_1} [Quiver V] {R : Type u_2} [AddMonoid R] (w : V → V → R) {a b c : V} (p : Path a b) (q : Path b c) : addWeightOfEPs w (p.comp q) = addWeightOfEPs w p + addWeightOfEPs w q

theorem Quiver.Path.weight_pos {V : Type u_1} [Quiver V] {R : Type u_2} [Semiring R] [LinearOrder R] [IsStrictOrderedRing R] {w : {i j : V} → (i ⟶ j) → R} (hw : ∀ {i j : V} (e : i ⟶ j), 0 < w e) {i j : V} (p : Path i j) : 0 < weight (fun {i j : V} => w) p

If all edge weights are positive, then the weight of any path is positive.

theorem Quiver.Path.weight_nonneg {V : Type u_1} [Quiver V] {R : Type u_2} [Semiring R] [LinearOrder R] [IsStrictOrderedRing R] {w : {i j : V} → (i ⟶ j) → R} (hw : ∀ {i j : V} (e : i ⟶ j), 0 ≤ w e) {i j : V} (p : Path i j) : 0 ≤ weight (fun {i j : V} => w) p

If all edge weights are non-negative, then the weight of any path is non-negative.

theorem Quiver.Path.weightOfEPs_pos {V : Type u_1} [Quiver V] {R : Type u_2} [Semiring R] [LinearOrder R] [IsStrictOrderedRing R] {w : V → V → R} (hw : ∀ (i j : V), 0 < w i j) {i j : V} (p : Path i j) : 0 < weightOfEPs w p

If all edge weights (given by a function on vertices) are positive, so is the path weight.

theorem Quiver.Path.weightOfEPs_nonneg {V : Type u_1} [Quiver V] {R : Type u_2} [Semiring R] [LinearOrder R] [IsStrictOrderedRing R] {w : V → V → R} (hw : ∀ (i j : V), 0 ≤ w i j) {i j : V} (p : Path i j) : 0 ≤ weightOfEPs w p

If all edge weights (given by a function on vertices) are non-negative, so is the path weight.