Mathlib.Combinatorics.Quiver.Path

Quiver.Path inductive

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

Full source

/-- `Path a b` is the type of paths from `a` to `b` through the arrows of `G`. -/
inductive Path {V : Type u} [Quiver.{v} V] (a : V) : V → Sort max (u + 1) v
  | nil : Path a a
  | cons : ∀ {b c : V}, Path a b → (b ⟶ c) → Path a c

Paths in a quiver

Informal description

Given a quiver `V` (a directed graph where edges are called arrows), the type `Path a b` represents all possible paths from vertex `a` to vertex `b` by composing arrows in the quiver. This is defined inductively, with the empty path (identity) at each vertex and the ability to extend a path by prepending an arrow.

Quiver.Hom.toPath definition

{V} [Quiver V] {a b : V} (e : a ⟶ b) : Path a b

Full source

/-- An arrow viewed as a path of length one. -/
def Hom.toPath {V} [Quiver V] {a b : V} (e : a ⟶ b) : Path a b :=
  Path.nil.cons e

Arrow as a path of length one

Informal description

Given a quiver $ V $ and an arrow $ e $ from vertex $ a $ to vertex $ b $, the function maps $ e $ to the path consisting of just $ e $, which is a path of length one from $ a $ to $ b $.

Quiver.Path.nil_ne_cons theorem

(p : Path a b) (e : b ⟶ a) : Path.nil ≠ p.cons e

Full source

lemma nil_ne_cons (p : Path a b) (e : b ⟶ a) : Path.nilPath.nil ≠ p.cons e :=
  fun h => by injection h

Empty Path is Not Equal to Prepended Path

Informal description

For any path $p$ from vertex $a$ to vertex $b$ in a quiver and any arrow $e$ from $b$ to $a$, the empty path $\mathrm{nil}$ is not equal to the path obtained by prepending $e$ to $p$ (denoted $p.\mathrm{cons}(e)$).

Quiver.Path.cons_ne_nil theorem

(p : Path a b) (e : b ⟶ a) : p.cons e ≠ Path.nil

Full source

lemma cons_ne_nil (p : Path a b) (e : b ⟶ a) : p.cons e ≠ Path.nil :=
  fun h => by injection h

Non-empty path inequality: $p.cons\ e \neq \text{nil}$

Informal description

For any path $p$ from vertex $a$ to vertex $b$ in a quiver $V$, and any arrow $e$ from $b$ to $a$, the path obtained by extending $p$ with $e$ (denoted $p.cons\ e$) is not equal to the empty path at $a$ (denoted $\text{Path.nil}$).

Quiver.Path.obj_eq_of_cons_eq_cons theorem

{p : Path a b} {p' : Path a c} {e : b ⟶ d} {e' : c ⟶ d} (h : p.cons e = p'.cons e') : b = c

Full source

