# mathlib3documentation

combinatorics.quiver.path

# Paths in quivers #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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) :
b

An arrow viewed as a path of length one.

Equations
theorem quiver.path.nil_ne_cons {V : Type u} [quiver V] {a b : V} (p : b) (e : b a) :
theorem quiver.path.cons_ne_nil {V : Type u} [quiver V] {a b : V} (p : b) (e : b a) :
theorem quiver.path.obj_eq_of_cons_eq_cons {V : Type u} [quiver V] {a b c d : V} {p : b} {p' : c} {e : b d} {e' : c d} (h : p.cons e = p'.cons e') :
b = c
theorem quiver.path.heq_of_cons_eq_cons {V : Type u} [quiver V] {a b c d : V} {p : b} {p' : c} {e : b d} {e' : c d} (h : p.cons e = p'.cons e') :
p == p'
theorem quiver.path.hom_heq_of_cons_eq_cons {V : Type u} [quiver V] {a b c d : V} {p : b} {p' : c} {e : b d} {e' : c d} (h : p.cons e = p'.cons e') :
e == e'
def quiver.path.length {V : Type u} [quiver V] {a b : V} :
b

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 : b) (e : b c) :
(p.cons e).length = p.length + 1
theorem quiver.path.eq_of_length_zero {V : Type u} [quiver V] {a b : V} (p : b) (hzero : p.length = 0) :
a = b
def quiver.path.comp {V : Type u} [quiver V] {a b c : V} :
b c c

Composition of paths.

Equations
@[simp]
theorem quiver.path.comp_cons {V : Type u} [quiver V] {a b c d : V} (p : b) (q : 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 : b) :
@[simp]
theorem quiver.path.nil_comp {V : Type u} [quiver V] {a b : V} (p : b) :
@[simp]
theorem quiver.path.comp_assoc {V : Type u} [quiver V] {a b c d : V} (p : b) (q : c) (r : d) :
(p.comp q).comp r = p.comp (q.comp r)
@[simp]
theorem quiver.path.length_comp {V : Type u} [quiver V] {a b : V} (p : b) {c : V} (q : c) :
theorem quiver.path.comp_inj {V : Type u} [quiver V] {a b c : V} {p₁ p₂ : b} {q₁ q₂ : c} (hq : q₁.length = q₂.length) :
p₁.comp q₁ = p₂.comp q₂ p₁ = p₂ q₁ = q₂
theorem quiver.path.comp_inj' {V : Type u} [quiver V] {a b c : V} {p₁ p₂ : b} {q₁ q₂ : c} (h : p₁.length = p₂.length) :
p₁.comp q₁ = p₂.comp q₂ p₁ = p₂ q₁ = q₂
theorem quiver.path.comp_injective_left {V : Type u} [quiver V] {a b c : V} (q : c) :
function.injective (λ (p : b), p.comp q)
theorem quiver.path.comp_injective_right {V : Type u} [quiver V] {a b c : V} (p : b) :
@[simp]
theorem quiver.path.comp_inj_left {V : Type u} [quiver V] {a b c : V} {p₁ p₂ : b} {q : c} :
p₁.comp q = p₂.comp q p₁ = p₂
@[simp]
theorem quiver.path.comp_inj_right {V : Type u} [quiver V] {a b c : V} {p : b} {q₁ q₂ : c} :
p.comp q₁ = p.comp q₂ q₁ = q₂
@[simp]
def quiver.path.to_list {V : Type u} [quiver V] {a b : V} :
b list V

Turn a path into a list. The list contains a at its head, but not b a priori.

Equations
@[simp]
theorem quiver.path.to_list_comp {V : Type u} [quiver V] {a b : V} (p : b) {c : V} (q : c) :

quiver.path.to_list is a contravariant functor. The inversion comes from quiver.path and list having different preferred directions for adding elements.

theorem quiver.path.to_list_chain_nonempty {V : Type u} [quiver V] {a b : V} (p : b) :
list.chain (λ (x y : V), nonempty (y x)) b p.to_list
theorem quiver.path.to_list_injective {V : Type u} [quiver V] [ (a b : V), subsingleton (a b)] (a b : V) :
@[simp]
theorem quiver.path.to_list_inj {V : Type u} [quiver V] {a b : V} [ (a b : V), subsingleton (a b)] {p q : b} :
def prefunctor.map_path {V : Type u₁} [quiver V] {W : Type u₂} [quiver W] (F : V ⥤q W) {a b : V} :
b quiver.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 : V ⥤q W) (a : V) :
@[simp]
theorem prefunctor.map_path_cons {V : Type u₁} [quiver V] {W : Type u₂} [quiver W] (F : V ⥤q W) {a b c : V} (p : 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 : V ⥤q W) {a b : V} (p : b) {c : V} (q : c) :
F.map_path (p.comp q) = (F.map_path p).comp (F.map_path q)
@[simp]
theorem prefunctor.map_path_to_path {V : Type u₁} [quiver V] {W : Type u₂} [quiver W] (F : V ⥤q W) {a b : V} (f : a b) :