# Documentation

Mathlib.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} [inst : ] (a : V) :
VSort (max(u+1)v)
• nil: {V : Type u} → [inst : ] → {a : V} →
• cons: {V : Type u} → [inst : ] → {a b c : V} → (b c) →

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

Instances For
def Quiver.Path.recC {V : Type t} [inst : ] {a : V} {motive : (b : V) → Sort w} (nil : motive a Quiver.Path.nil) (cons : {b c : V} → (p : ) → (e : b c) → motive b pmotive c ()) {b : V} (p : ) :
motive b p

A computable version of Quiver.Path.rec. Workaround until Lean has native support for this.

Equations
@[csimp]
def Quiver.Hom.toPath {V : Type u_1} [inst : ] {a : V} {b : V} (e : a b) :

An arrow viewed as a path of length one.

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

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

Equations
instance Quiver.Path.instInhabitedPath {V : Type u} [inst : ] {a : V} :
Equations
• Quiver.Path.instInhabitedPath = { default := Quiver.Path.nil }
@[simp]
theorem Quiver.Path.length_nil {V : Type u} [inst : ] {a : V} :
Quiver.Path.length Quiver.Path.nil = 0
@[simp]
theorem Quiver.Path.length_cons {V : Type u} [inst : ] (a : V) (b : V) (c : V) (p : ) (e : b c) :
theorem Quiver.Path.eq_of_length_zero {V : Type u} [inst : ] {a : V} {b : V} (p : ) (hzero : ) :
a = b
def Quiver.Path.comp {V : Type u} [inst : ] {a : V} {b : V} {c : V} :

Composition of paths.

Equations
@[simp]
theorem Quiver.Path.comp_cons {V : Type u} [inst : ] {a : V} {b : V} {c : V} {d : V} (p : ) (q : ) (e : c d) :
=
@[simp]
theorem Quiver.Path.comp_nil {V : Type u} [inst : ] {a : V} {b : V} (p : ) :
Quiver.Path.comp p Quiver.Path.nil = p
@[simp]
theorem Quiver.Path.nil_comp {V : Type u} [inst : ] {a : V} {b : V} (p : ) :
Quiver.Path.comp Quiver.Path.nil p = p
@[simp]
theorem Quiver.Path.comp_assoc {V : Type u} [inst : ] {a : V} {b : V} {c : V} {d : V} (p : ) (q : ) (r : ) :
=
@[simp]
theorem Quiver.Path.length_comp {V : Type u} [inst : ] {a : V} {b : V} (p : ) {c : V} (q : ) :
theorem Quiver.Path.comp_inj {V : Type u} [inst : ] {a : V} {b : V} {c : V} {p₁ : } {p₂ : } {q₁ : } {q₂ : } (hq : ) :
Quiver.Path.comp p₁ q₁ = Quiver.Path.comp p₂ q₂ p₁ = p₂ q₁ = q₂
theorem Quiver.Path.comp_inj' {V : Type u} [inst : ] {a : V} {b : V} {c : V} {p₁ : } {p₂ : } {q₁ : } {q₂ : } (h : ) :
Quiver.Path.comp p₁ q₁ = Quiver.Path.comp p₂ q₂ p₁ = p₂ q₁ = q₂
theorem Quiver.Path.comp_injective_left {V : Type u} [inst : ] {a : V} {b : V} {c : V} (q : ) :
theorem Quiver.Path.comp_injective_right {V : Type u} [inst : ] {a : V} {b : V} {c : V} (p : ) :
@[simp]
theorem Quiver.Path.comp_inj_left {V : Type u} [inst : ] {a : V} {b : V} {c : V} {p₁ : } {p₂ : } {q : } :
= p₁ = p₂
@[simp]
theorem Quiver.Path.comp_inj_right {V : Type u} [inst : ] {a : V} {b : V} {c : V} {p : } {q₁ : } {q₂ : } :
= q₁ = q₂
def Quiver.Path.toList {V : Type u} [inst : ] {a : V} {b : V} :
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.toList_comp {V : Type u} [inst : ] {a : V} {b : V} (p : ) {c : V} (q : ) :

Quiver.Path.toList is a contravariant functor. The inversion comes from Quiver.Path and List having different preferred directions for adding elements.

theorem Quiver.Path.toList_chain_nonempty {V : Type u} [inst : ] {a : V} {b : V} (p : ) :
List.Chain (fun x y => Nonempty (y x)) b ()
theorem Quiver.Path.toList_injective {V : Type u} [inst : ] [inst : ∀ (a b : V), Subsingleton (a b)] (a : V) (b : V) :
Function.Injective Quiver.Path.toList
@[simp]
theorem Quiver.Path.toList_inj {V : Type u} [inst : ] {a : V} {b : V} [inst : ∀ (a b : V), Subsingleton (a b)] {p : } {q : } :
p = q
def Prefunctor.mapPath {V : Type u₁} [inst : ] {W : Type u₂} [inst : ] (F : V ⥤q W) {a : V} {b : V} :
Quiver.Path () ()

The image of a path under a prefunctor.

Equations
@[simp]
theorem Prefunctor.mapPath_nil {V : Type u₁} [inst : ] {W : Type u₂} [inst : ] (F : V ⥤q W) (a : V) :
Prefunctor.mapPath F Quiver.Path.nil = Quiver.Path.nil
@[simp]
theorem Prefunctor.mapPath_cons {V : Type u₁} [inst : ] {W : Type u₂} [inst : ] (F : V ⥤q W) {a : V} {b : V} {c : V} (p : ) (e : b c) :
@[simp]
theorem Prefunctor.mapPath_comp {V : Type u₁} [inst : ] {W : Type u₂} [inst : ] (F : V ⥤q W) {a : V} {b : V} (p : ) {c : V} (q : ) :
@[simp]
theorem Prefunctor.mapPath_toPath {V : Type u₁} [inst : ] {W : Type u₂} [inst : ] (F : V ⥤q W) {a : V} {b : V} (f : a b) :