mathlib documentation

combinatorics.quiver.path

Paths in quivers #

Given a quiver V, we define the type of paths from a : V to b : V as an inductive family. We define composition of paths and the action of prefunctors on paths.

inductive quiver.path {V : Type u} [quiver V] (a : V) :
V → Sort (max (u+1) v)

G.path a b is the type of paths from a to b through the arrows of G.

Instances for quiver.path
def quiver.hom.to_path {V : Type u_1} [quiver V] {a b : V} (e : a b) :

An arrow viewed as a path of length one.

Equations
def quiver.path.length {V : Type u} [quiver V] {a b : V} :

The length of a path is the number of arrows it uses.

Equations
@[protected, instance]
def quiver.path.inhabited {V : Type u} [quiver V] {a : V} :
Equations
@[simp]
theorem quiver.path.length_nil {V : Type u} [quiver V] {a : V} :
@[simp]
theorem quiver.path.length_cons {V : Type u} [quiver V] (a b c : V) (p : quiver.path a b) (e : b c) :
(p.cons e).length = p.length + 1
def quiver.path.comp {V : Type u} [quiver V] {a b c : V} :
quiver.path a bquiver.path b cquiver.path a c

Composition of paths.

Equations
@[simp]
theorem quiver.path.comp_cons {V : Type u} [quiver V] {a b c d : V} (p : quiver.path a b) (q : quiver.path b c) (e : c d) :
p.comp (q.cons e) = (p.comp q).cons e
@[simp]
theorem quiver.path.comp_nil {V : Type u} [quiver V] {a b : V} (p : quiver.path a b) :
@[simp]
theorem quiver.path.nil_comp {V : Type u} [quiver V] {a b : V} (p : quiver.path a b) :
@[simp]
theorem quiver.path.comp_assoc {V : Type u} [quiver V] {a b c d : V} (p : quiver.path a b) (q : quiver.path b c) (r : quiver.path c d) :
(p.comp q).comp r = p.comp (q.comp r)
def prefunctor.map_path {V : Type u₁} [quiver V] {W : Type u₂} [quiver W] (F : prefunctor V W) {a b : V} :
quiver.path a bquiver.path (F.obj a) (F.obj b)

The image of a path under a prefunctor.

Equations
@[simp]
theorem prefunctor.map_path_nil {V : Type u₁} [quiver V] {W : Type u₂} [quiver W] (F : prefunctor V W) (a : V) :
@[simp]
theorem prefunctor.map_path_cons {V : Type u₁} [quiver V] {W : Type u₂} [quiver W] (F : prefunctor V W) {a b c : V} (p : quiver.path a b) (e : b c) :
F.map_path (p.cons e) = (F.map_path p).cons (F.map e)
@[simp]
theorem prefunctor.map_path_comp {V : Type u₁} [quiver V] {W : Type u₂} [quiver W] (F : prefunctor V W) {a b : V} (p : quiver.path a b) {c : V} (q : quiver.path b c) :
F.map_path (p.comp q) = (F.map_path p).comp (F.map_path q)