Skip to the content.
← Index Next: Paths →

Recall

Formal definition cited in this section, gathered here for quick reference (full citation in the Bibliography):

A quiver is a directed graph: a set of vertices and a set of directed edges (called arrows) between them. This is the same notion Mathlib calls Quiver (built here from scratch, following Chapter 0’s “no Mathlib” policy, rather than reusing Mathlib’s). Formally, a quiver $Q$ consists of:

Picture an arrow $\alpha : i \to j$ as a literal arrow drawn from vertex $i$ to vertex $j$; $s(\alpha) = i$ and $t(\alpha) = j$.

Example quiver

Take vertices ${1, 2, 3}$ and arrows

\[\alpha : 1 \to 2, \qquad \beta : 2 \to 3\]

References

Full citations in the Bibliography. Formal definitions are gathered in Recall, above.


← Index Next: Paths →
Try Lean
Lean playground · v1.4.18