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.

ink

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

• 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

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

ink

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

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

Equations

• Quiver.Path.recC nil cons Quiver.Path.nil = nil
• Quiver.Path.recC nil cons (Quiver.Path.cons p e) = cons b x p e (Quiver.Path.recC nil (fun {b c} => cons b c) p)

ink

@[csimp]

theorem Quiver.Path.rec_eq_recC : @Quiver.Path.rec = @Quiver.Path.recC

ink

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

An arrow viewed as a path of length one.

Equations

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

ink

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

ink

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

ink

theorem Quiver.Path.obj_eq_of_cons_eq_cons {V : Type u} [inst : 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 : Quiver.Path.cons p e = Quiver.Path.cons p' e') : b = c

ink

theorem Quiver.Path.heq_of_cons_eq_cons {V : Type u} [inst : 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 : Quiver.Path.cons p e = Quiver.Path.cons p' e') : HEq p p'

ink

theorem Quiver.Path.hom_heq_of_cons_eq_cons {V : Type u} [inst : 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 : Quiver.Path.cons p e = Quiver.Path.cons p' e') : HEq e e'

ink

def Quiver.Path.length {V : Type u} [inst : 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.length Quiver.Path.nil = 0
• Quiver.Path.length (Quiver.Path.cons p e) = Quiver.Path.length p + 1

ink

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

Equations

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

ink

@[simp]

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

ink

@[simp]

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

ink

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

ink

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

Composition of paths.

Equations

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

ink

@[simp]

theorem Quiver.Path.comp_cons {V : Type u} [inst : Quiver V] {a : V} {b : V} {c : V} {d : V} (p : Quiver.Path a b) (q : Quiver.Path b c) (e : c ⟶ d) : Quiver.Path.comp p (Quiver.Path.cons q e) = Quiver.Path.cons (Quiver.Path.comp p q) e

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

theorem Quiver.Path.comp_assoc {V : Type u} [inst : 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) : Quiver.Path.comp (Quiver.Path.comp p q) r = Quiver.Path.comp p (Quiver.Path.comp q r)

ink

@[simp]

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

ink

theorem Quiver.Path.comp_inj {V : Type u} [inst : 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 : Quiver.Path.length q₁ = Quiver.Path.length q₂) : Quiver.Path.comp p₁ q₁ = Quiver.Path.comp p₂ q₂ ↔ p₁ = p₂ ∧ q₁ = q₂

ink

theorem Quiver.Path.comp_inj' {V : Type u} [inst : 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 : Quiver.Path.length p₁ = Quiver.Path.length p₂) : Quiver.Path.comp p₁ q₁ = Quiver.Path.comp p₂ q₂ ↔ p₁ = p₂ ∧ q₁ = q₂

ink

theorem Quiver.Path.comp_injective_left {V : Type u} [inst : Quiver V] {a : V} {b : V} {c : V} (q : Quiver.Path b c) : Function.Injective fun p => Quiver.Path.comp p q

ink

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

ink

@[simp]

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

ink

@[simp]

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

ink

def Quiver.Path.toList {V : Type u} [inst : 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.toList Quiver.Path.nil = []
• Quiver.Path.toList (Quiver.Path.cons p e) = b :: Quiver.Path.toList p

ink

@[simp]

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

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

ink

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

ink

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

ink

@[simp]

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

ink

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

The image of a path under a prefunctor.

Equations

• Prefunctor.mapPath F Quiver.Path.nil = Quiver.Path.nil
• Prefunctor.mapPath F (Quiver.Path.cons p e) = Quiver.Path.cons (Prefunctor.mapPath F p) (Prefunctor.map F e)

ink

@[simp]

theorem Prefunctor.mapPath_nil {V : Type u₁} [inst : Quiver V] {W : Type u₂} [inst : Quiver W] (F : V ⥤q W) (a : V) : Prefunctor.mapPath F Quiver.Path.nil = Quiver.Path.nil

ink

@[simp]

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

ink

@[simp]

theorem Prefunctor.mapPath_comp {V : Type u₁} [inst : Quiver V] {W : Type u₂} [inst : Quiver W] (F : V ⥤q W) {a : V} {b : V} (p : Quiver.Path a b) {c : V} (q : Quiver.Path b c) : Prefunctor.mapPath F (Quiver.Path.comp p q) = Quiver.Path.comp (Prefunctor.mapPath F p) (Prefunctor.mapPath F q)

ink

@[simp]

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