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.
- nil : Π {V : Type u} [_inst_1 : quiver V] {a : V}, quiver.path a a
- cons : Π {V : Type u} [_inst_1 : quiver V] {a b c : V}, quiver.path a b → (b ⟶ c) → quiver.path a c
G.path a b
is the type of paths from a
to b
through the arrows of G
.
An arrow viewed as a path of length one.
Equations
- e.to_path = quiver.path.nil.cons e
The length of a path is the number of arrows it uses.
@[protected, instance]
Equations
@[simp]
@[simp]
theorem
quiver.path.length_cons
{V : Type u}
[quiver V]
(a b c : V)
(p : quiver.path a b)
(e : b ⟶ c) :
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.
@[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) :
@[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
@[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
@[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) :
def
prefunctor.map_path
{V : Type u₁}
[quiver V]
{W : Type u₂}
[quiver W]
(F : prefunctor V 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.map_path (p.cons e) = (F.map_path p).cons (F.map e)
- F.map_path quiver.path.nil = quiver.path.nil
@[simp]
theorem
prefunctor.map_path_nil
{V : Type u₁}
[quiver V]
{W : Type u₂}
[quiver W]
(F : prefunctor V W)
(a : V) :
@[simp]
theorem
prefunctor.map_path_cons
{V : Type u₁}
[quiver V]
{W : Type u₂}
[quiver W]
(F : prefunctor V W)
{a b c : V}
(p : quiver.path a b)
(e : b ⟶ c) :
@[simp]
theorem
prefunctor.map_path_comp
{V : Type u₁}
[quiver V]
{W : Type u₂}
[quiver W]
(F : prefunctor V W)
{a b : V}
(p : quiver.path a b)
{c : V}
(q : quiver.path b c) :