Theorems · Inductive type · combinatorics

Quiver

Type u → Type (max u (v + 1))

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

Cited by

405 results in Mathlib

Foundations

Depth 0 from the axioms, rests on 1 definitions · uses no axioms