mathlib documentation

combinatorics.quiver.basic

Quivers #

This module defines quivers. A quiver 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 a very permissive notion of directed graph.

Implementation notes #

Currently quiver is defined with arrow : V → V → Sort v. This is different from the category theory setup, where we insist that morphisms live in some Type. There's some balance here: it's nice to allow Prop to ensure there are no multiple arrows, but it is also results in error-prone universe signatures when constraints require a Type.

source
@[class]
structure quiver (V : Type u) :
Type (max u v)
  • hom : V → V → Sort ?

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.

For graphs with no repeated edges, one can use quiver.{0} V, which ensures a ⟶ b : Prop. For multigraphs, one can use quiver.{v+1} V, which ensures a ⟶ b : Type v.

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.

Instances
source
structure prefunctor (V : Type u₁) [quiver V] (W : Type u₂) [quiver W] :
Sort (max (imax (u₁+1) (u₁+1) v₁ v₂) (u₁+1) (u₂+1))
  • obj : V → W
  • map : Π {X Y : V}, (X ⟶ Y) → (self.obj X ⟶ self.obj Y)

A morphism of quivers. As we will later have categorical functors extend this structure, we call it a prefunctor.

source
def prefunctor.id (V : Type u_1) [quiver V] :
prefunctor V V

The identity morphism between quivers.

Equations
source
@[simp]
theorem prefunctor.id_map (V : Type u_1) [quiver V] (X Y : V) (f : X ⟶ Y) :
(prefunctor.id V).map f = f
source
@[simp]
theorem prefunctor.id_obj (V : Type u_1) [quiver V] (a : V) :
(prefunctor.id V).obj a = id a
source
@[protected, instance]
def prefunctor.inhabited (V : Type u_1) [quiver V] :
inhabited (prefunctor V V)
Equations
source
def prefunctor.comp {U : Type u_1} [quiver U] {V : Type u_3} [quiver V] {W : Type u_5} [quiver W] (F : prefunctor U V) (G : prefunctor V W) :
prefunctor U W

Composition of morphisms between quivers.

Equations
source
@[simp]
theorem prefunctor.comp_obj {U : Type u_1} [quiver U] {V : Type u_3} [quiver V] {W : Type u_5} [quiver W] (F : prefunctor U V) (G : prefunctor V W) (X : U) :
(F.comp G).obj X = G.obj (F.obj X)
source
@[simp]
theorem prefunctor.comp_map {U : Type u_1} [quiver U] {V : Type u_3} [quiver V] {W : Type u_5} [quiver W] (F : prefunctor U V) (G : prefunctor V W) (X Y : U) (f : X ⟶ Y) :
(F.comp G).map f = G.map (F.map f)
source
@[protected, instance]
def quiver.opposite {V : Type u_1} [quiver V] :
quiver Vᵒᵖ

Vᵒᵖ reverses the direction of all arrows of V.

Equations
source
def quiver.hom.op {V : Type u_1} [quiver V] {X Y : V} (f : X ⟶ Y) :
opposite.op Y ⟶ opposite.op X

The opposite of an arrow in V.

Equations
source
def quiver.hom.unop {V : Type u_1} [quiver V] {X Y : Vᵒᵖ} (f : X ⟶ Y) :
opposite.unop Y ⟶ opposite.unop X

Given an arrow in Vᵒᵖ, we can take the "unopposite" back in V.

Equations
source
@[nolint]
def quiver.empty (V : Type u) :
Type u

A type synonym for a quiver with no arrows.

Equations
source
@[protected, instance]
def quiver.empty_quiver (V : Type u) :
quiver (quiver.empty V)
Equations
source
@[simp]
theorem quiver.empty_arrow {V : Type u} (a b : quiver.empty V) :
(a ⟶ b) = pempty