lemma obj_eq_of_cons_eq_cons {p : Path a b} {p' : Path a c}
    {e : b ⟶ d} {e' : c ⟶ d} (h : p.cons e = p'.cons e') : b = c := by injection h

Equality of Target Vertices for Equal Extended Paths in a Quiver

Informal description

Let $V$ be a quiver, and let $a, b, c, d$ be vertices in $V$. For any paths $p$ from $a$ to $b$ and $p'$ from $a$ to $c$, and any arrows $e : b \to d$ and $e' : c \to d$, if the extended paths $p.cons\, e$ and $p'.cons\, e'$ are equal, then $b = c$.

Quiver.Path.heq_of_cons_eq_cons theorem

{p : Path a b} {p' : Path a c} {e : b ⟶ d} {e' : c ⟶ d} (h : p.cons e = p'.cons e') : HEq p p'

Full source

lemma heq_of_cons_eq_cons {p : Path a b} {p' : Path a c}
    {e : b ⟶ d} {e' : c ⟶ d} (h : p.cons e = p'.cons e') : HEq p p' := by injection h

Heterogeneous Equality of Paths from Cons Equality

Informal description

Given paths $p$ from $a$ to $b$ and $p'$ from $a$ to $c$ in a quiver, and arrows $e : b \to d$ and $e' : c \to d$, if the extended paths $p.cons\ e$ and $p'.cons\ e'$ are equal, then the original paths $p$ and $p'$ are heterogeneously equal (HEq).

Quiver.Path.hom_heq_of_cons_eq_cons theorem

{p : Path a b} {p' : Path a c} {e : b ⟶ d} {e' : c ⟶ d} (h : p.cons e = p'.cons e') : HEq e e'

Full source

lemma hom_heq_of_cons_eq_cons {p : Path a b} {p' : Path a c}
    {e : b ⟶ d} {e' : c ⟶ d} (h : p.cons e = p'.cons e') : HEq e e' := by injection h

Heterogeneous Equality of Arrows in Extended Path Equality

Informal description

Given two paths $p$ from $a$ to $b$ and $p'$ from $a$ to $c$ in a quiver, and arrows $e : b \to d$ and $e' : c \to d$, if the extended paths $p.cons\ e$ and $p'.cons\ e'$ are equal, then the arrows $e$ and $e'$ are heterogeneously equal (i.e., equal up to the equality of their domains and codomains).

Quiver.Path.length definition

{a : V} : ∀ {b : V}, Path a b → ℕ

Full source

/-- The length of a path is the number of arrows it uses. -/
def length {a : V} : ∀ {b : V}, Path a b → ℕ
  | _, nil => 0
  | _, cons p _ => p.length + 1

Length of a path in a quiver

Informal description

The length of a path in a quiver is defined inductively as follows: - The empty path (from any vertex to itself) has length $0$. - For a path formed by extending another path $p$ with an additional arrow, the length is $p.\text{length} + 1$.

Quiver.Path.instInhabited instance

{a : V} : Inhabited (Path a a)

Full source

instance {a : V} : Inhabited (Path a a) :=
  ⟨nil⟩

Inhabited Type of Trivial Paths in a Quiver

Informal description

For any vertex $a$ in a quiver $V$, the type of paths from $a$ to itself is inhabited by the empty path.

Quiver.Path.length_nil theorem

{a : V} : (nil : Path a a).length = 0

Full source

@[simp]
theorem length_nil {a : V} : (nil : Path a a).length = 0 :=
  rfl

Length of Empty Path is Zero

Informal description

For any vertex $a$ in a quiver $V$, the length of the empty path from $a$ to itself is $0$.

Quiver.Path.length_cons theorem

(a b c : V) (p : Path a b) (e : b ⟶ c) : (p.cons e).length = p.length + 1

Full source

@[simp]
theorem length_cons (a b c : V) (p : Path a b) (e : b ⟶ c) : (p.cons e).length = p.length + 1 :=
  rfl

Length of Extended Path in a Quiver: $(p.\text{cons}(e)).\text{length} = p.\text{length} + 1$

Informal description

For any vertices $a, b, c$ in a quiver $V$, given a path $p$ from $a$ to $b$ and an arrow $e$ from $b$ to $c$, the length of the path obtained by extending $p$ with $e$ (denoted $p.\text{cons}(e)$) is equal to the length of $p$ plus one, i.e., $(p.\text{cons}(e)).\text{length} = p.\text{length} + 1$.

Quiver.Path.comp definition

{a b : V} : ∀ {c}, Path a b → Path b c → Path a c

Full source

/-- Composition of paths. -/
def comp {a b : V} : ∀ {c}, Path a b → Path b c → Path a c
  | _, p, nil => p
  | _, p, cons q e => (p.comp q).cons e

Composition of paths in a quiver

Informal description

Given a quiver $ V $ and vertices $ a, b, c $, the composition of paths $ p : \text{Path } a b $ and $ q : \text{Path } b c $ is a path $ \text{Path } a c $ obtained by concatenating $ p $ and $ q $. The composition is defined inductively: - If $ q $ is the empty path (identity) at $ b $, then $ p \circ q = p $. - If $ q $ is of the form $ q' \circ e $ where $ q' : \text{Path } b c' $ and $ e : c' \to c $ is an arrow, then $ p \circ q = (p \circ q') \circ e $.

Quiver.Path.comp_cons theorem

{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

Full source

@[simp]
theorem comp_cons {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 :=
  rfl

Associativity of Path Composition with Arrow Extension in Quivers

Informal description

For any vertices $a, b, c, d$ in a quiver $V$, given a path $p$ from $a$ to $b$, a path $q$ from $b$ to $c$, and an arrow $e$ from $c$ to $d$, the composition of $p$ with the path obtained by extending $q$ with $e$ is equal to the path obtained by extending the composition of $p$ and $q$ with $e$. In symbols: $$ p \circ (q \circ e) = (p \circ q) \circ e $$

Quiver.Path.comp_nil theorem

{a b : V} (p : Path a b) : p.comp Path.nil = p

Full source

@[simp]
theorem comp_nil {a b : V} (p : Path a b) : p.comp Path.nil = p :=
  rfl

Right Identity of Path Composition with Empty Path

Informal description

For any path $p$ from vertex $a$ to vertex $b$ in a quiver $V$, the composition of $p$ with the empty path at $b$ is equal to $p$ itself, i.e., $p \circ \text{nil} = p$.

Quiver.Path.nil_comp theorem

{a : V} : ∀ {b} (p : Path a b), Path.nil.comp p = p

Full source

@[simp]
theorem nil_comp {a : V} : ∀ {b} (p : Path a b), Path.nil.comp p = p
  | _, nil => rfl
  | _, cons p _ => by rw [comp_cons, nil_comp p]

Left Identity of Path Composition with Empty Path

Informal description

For any vertex $a$ in a quiver $V$ and any path $p$ from $a$ to $b$, the composition of the empty path at $a$ with $p$ equals $p$, i.e., $\text{nil} \circ p = p$.

Quiver.Path.comp_assoc theorem

{a b c : V} : ∀ {d} (p : Path a b) (q : Path b c) (r : Path c d), (p.comp q).comp r = p.comp (q.comp r)

Full source

@[simp]
theorem comp_assoc {a b c : V} :
    ∀ {d} (p : Path a b) (q : Path b c) (r : Path c d), (p.comp q).comp r = p.comp (q.comp r)
  | _, _, _, nil => rfl
  | _, p, q, cons r _ => by rw [comp_cons, comp_cons, comp_cons, comp_assoc p q r]

Associativity of Path Composition in Quivers

Informal description

For any vertices $a, b, c, d$ in a quiver $V$ and paths $p : \text{Path } a b$, $q : \text{Path } b c$, $r : \text{Path } c d$, the composition of paths is associative: $$ (p \circ q) \circ r = p \circ (q \circ r) $$

Quiver.Path.length_comp theorem

(p : Path a b) : ∀ {c} (q : Path b c), (p.comp q).length = p.length + q.length

Full source

@[simp]
theorem length_comp (p : Path a b) : ∀ {c} (q : Path b c), (p.comp q).length = p.length + q.length
  | _, nil => rfl
  | _, cons _ _ => congr_arg Nat.succ (length_comp _ _)

Additivity of Path Length under Composition

Informal description

For any path $p$ from vertex $a$ to vertex $b$ in a quiver and any path $q$ from $b$ to $c$, the length of the composed path $p \circ q$ is equal to the sum of the lengths of $p$ and $q$, i.e., $\text{length}(p \circ q) = \text{length}(p) + \text{length}(q)$.

Quiver.Path.comp_inj theorem

 {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₂

Full source

theorem comp_inj {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₂ := by
  refine ⟨fun h => ?_, by rintro ⟨rfl, rfl⟩; rfl⟩
  induction q₁ with
  | nil =>
    rcases q₂ with _ | ⟨q₂, f₂⟩
    · exact ⟨h, rfl⟩
    · cases hq
  | cons q₁ f₁ ih =>
    rcases q₂ with _ | ⟨q₂, f₂⟩
    · cases hq
    · simp only [comp_cons, cons.injEq] at h
      obtain rfl := h.1
      obtain ⟨rfl, rfl⟩ := ih (Nat.succ.inj hq) h.2.1.eq
      rw [h.2.2.eq]
      exact ⟨rfl, rfl⟩

Injectivity of Path Composition under Equal Length Condition

Informal description

For any paths $p_1, p_2$ from vertex $a$ to vertex $b$ and any paths $q_1, q_2$ from $b$ to $c$ in a quiver, if $q_1$ and $q_2$ have the same length, then the composition $p_1 \circ q_1$ equals $p_2 \circ q_2$ if and only if $p_1 = p_2$ and $q_1 = q_2$.

Quiver.Path.comp_inj' theorem

 {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₂

Full source

theorem comp_inj' {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₂ :=
  ⟨fun h_eq => (comp_inj <| Nat.add_left_cancel (n := p₂.length) <|
    by simpa [h] using congr_arg length h_eq).1 h_eq,
   by rintro ⟨rfl, rfl⟩; rfl⟩

Injectivity of Path Composition under Equal Source Path Length Condition

Informal description

For any paths $p_1, p_2$ from vertex $a$ to vertex $b$ and any paths $q_1, q_2$ from $b$ to $c$ in a quiver, if $p_1$ and $p_2$ have the same length, then the composition $p_1 \circ q_1$ equals $p_2 \circ q_2$ if and only if $p_1 = p_2$ and $q_1 = q_2$.

Quiver.Path.comp_injective_left theorem

(q : Path b c) : Injective fun p : Path a b => p.comp q

Full source

theorem comp_injective_left (q : Path b c) : Injective fun p : Path a b => p.comp q :=
  fun _ _ h => ((comp_inj rfl).1 h).1

Left Injectivity of Path Composition in Quivers

Informal description

For any path $q$ from vertex $b$ to vertex $c$ in a quiver, the function that composes paths $p$ from $a$ to $b$ with $q$ is injective. That is, if $p_1 \circ q = p_2 \circ q$ for paths $p_1, p_2 : \text{Path } a b$, then $p_1 = p_2$.

Quiver.Path.comp_injective_right theorem

(p : Path a b) : Injective (p.comp : Path b c → Path a c)

Full source

theorem comp_injective_right (p : Path a b) : Injective (p.comp : Path b c → Path a c) :=
  fun _ _ h => ((comp_inj' rfl).1 h).2

Right Injectivity of Path Composition in Quivers

Informal description

For any path $p$ from vertex $a$ to vertex $b$ in a quiver, the function that composes $p$ with paths $q$ from $b$ to $c$ is injective. That is, if $p \circ q_1 = p \circ q_2$ for paths $q_1, q_2 : \text{Path } b c$, then $q_1 = q_2$.

Quiver.Path.comp_inj_left theorem

{p₁ p₂ : Path a b} {q : Path b c} : p₁.comp q = p₂.comp q ↔ p₁ = p₂

Full source

@[simp]
theorem comp_inj_left {p₁ p₂ : Path a b} {q : Path b c} : p₁.comp q = p₂.comp q ↔ p₁ = p₂ :=
  q.comp_injective_left.eq_iff

Left Cancellation Property of Path Composition in Quivers: $p_1 \circ q = p_2 \circ q \leftrightarrow p_1 = p_2$

Informal description

For any paths $p_1, p_2$ from vertex $a$ to vertex $b$ and any path $q$ from $b$ to $c$ in a quiver, the composition $p_1 \circ q$ equals $p_2 \circ q$ if and only if $p_1 = p_2$.

Quiver.Path.comp_inj_right theorem

{p : Path a b} {q₁ q₂ : Path b c} : p.comp q₁ = p.comp q₂ ↔ q₁ = q₂

Full source

@[simp]
theorem comp_inj_right {p : Path a b} {q₁ q₂ : Path b c} : p.comp q₁ = p.comp q₂ ↔ q₁ = q₂ :=
  p.comp_injective_right.eq_iff

Right Cancellation Property of Path Composition in Quivers: $p \circ q_1 = p \circ q_2 \leftrightarrow q_1 = q_2$

Informal description

For any path $p$ from vertex $a$ to vertex $b$ in a quiver, and any two paths $q_1, q_2$ from $b$ to $c$, the composition $p \circ q_1$ equals $p \circ q_2$ if and only if $q_1 = q_2$.

Quiver.Path.toList definition

: ∀ {b : V}, Path a b → List V

Full source

/-- Turn a path into a list. The list contains `a` at its head, but not `b` a priori. -/
@[simp]
def toList : ∀ {b : V}, Path a b → List V
  | _, nil => []
  | _, @cons _ _ _ c _ p _ => c :: p.toList

List of vertices in a quiver path

Informal description

Given a path $ p $ from vertex $ a $ to vertex $ b $ in a quiver $ V $, the function returns the list of vertices encountered along the path, starting with $ a $ and ending just before $ b $. The empty path at $ a $ returns an empty list.

Quiver.Path.toList_comp theorem

(p : Path a b) : ∀ {c} (q : Path b c), (p.comp q).toList = q.toList ++ p.toList

Full source

/-- `Quiver.Path.toList` is a contravariant functor. The inversion comes from `Quiver.Path` and
`List` having different preferred directions for adding elements. -/
@[simp]
theorem toList_comp (p : Path a b) : ∀ {c} (q : Path b c), (p.comp q).toList = q.toList ++ p.toList
  | _, nil => by simp
  | _, @cons _ _ _ d _ q _ => by simp [toList_comp]

Vertex List of Composed Path Equals Concatenated Vertex Lists

Informal description

For any path $p$ from vertex $a$ to vertex $b$ and any path $q$ from vertex $b$ to vertex $c$ in a quiver $V$, the list of vertices obtained from the composition $p \circ q$ is equal to the concatenation of the vertex lists of $q$ and $p$, i.e., $\text{toList}(p \circ q) = \text{toList}(q) +\!\!+ \text{toList}(p)$.

Quiver.Path.toList_chain_nonempty theorem

: ∀ {b} (p : Path a b), p.toList.Chain (fun x y => Nonempty (y ⟶ x)) b

Full source

theorem toList_chain_nonempty :
    ∀ {b} (p : Path a b), p.toList.Chain (fun x y => Nonempty (y ⟶ x)) b
  | _, nil => List.Chain.nil
  | _, cons p f => p.toList_chain_nonempty.cons ⟨f⟩

Path Vertex List Forms Nonempty Arrow Chain

Informal description

For any path $p$ from vertex $a$ to vertex $b$ in a quiver $V$, the list of vertices obtained from $p$ forms a chain where for each consecutive pair of vertices $(x, y)$ in the list, there exists at least one arrow from $y$ to $x$ (i.e., $\text{Nonempty}(y \to x)$), and this chain ends at $b$.

Quiver.Path.toList_injective theorem

(a : V) : ∀ b, Injective (toList : Path a b → List V)

Full source

theorem toList_injective (a : V) : ∀ b, Injective (toList : Path a b → List V)
  | _, nil, nil, _ => rfl
  | _, nil, @cons _ _ _ c _ p f, h => by cases h
  | _, @cons _ _ _ c _ p f, nil, h => by cases h
  | _, @cons _ _ _ c _ p f, @cons _ _ _ t _ C D, h => by
    simp only [toList, List.cons.injEq] at h
    obtain ⟨rfl, hAC⟩ := h
    simp [toList_injective _ _ hAC, eq_iff_true_of_subsingleton]

Injectivity of Vertex List Mapping for Quiver Paths

Informal description

For any vertex $a$ in a quiver $V$ and any vertex $b$, the function $\text{toList} : \text{Path}(a, b) \to \text{List}(V)$ is injective. That is, for any two paths $p, q$ from $a$ to $b$, if $\text{toList}(p) = \text{toList}(q)$, then $p = q$.

Quiver.Path.toList_inj theorem

{p q : Path a b} : p.toList = q.toList ↔ p = q

Full source

@[simp]
theorem toList_inj {p q : Path a b} : p.toList = q.toList ↔ p = q :=
  (toList_injective _ _).eq_iff

Vertex List Determines Path in Quiver: $p.\text{toList} = q.\text{toList} \leftrightarrow p = q$

Informal description

For any two paths $p$ and $q$ from vertex $a$ to vertex $b$ in a quiver, the list of vertices obtained from $p$ is equal to the list obtained from $q$ if and only if the paths $p$ and $q$ are equal. In other words, the function mapping paths to their vertex lists is injective.

Prefunctor.mapPath definition

{a : V} : ∀ {b : V}, Path a b → Path (F.obj a) (F.obj b)

Full source

/-- The image of a path under a prefunctor. -/
def mapPath {a : V} : ∀ {b : V}, Path a b → Path (F.obj a) (F.obj b)
  | _, Path.nil => Path.nil
  | _, Path.cons p e => Path.cons (mapPath p) (F.map e)

Image of a path under a prefunctor

Informal description

Given a prefunctor $ F $ between quivers $ V $ and $ W $, the function $ \text{mapPath} $ maps a path $ p $ from $ a $ to $ b $ in $ V $ to a path from $ F(a) $ to $ F(b) $ in $ W $. This is defined recursively: - The empty path at $ a $ is mapped to the empty path at $ F(a) $. - A path formed by extending a path $ p $ with an arrow $ e $ is mapped to the path formed by extending $ \text{mapPath}(p) $ with $ F(e) $.

Prefunctor.mapPath_nil theorem

(a : V) : F.mapPath (Path.nil : Path a a) = Path.nil

Full source

@[simp]
theorem mapPath_nil (a : V) : F.mapPath (Path.nil : Path a a) = Path.nil :=
  rfl

Prefunctor Maps Empty Path to Empty Path

Informal description

For any vertex $a$ in a quiver $V$, the image of the empty path at $a$ under a prefunctor $F$ is the empty path at $F(a)$. That is, $F(\text{nil}_a) = \text{nil}_{F(a)}$.

Prefunctor.mapPath_cons theorem

{a b c : V} (p : Path a b) (e : b ⟶ c) : F.mapPath (Path.cons p e) = Path.cons (F.mapPath p) (F.map e)

Full source

@[simp]
theorem mapPath_cons {a b c : V} (p : Path a b) (e : b ⟶ c) :
    F.mapPath (Path.cons p e) = Path.cons (F.mapPath p) (F.map e) :=
  rfl

Prefunctor Image of Extended Path Equals Extended Image Path

Informal description

Given a prefunctor $F$ between quivers $V$ and $W$, and a path $p$ from $a$ to $b$ in $V$ followed by an arrow $e : b \to c$, the image of the extended path $\text{cons}(p, e)$ under $F$ is equal to the path formed by extending the image of $p$ under $F$ with the image of $e$ under $F$. That is: $$ F.\text{mapPath}(\text{cons}(p, e)) = \text{cons}(F.\text{mapPath}(p), F.\text{map}(e)) $$

Prefunctor.mapPath_comp theorem

{a b : V} (p : Path a b) : ∀ {c : V} (q : Path b c), F.mapPath (p.comp q) = (F.mapPath p).comp (F.mapPath q)

Full source

@[simp]
theorem mapPath_comp {a b : V} (p : Path a b) :
    ∀ {c : V} (q : Path b c), F.mapPath (p.comp q) = (F.mapPath p).comp (F.mapPath q)
  | _, Path.nil => rfl
  | c, Path.cons q e => by dsimp; rw [mapPath_comp p q]

Functoriality of Path Composition under Prefunctors

Informal description

Let $V$ and $W$ be quivers, and let $F : V \to W$ be a prefunctor between them. For any vertices $a, b, c \in V$ and paths $p : \text{Path } a b$, $q : \text{Path } b c$, the image of the composed path $p \circ q$ under $F$ equals the composition of the images of $p$ and $q$ under $F$. That is, $$ F_{\text{mapPath}}(p \circ q) = F_{\text{mapPath}}(p) \circ F_{\text{mapPath}}(q). $$

Prefunctor.mapPath_toPath theorem

{a b : V} (f : a ⟶ b) : F.mapPath f.toPath = (F.map f).toPath

Full source

@[simp]
theorem mapPath_toPath {a b : V} (f : a ⟶ b) : F.mapPath f.toPath = (F.map f).toPath :=
  rfl

Prefunctor Maps Single-Arrow Path to Single-Arrow Path

Informal description

Given a prefunctor $F$ between quivers $V$ and $W$, and an arrow $f : a \to b$ in $V$, the image under $F$ of the path consisting solely of $f$ (i.e., $f.\text{toPath}$) is equal to the path consisting solely of $F(f)$ (i.e., $(F(f)).\text{toPath}$). In other words, $F.\text{mapPath}(f.\text{toPath}) = (F(f)).\text{toPath}$.

Prefunctor.mapPath_id theorem

{a b : V} : (p : Path a b) → (𝟭q V).mapPath p = p

Full source

@[simp]
theorem mapPath_id {a b : V} : (p : Path a b) → (𝟭q V).mapPath p = p
  | Path.nil => rfl
  | Path.cons q e => by dsimp; rw [mapPath_id q]

Identity Prefunctor Preserves Paths

Informal description

For any path $p$ from $a$ to $b$ in a quiver $V$, the image of $p$ under the identity prefunctor $\text{id}_V$ is equal to $p$ itself, i.e., $\text{id}_V.\text{mapPath}(p) = p$.

Prefunctor.mapPath_comp_apply theorem

{a b : V} (p : Path a b) : (F ⋙q G).mapPath p = G.mapPath (F.mapPath p)

Full source

@[simp]
theorem mapPath_comp_apply {a b : V} (p : Path a b) :
    (F ⋙q G).mapPath p = G.mapPath (F.mapPath p) := by
  induction p with
  | nil => rfl
  | cons x y h => simp [h]

Functoriality of Path Mapping under Prefunctor Composition

Informal description

Given quivers $ V $ and $ W $, a prefunctor $ F : V \to W $, and a path $ p $ from $ a $ to $ b $ in $ V $, the image of $ p $ under the composition of prefunctors $ F $ and $ G $ is equal to the image under $ G $ of the image of $ p $ under $ F $. In other words, \[ (F \circ G).\text{mapPath}(p) = G.\text{mapPath}(F.\text{mapPath}(p)). \]