Structures · Combinatorics

Quiver

A quiver G on a type V of vertices assigns to every pair a b : V of vertices a type a ⟶ b of arrows from a to b. This is hence a form of directed multigraphs. For graphs with no repeated edges, one can either use Quiver.IsThin to demand that the hom sets are subsingletons, or Digraph V (where the hom sets are Prop-valued). Because Category will later extend this class, we call the field Hom. Except when constructing instances, you should rarely see this, and use the ⟶ notation instead.

Defined in

Mathlib.Combinatorics.Quiver.Basic

Shape

One type argument · adds Hom