mathlib3 documentation

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.

source
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
source
def quiver.hom.to_path {V : Type u_1} [quiver V] {a b : V} (e : a ⟶ b) :
quiver.path a b

An arrow viewed as a path of length one.

Equations
source
theorem quiver.path.nil_ne_cons {V : Type u} [quiver V] {a b : V} (p : quiver.path a b) (e : b ⟶ a) :
quiver.path.nil ≠ p.cons e
source
theorem quiver.path.cons_ne_nil {V : Type u} [quiver V] {a b : V} (p : quiver.path a b) (e : b ⟶ a) :
p.cons e ≠ quiver.path.nil
source
theorem quiver.path.obj_eq_of_cons_eq_cons {V : Type u} [quiver V] {a b c 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
source
theorem quiver.path.heq_of_cons_eq_cons {V : Type u} [quiver V] {a b c 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') :
p == p'
source
theorem quiver.path.hom_heq_of_cons_eq_cons {V : Type u} [quiver V] {a b c 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') :
e == e'
source
def quiver.path.length {V : Type u} [quiver V] {a b : V} :
quiver.path a b → ℕ

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

Equations
source
@[protected, instance]
def quiver.path.inhabited {V : Type u} [quiver V] {a : V} :
inhabited (quiver.path a a)
Equations
source
@[simp]
theorem quiver.path.length_nil {V : Type u} [quiver V] {a : V} :
quiver.path.nil.length = 0
source
@[simp]
theorem quiver.path.length_cons {V : Type u} [quiver V] (a b c : V) (p : quiver.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 : quiver.path a b) (hzero : p.length = 0) :
a = b
source
def quiver.path.comp {V : Type u} [quiver V] {a b c : V} :
quiver.path a b → quiver.path b c → quiver.path a c

Composition of paths.

Equations
source
@[simp]
theorem quiver.path.comp_cons {V : Type u} [quiver V] {a b c 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
source
@[simp]
theorem quiver.path.comp_nil {V : Type u} [quiver V] {a b : V} (p : quiver.path a b) :
p.comp quiver.path.nil = p
source
@[simp]
theorem quiver.path.nil_comp {V : Type u} [quiver V] {a b : V} (p : quiver.path a b) :
quiver.path.nil.comp p = p
source
@[simp]
theorem quiver.path.comp_assoc {V : Type u} [quiver V] {a b c 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)
source
@[simp]
theorem quiver.path.length_comp {V : Type u} [quiver V] {a b : V} (p : quiver.path a b) {c : V} (q : quiver.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₂ : quiver.path a b} {q₁ q₂ : quiver.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₂ : quiver.path a b} {q₁ q₂ : quiver.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 : quiver.path b c) :
function.injective (λ (p : quiver.path a b), p.comp q)
source
theorem quiver.path.comp_injective_right {V : Type u} [quiver V] {a b c : V} (p : quiver.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₂ : quiver.path a b} {q : quiver.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 : quiver.path a b} {q₁ q₂ : quiver.path b c} :
p.comp q₁ = p.comp q₂ ↔ q₁ = q₂
source
@[simp]
def quiver.path.to_list {V : Type u} [quiver V] {a 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
source
@[simp]
theorem quiver.path.to_list_comp {V : Type u} [quiver V] {a b : V} (p : quiver.path a b) {c : V} (q : quiver.path b c) :
(p.comp q).to_list = q.to_list ++ p.to_list

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

source
theorem quiver.path.to_list_chain_nonempty {V : Type u} [quiver V] {a b : V} (p : quiver.path a b) :
list.chain (λ (x y : V), nonempty (y ⟶ x)) b p.to_list
source
theorem quiver.path.to_list_injective {V : Type u} [quiver V] [∀ (a b : V), subsingleton (a ⟶ b)] (a b : V) :
function.injective quiver.path.to_list
source
@[simp]
theorem quiver.path.to_list_inj {V : Type u} [quiver V] {a b : V} [∀ (a b : V), subsingleton (a ⟶ b)] {p q : quiver.path a b} :
p.to_list = q.to_list ↔ p = q
source
def prefunctor.map_path {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
source
@[simp]
theorem prefunctor.map_path_nil {V : Type u₁} [quiver V] {W : Type u₂} [quiver W] (F : V ⥤q W) (a : V) :
F.map_path quiver.path.nil = quiver.path.nil
source
@[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 : quiver.path a b) (e : b ⟶ c) :
F.map_path (p.cons e) = (F.map_path p).cons (F.map e)
source
@[simp]
theorem prefunctor.map_path_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.map_path (p.comp q) = (F.map_path p).comp (F.map_path q)
source
@[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) :
F.map_path f.to_path = (F.map f).to_path