# 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.

source
inductive Quiver.Path {V : Type u} [Quiver V] (a : V) :
V → Sort (max (u + 1) v)

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

- nil {V : Type u} [Quiver V] {a : V} : Path a a
- cons {V : Type u} [Quiver V] {a b c : V} : Path a b → (b ⟶ c) → Path a c

Instances For

source
def Quiver.Hom.toPath {V : Type u_1} [Quiver V] {a b : V} (e : a ⟶ b) :
Path a b

An arrow viewed as a path of length one.

Equations

- e.toPath = Quiver.Path.nil.cons e

Instances For

source
theorem Quiver.Path.nil_ne_cons {V : Type u} [Quiver V] {a b : V} (p : Path a b) (e : b ⟶ a) :
nil ≠ p.cons e
source
theorem Quiver.Path.cons_ne_nil {V : Type u} [Quiver V] {a b : V} (p : Path a b) (e : b ⟶ a) :
p.cons e ≠ nil
source
theorem Quiver.Path.obj_eq_of_cons_eq_cons {V : Type u} [Quiver V] {a b c d : V} {p : Path a b} {p' : Path a c} {e : b ⟶ d} {e' : c ⟶ d} (h : p.cons e = p'.cons e') :
b = c
source
theorem Quiver.Path.heq_of_cons_eq_cons {V : Type u} [Quiver V] {a b c d : V} {p : Path a b} {p' : Path a c} {e : b ⟶ d} {e' : c ⟶ d} (h : p.cons e = p'.cons e') :
p ≍ p'
source
theorem Quiver.Path.hom_heq_of_cons_eq_cons {V : Type u} [Quiver V] {a b c d : V} {p : Path a b} {p' : Path a c} {e : b ⟶ d} {e' : c ⟶ d} (h : p.cons e = p'.cons e') :
e ≍ e'
source
def Quiver.Path.length {V : Type u} [Quiver V] {a b : V} :
Path a b → ℕ

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

Equations

- Quiver.Path.nil.length = 0
- (p.cons a_1).length = p.length + 1

Instances For

source
instance Quiver.Path.instInhabited {V : Type u} [Quiver V] {a : V} :
Inhabited (Path a a)
Equations

- Quiver.Path.instInhabited = { default := Quiver.Path.nil }

source
@[simp]
theorem Quiver.Path.length_nil {V : Type u} [Quiver V] {a : V} :
nil.length = 0
source
@[simp]
theorem Quiver.Path.length_cons {V : Type u} [Quiver V] (a b c : V) (p : Path a b) (e : b ⟶ c) :
(p.cons e).length = p.length + 1
source
theorem Quiver.Path.eq_of_length_zero {V : Type u} [Quiver V] {a b : V} (p : Path a b) (hzero : p.length = 0) :
a = b
source
theorem Quiver.Path.eq_nil_of_length_zero {V : Type u} [Quiver V] {a : V} (p : Path a a) (hzero : p.length = 0) :
p = nil
source
@[simp]
theorem Quiver.Path.length_toPath {V : Type u} [Quiver V] {a b : V} (e : a ⟶ b) :
e.toPath.length = 1
source
def Quiver.Path.comp {V : Type u} [Quiver V] {a b c : V} :
Path a b → Path b c → Path a c

Composition of paths.

Equations

- x✝.comp Quiver.Path.nil = x✝
- x✝.comp (q.cons e) = (x✝.comp q).cons e

Instances For

