Quiver.Path.comp_assoc
theorem Quiver.Path.comp_assoc :
∀ {V : Type u} [inst : 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)
This theorem asserts the associativity of path composition in a quiver. Specifically, for any quiver labeled by a type `V`, and any vertices `a`, `b`, `c`, and `d` in this quiver, if there are paths `p` from `a` to `b`, `q` from `b` to `c`, and `r` from `c` to `d`, then composing `p` and `q` and then `r` is the same as composing `p` with the composition of `q` and `r`. In other words, `(p∘q)∘r = p∘(q∘r)`, where `∘` denotes the path composition operation.
More concisely: For any quiver with vertex labels, and paths `p` from `a` to `b`, `q` from `b` to `c`, and `r` from `c` to `d`, the composition of `p` and `q` followed by `r` equals the composition of `p` with the composition of `q` and `r`. In other words, `(p∘q)∘r = p∘(q∘r)`.
|
Quiver.Path.toList_comp
theorem Quiver.Path.toList_comp :
∀ {V : Type u} [inst : Quiver V] {a b : V} (p : Quiver.Path a b) {c : V} (q : Quiver.Path b c),
(p.comp q).toList = q.toList ++ p.toList
The theorem `Quiver.Path.toList_comp` states that for any two paths `p` and `q` in a quiver (or directed graph), the list of vertices in the composition of the paths is the concatenation of the list of vertices in `q` and `p`. This is a demonstration of the contravariance property of the `Quiver.Path.toList` functor, where the "inversion" is due to the differing preferred directions of `Quiver.Path` and `List` for adding elements. In other words, composing two paths and then converting to a list is the same as converting each path to a list, reversing the order, and then concatenating.
More concisely: For any two paths `p` and `q` in a quiver, the list of vertices in the composition of `p` and `q` is equal to the concatenation of the lists of vertices in `q` and `p`.
|