# mathlibdocumentation

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.

@[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 of this typeclass
Instances of other typeclasses for quiver
• quiver.has_sizeof_inst
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.

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

The identity morphism between quivers.

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

Composition of morphisms between quivers.

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

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

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

The opposite of an arrow in V.

Equations
Instances for quiver.hom.op
def quiver.hom.unop {V : Type u_1} [quiver V] {X Y : Vᵒᵖ} (f : X Y) :

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

Equations
Instances for quiver.hom.unop
@[nolint]
def quiver.empty (V : Type u) :
Type u

A type synonym for a quiver with no arrows.

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