source
@[simp]
theorem Quiver.Path.comp_cons {V : Type u} [Quiver V] {a b c d : V} (p : Path a b) (q : Path b c) (e : c ⟶ d) :
p.comp (q.cons e) = (p.comp q).cons e
source
@[simp]
theorem Quiver.Path.comp_nil {V : Type u} [Quiver V] {a b : V} (p : Path a b) :
p.comp nil = p
source
@[simp]
theorem Quiver.Path.nil_comp {V : Type u} [Quiver V] {a b : V} (p : Path a b) :
nil.comp p = p
source
@[simp]
theorem Quiver.Path.comp_assoc {V : Type u} [Quiver V] {a b c d : V} (p : Path a b) (q : Path b c) (r : Path c d) :
(p.comp q).comp r = p.comp (q.comp r)
source
@[simp]
theorem Quiver.Path.length_comp {V : Type u} [Quiver V] {a b : V} (p : Path a b) {c : V} (q : Path b c) :
(p.comp q).length = p.length + q.length
source
theorem Quiver.Path.comp_inj {V : Type u} [Quiver V] {a b c : V} {p₁ p₂ : Path a b} {q₁ q₂ : Path b c} (hq : q₁.length = q₂.length) :
p₁.comp q₁ = p₂.comp q₂ ↔ p₁ = p₂ ∧ q₁ = q₂
source
theorem Quiver.Path.comp_inj' {V : Type u} [Quiver V] {a b c : V} {p₁ p₂ : Path a b} {q₁ q₂ : Path b c} (h : p₁.length = p₂.length) :
p₁.comp q₁ = p₂.comp q₂ ↔ p₁ = p₂ ∧ q₁ = q₂
source
theorem Quiver.Path.comp_injective_left {V : Type u} [Quiver V] {a b c : V} (q : Path b c) :
Function.Injective fun (p : Path a b) => p.comp q
source
theorem Quiver.Path.comp_injective_right {V : Type u} [Quiver V] {a b c : V} (p : Path a b) :
Function.Injective p.comp
source
@[simp]
theorem Quiver.Path.comp_inj_left {V : Type u} [Quiver V] {a b c : V} {p₁ p₂ : Path a b} {q : Path b c} :
p₁.comp q = p₂.comp q ↔ p₁ = p₂
source
@[simp]
theorem Quiver.Path.comp_inj_right {V : Type u} [Quiver V] {a b c : V} {p : Path a b} {q₁ q₂ : Path b c} :
p.comp q₁ = p.comp q₂ ↔ q₁ = q₂
source
theorem Quiver.Path.eq_toPath_comp_of_length_eq_succ {V : Type u} [Quiver V] {a b : V} (p : Path a b) {n : ℕ} (hp : p.length = n + 1) :
∃ (c : V), ∃ (f : a ⟶ c), ∃ (q : Path c b), ∃ (x : q.length = n), p = f.toPath.comp q
source
theorem Quiver.Path.length_ne_zero_iff_eq_comp {V : Type u_1} [Quiver V] {a b : V} (p : Path a b) :
p.length ≠ 0 ↔ ∃ (c : V), ∃ (e : a ⟶ c), ∃ (p' : Path c b), p = e.toPath.comp p' ∧ p.length = p'.length + 1
source
theorem Quiver.Path.length_ne_zero_iff_eq_cons {V : Type u_1} [Quiver V] {a b : V} (p : Path a b) :
p.length ≠ 0 ↔ ∃ (c : V), ∃ (p' : Path a c), ∃ (e : c ⟶ b), p = p'.cons e

Every non-empty path can be decomposed as an initial path plus a final edge.

source
@[simp]
theorem Quiver.Path.comp_toPath_eq_cons {V : Type u_1} [Quiver V] {a b c : V} (p : Path a b) (e : b ⟶ c) :
p.comp e.toPath = p.cons e
source
def Quiver.Path.toList {V : Type u} [Quiver V] {a b : V} :
Path a b → List V

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

Equations

- Quiver.Path.nil.toList = []
- (p.cons a_1).toList = b :: p.toList

Instances For

source
@[simp]
theorem Quiver.Path.toList_comp {V : Type u} [Quiver V] {a b : V} (p : Path a b) {c : V} (q : Path b c) :
(p.comp q).toList = q.toList ++ p.toList

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

source
theorem Quiver.Path.isChain_toList_nonempty {V : Type u} [Quiver V] {a b : V} (p : Path a b) :
List.IsChain (fun (x y : V) => Nonempty (y ⟶ x)) p.toList
source
theorem Quiver.Path.isChain_cons_toList_nonempty {V : Type u} [Quiver V] {a b : V} (p : Path a b) :
List.IsChain (fun (x y : V) => Nonempty (y ⟶ x)) (b :: p.toList)
source
@[deprecated Quiver.Path.isChain_cons_toList_nonempty (since := "2025-09-19")]
theorem Quiver.Path.toList_chain_nonempty {V : Type u} [Quiver V] {a b : V} (p : Path a b) :
List.IsChain (fun (x y : V) => Nonempty (y ⟶ x)) (b :: p.toList)

Alias of `Quiver.Path.isChain_cons_toList_nonempty`.

source
theorem Quiver.Path.toList_injective {V : Type u} [Quiver V] [∀ (a b : V), Subsingleton (a ⟶ b)] (a b : V) :
Function.Injective toList
source
@[simp]
theorem Quiver.Path.toList_inj {V : Type u} [Quiver V] {a b : V} [∀ (a b : V), Subsingleton (a ⟶ b)] {p q : Path a b} :
p.toList = q.toList ↔ p = q
source
def Quiver.Path.BoundedPaths {V : Type u_1} [Quiver V] (v w : V) (n : ℕ) :
Sort (max 1 (u_1 + 1) u_2)

A bounded path is a path with a uniform bound on its length.

Equations

- Quiver.Path.BoundedPaths v w n = { p : Quiver.Path v w // p.length ≤ n }

Instances For

source
instance Quiver.Path.instSubsingletonBddPaths {V : Type u_1} [Quiver V] (v w : V) :
Subsingleton (BoundedPaths v w 0)

Bounded paths of length zero between two vertices form a subsingleton.

source
def Quiver.Path.decidableEqBddPathsZero {V : Type u_1} [Quiver V] (v w : V) :
DecidableEq (BoundedPaths v w 0)

Bounded paths of length zero between two vertices have decidable equality.

Equations

- Quiver.Path.decidableEqBddPathsZero v w x✝¹ x✝ = isTrue ⋯

Instances For

source
def Quiver.Path.decidableEqBddPathsOfDecidableEq {V : Type u_1} [Quiver V] (n : ℕ) (h₁ : DecidableEq V) (h₂ : (v w : V) → DecidableEq (v ⟶ w)) (h₃ : (v w : V) → DecidableEq (BoundedPaths v w n)) (v w : V) :
DecidableEq (BoundedPaths v w (n + 1))

Given decidable equality on paths of length up to `n`, we can construct decidable equality on paths of length up to `n + 1`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
instance Quiver.Path.decidableEqBoundedPaths {V : Type u_1} [Quiver V] [DecidableEq V] [(v w : V) → DecidableEq (v ⟶ w)] (n : ℕ) (v w : V) :
DecidableEq (BoundedPaths v w n)

Equality is decidable on all uniformly bounded paths given decidable equality on the vertices and the arrows.

Equations

- One or more equations did not get rendered due to their size.

source
instance Quiver.Path.instDecidableEq {V : Type u_1} [Quiver V] [DecidableEq V] [(v w : V) → DecidableEq (v ⟶ w)] (v w : V) :
DecidableEq (Path v w)

Equality is decidable on paths in a quiver given decidable equality on the vertices and arrows.

Equations

- Quiver.Path.instDecidableEq v w p q = decidable_of_iff (⟨p, ⋯⟩ = ⟨q, ⋯⟩) ⋯

source
def Prefunctor.mapPath {V : Type u₁} [Quiver V] {W : Type u₂} [Quiver W] (F : V ⥤q W) {a b : V} :
Quiver.Path a b → Quiver.Path (F.obj a) (F.obj b)

The image of a path under a prefunctor.

Equations

- F.mapPath Quiver.Path.nil = Quiver.Path.nil
- F.mapPath (p.cons a_1) = (F.mapPath p).cons (F.map a_1)

Instances For

source
@[simp]
theorem Prefunctor.mapPath_nil {V : Type u₁} [Quiver V] {W : Type u₂} [Quiver W] (F : V ⥤q W) (a : V) :
F.mapPath Quiver.Path.nil = Quiver.Path.nil
source
@[simp]
theorem Prefunctor.mapPath_cons {V : Type u₁} [Quiver V] {W : Type u₂} [Quiver W] (F : V ⥤q W) {a b c : V} (p : Quiver.Path a b) (e : b ⟶ c) :
F.mapPath (p.cons e) = (F.mapPath p).cons (F.map e)
source
@[simp]
theorem Prefunctor.mapPath_comp {V : Type u₁} [Quiver V] {W : Type u₂} [Quiver W] (F : V ⥤q W) {a b : V} (p : Quiver.Path a b) {c : V} (q : Quiver.Path b c) :
F.mapPath (p.comp q) = (F.mapPath p).comp (F.mapPath q)
source
@[simp]
theorem Prefunctor.mapPath_toPath {V : Type u₁} [Quiver V] {W : Type u₂} [Quiver W] (F : V ⥤q W) {a b : V} (f : a ⟶ b) :
F.mapPath f.toPath = (F.map f).toPath
source
@[simp]
theorem Prefunctor.mapPath_id {V : Type u₁} [Quiver V] {a b : V} (p : Quiver.Path a b) :
(𝟭q V).mapPath p = p
source
@[simp]
theorem Prefunctor.mapPath_comp_apply {V : Type u₁} [Quiver V] {W : Type u₂} [Quiver W] (F : V ⥤q W) {U : Type u₃} [Quiver U] (G : W ⥤q U) {a b : V} (p : Quiver.Path a b) :
(F ⋙q G).mapPath p = G.mapPath (F.mapPath p)