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)

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

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

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

An arrow viewed as a path of length one.

Equations

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

theorem Quiver.Path.nil_ne_cons {V : Type u} [Quiver V] {a : V} {b : V} (p : Quiver.Path a b) (e : b ⟶ a) : Quiver.Path.nil ≠ p.cons e

theorem Quiver.Path.cons_ne_nil {V : Type u} [Quiver V] {a : V} {b : V} (p : Quiver.Path a b) (e : b ⟶ a) : p.cons e ≠ Quiver.Path.nil

theorem Quiver.Path.obj_eq_of_cons_eq_cons {V : Type u} [Quiver V] {a : V} {b : V} {c : V} {d : V} {p : Quiver.Path a b} {p' : Quiver.Path a 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 : V} {b : V} {c : V} {d : V} {p : Quiver.Path a b} {p' : Quiver.Path a c} {e : b ⟶ d} {e' : c ⟶ d} (h : p.cons e = p'.cons e') : HEq p p'

theorem Quiver.Path.hom_heq_of_cons_eq_cons {V : Type u} [Quiver V] {a : V} {b : V} {c : V} {d : V} {p : Quiver.Path a b} {p' : Quiver.Path a c} {e : b ⟶ d} {e' : c ⟶ d} (h : p.cons e = p'.cons e') : HEq e e'

def Quiver.Path.length {V : Type u} [Quiver V] {a : V} {b : V} : Quiver.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

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

Equations

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

@[simp]

theorem Quiver.Path.length_nil {V : Type u} [Quiver V] {a : V} : Quiver.Path.nil.length = 0

@[simp]

theorem Quiver.Path.length_cons {V : Type u} [Quiver V] (a : V) (b : V) (c : V) (p : Quiver.Path a b) (e : b ⟶ c) : (p.cons e).length = p.length + 1

theorem Quiver.Path.eq_of_length_zero {V : Type u} [Quiver V] {a : V} {b : V} (p : Quiver.Path a b) (hzero : p.length = 0) : a = b

theorem Quiver.Path.eq_nil_of_length_zero {V : Type u} [Quiver V] {a : V} (p : Quiver.Path a a) (hzero : p.length = 0) : p = Quiver.Path.nil

def Quiver.Path.comp {V : Type u} [Quiver V] {a : V} {b : V} {c : V} : Quiver.Path a b → Quiver.Path b c → Quiver.Path a c

Composition of paths.

Equations

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

@[simp]

theorem Quiver.Path.comp_cons {V : Type u} [Quiver V] {a : V} {b : V} {c : V} {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 : V} {b : V} (p : Quiver.Path a b) : p.comp Quiver.Path.nil = p

@[simp]

theorem Quiver.Path.nil_comp {V : Type u} [Quiver V] {a : V} {b : V} (p : Quiver.Path a b) : Quiver.Path.nil.comp p = p

@[simp]

theorem Quiver.Path.comp_assoc {V : Type u} [Quiver V] {a : V} {b : V} {c : V} {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)

@[simp]

theorem Quiver.Path.length_comp {V : Type u} [Quiver V] {a : V} {b : V} (p : Quiver.Path a b) {c : V} (q : Quiver.Path b c) : (p.comp q).length = p.length + q.length

theorem Quiver.Path.comp_inj {V : Type u} [Quiver V] {a : V} {b : V} {c : V} {p₁ : Quiver.Path a b} {p₂ : Quiver.Path a b} {q₁ : Quiver.Path b c} {q₂ : Quiver.Path b 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 : V} {b : V} {c : V} {p₁ : Quiver.Path a b} {p₂ : Quiver.Path a b} {q₁ : Quiver.Path b c} {q₂ : Quiver.Path b 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 : V} {b : V} {c : V} (q : Quiver.Path b c) : Function.Injective fun (p : Quiver.Path a b) => p.comp q

theorem Quiver.Path.comp_injective_right {V : Type u} [Quiver V] {a : V} {b : V} {c : V} (p : Quiver.Path a b) : Function.Injective p.comp

@[simp]

theorem Quiver.Path.comp_inj_left {V : Type u} [Quiver V] {a : V} {b : V} {c : V} {p₁ : Quiver.Path a b} {p₂ : Quiver.Path a b} {q : Quiver.Path b c} : p₁.comp q = p₂.comp q ↔ p₁ = p₂

@[simp]

theorem Quiver.Path.comp_inj_right {V : Type u} [Quiver V] {a : V} {b : V} {c : V} {p : Quiver.Path a b} {q₁ : Quiver.Path b c} {q₂ : Quiver.Path b c} : p.comp q₁ = p.comp q₂ ↔ q₁ = q₂

theorem Quiver.Path.eq_toPath_comp_of_length_eq_succ {V : Type u} [Quiver V] {a : V} {b : V} (p : Quiver.Path a b) {n : ℕ} (hp : p.length = n + 1) : ∃ (c : V), ∃ (f : a ⟶ c), ∃ (q : Quiver.Path c b), ∃ (x : q.length = n), p = f.toPath.comp q

def Quiver.Path.toList {V : Type u} [Quiver V] {a : V} {b : V} : Quiver.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

@[simp]

theorem Quiver.Path.toList_comp {V : Type u} [Quiver V] {a : V} {b : V} (p : Quiver.Path a b) {c : V} (q : Quiver.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.

theorem Quiver.Path.toList_chain_nonempty {V : Type u} [Quiver V] {a : V} {b : V} (p : Quiver.Path a b) : List.Chain (fun (x y : V) => Nonempty (y ⟶ x)) b p.toList

theorem Quiver.Path.toList_injective {V : Type u} [Quiver V] [∀ (a b : V), Subsingleton (a ⟶ b)] (a : V) (b : V) : Function.Injective Quiver.Path.toList

@[simp]

theorem Quiver.Path.toList_inj {V : Type u} [Quiver V] {a : V} {b : V} [∀ (a b : V), Subsingleton (a ⟶ b)] {p : Quiver.Path a b} {q : Quiver.Path a b} : p.toList = q.toList ↔ p = q

def Prefunctor.mapPath {V : Type u₁} [Quiver V] {W : Type u₂} [Quiver W] (F : V ⥤q W) {a : V} {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)

@[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

@[simp]

theorem Prefunctor.mapPath_cons {V : Type u₁} [Quiver V] {W : Type u₂} [Quiver W] (F : V ⥤q W) {a : V} {b : V} {c : V} (p : Quiver.Path a b) (e : b ⟶ c) : F.mapPath (p.cons e) = (F.mapPath p).cons (F.map e)

@[simp]

theorem Prefunctor.mapPath_comp {V : Type u₁} [Quiver V] {W : Type u₂} [Quiver W] (F : V ⥤q W) {a : V} {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)

@[simp]

theorem Prefunctor.mapPath_toPath {V : Type u₁} [Quiver V] {W : Type u₂} [Quiver W] (F : V ⥤q W) {a : V} {b : V} (f : a ⟶ b) : F.mapPath f.toPath = (F.map f).toPath