# mathlibdocumentation

combinatorics.quiver

# 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
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.

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
@[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)
def wide_subquiver (V : Type u_1) [quiver V] :
Type (max u_1 v)

A wide subquiver H of G picks out a set H a b of arrows from a to b for every pair of vertices a b.

NB: this does not work for Prop-valued quivers. It requires G : quiver.{v+1} V.

Equations
@[nolint]
def wide_subquiver.to_Type (V : Type u) [quiver V] (H : wide_subquiver V) :
Type u

A type synonym for V, when thought of as a quiver having only the arrows from some wide_subquiver.

Equations
@[instance]
def wide_subquiver_has_coe_to_sort {V : Type u} [quiver V] :
Equations
@[instance]
def wide_subquiver.quiver {V : Type u_1} [quiver V] (H : wide_subquiver V) :

A wide subquiver viewed as a quiver on its own.

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

A type synonym for a quiver with no arrows.

Equations
@[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
@[instance]
def quiver.wide_subquiver.has_bot {V : Type u_1} [quiver V] :
Equations
@[instance]
def quiver.wide_subquiver.has_top {V : Type u_1} [quiver V] :
Equations
@[instance]
def quiver.wide_subquiver.inhabited {V : Type u_1} [quiver V] :
Equations
@[instance]
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
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
@[nolint]
def quiver.symmetrify (V : Type u) :
Type u

A type synonym for the symmetrized quiver (with an arrow both ways for each original arrow). NB: this does not work for Prop-valued quivers. It requires [quiver.{v+1} V].

Equations
@[instance]
def quiver.symmetrify_quiver (V : Type u) [quiver V] :
Equations
theorem quiver.total.ext {V : Type u} {_inst_1 : quiver V} (x y : quiver.total V) (h : x.left = y.left) (h_1 : x.right = y.right) (h_2 : x.hom == y.hom) :
x = y
@[nolint, ext]
structure quiver.total (V : Type u) [quiver V] :
Sort (max (u+1) v)

total V is the type of all arrows of V.

theorem quiver.total.ext_iff {V : Type u} {_inst_1 : quiver V} (x y : quiver.total V) :
x = y x.left = y.left x.right = y.right x.hom == y.hom
def quiver.wide_subquiver_symmetrify {V : Type u_1} [quiver V] :

A wide subquiver H of G.symmetrify determines a wide subquiver of G, containing an an arrow e if either e or its reversal is in H.

Equations
def quiver.wide_subquiver_equiv_set_total {V : Type u_1} [quiver V] :

A wide subquiver of G can equivalently be viewed as a total set of arrows.

Equations
inductive quiver.path {V : Type u} [quiver V] (a : V) :
V → Sort (max (u+1) v)
• nil : Π {V : Type u} [_inst_1 : quiver V] (a : V), a
• cons : Π {V : Type u} [_inst_1 : quiver V] (a : V) {b c : V}, b(b c) c

G.path a b is the type of paths from a to b through the arrows of G.

def quiver.hom.to_path {V : Type u_1} [quiver V] {a b : V} (e : a b) :
b

An arrow viewed as a path of length one.

Equations
def quiver.path.length {V : Type u} [quiver V] {a b : V} :
b

The length of a path is the number of arrows it uses.

Equations
@[simp]
theorem quiver.path.length_nil {V : Type u} [quiver V] {a : V} :
@[simp]
theorem quiver.path.length_cons {V : Type u} [quiver V] (a b c : V) (p : b) (e : b c) :
(p.cons e).length = p.length + 1
def quiver.path.comp {V : Type u} [quiver V] {a b c : V} :
b c c

Composition of paths.

Equations
@[simp]
theorem quiver.path.comp_cons {V : Type u} [quiver V] {a b c d : V} (p : b) (q : c) (e : c d) :
p.comp (q.cons e) = (p.comp q).cons e
@[simp]
theorem quiver.path.comp_nil {V : Type u} [quiver V] {a b : V} (p : b) :
@[simp]
theorem quiver.path.nil_comp {V : Type u} [quiver V] {a b : V} (p : b) :
@[simp]
theorem quiver.path.comp_assoc {V : Type u} [quiver V] {a b c d : V} (p : b) (q : c) (r : d) :
(p.comp q).comp r = p.comp (q.comp r)
def prefunctor.map_path {V : Type u₁} [quiver V] {W : Type u₂} [quiver W] (F : W) {a b : V} :
bquiver.path (F.obj a) (F.obj b)

The image of a path under a prefunctor.

Equations
@[simp]
theorem prefunctor.map_path_nil {V : Type u₁} [quiver V] {W : Type u₂} [quiver W] (F : W) (a : V) :
@[simp]
theorem prefunctor.map_path_cons {V : Type u₁} [quiver V] {W : Type u₂} [quiver W] (F : W) {a b c : V} (p : b) (e : b c) :
F.map_path (p.cons e) = (F.map_path p).cons (F.map e)
@[simp]
theorem prefunctor.map_path_comp {V : Type u₁} [quiver V] {W : Type u₂} [quiver W] (F : W) {a b : V} (p : b) {c : V} (q : c) :
F.map_path (p.comp q) = (F.map_path p).comp (F.map_path q)
@[class]
structure quiver.arborescence (V : Type u) [quiver V] :
Type (max u v)
• root : V
• unique_path : Π (b : V),

A quiver is an arborescence when there is a unique path from the default vertex to every other vertex.

Instances
def quiver.root (V : Type u) [quiver V]  :
V

The root of an arborescence.

Equations
@[instance]
def quiver.path.unique {V : Type u} [quiver V] (b : V) :
Equations
def quiver.labelling (V : Type u) [quiver V] (L : Sort u_2) :
Sort (imax (u+1) (u+1) u_1 u_2)

An L-labelling of a quiver assigns to every arrow an element of L.

Equations
• = Π ⦃a b : V⦄, (a b) → L
@[instance]
def quiver.labelling.inhabited {V : Type u} [quiver V] (L : Sort u_2) [inhabited L] :
Equations
def quiver.arborescence_mk {V : Type u} [quiver V] (r : V) (height : V → ) (height_lt : ∀ ⦃a b : V⦄, (a b)height a < height b) (unique_arrow : ∀ ⦃a b c : V⦄ (e : a c) (f : b c), a = b e == f) (root_or_arrow : ∀ (b : V), b = r ∃ (a : V), nonempty (a b)) :

To show that [quiver V] is an arborescence with root r : V, it suffices to

• provide a height function V → ℕ such that every arrow goes from a lower vertex to a higher vertex,
• show that every vertex has at most one arrow to it, and
• show that every vertex other than r has an arrow to it.
Equations
• height height_lt unique_arrow root_or_arrow = {root := r, unique_path := λ (b : V),
@[class]
structure quiver.rooted_connected {V : Type u} [quiver V] (r : V) :
Prop
• nonempty_path : ∀ (b : V), nonempty b)

rooted_connected r means that there is a path from r to any other vertex.

Instances
def quiver.shortest_path {V : Type u} [quiver V] (r : V) (b : V) :
b

A path from r of minimal length.

Equations
• = _
theorem quiver.shortest_path_spec {V : Type u} [quiver V] (r : V) {a : V} (p : a) :

The length of a path is at least the length of the shortest path

def quiver.geodesic_subtree {V : Type u} [quiver V] (r : V)  :

A subquiver which by construction is an arborescence.

Equations
• = λ (a b : V), {e : a b | ∃ (p : a), = p.cons e}
@[instance]
def quiver.geodesic_arborescence {V : Type u} [quiver V] (r : V)  :
Equations
@[class]
structure quiver.has_reverse (V : Type u) [quiver V] :
Type (max u v)
• reverse' : Π {a b : V}, (a b)(b a)

A quiver has_reverse if we can reverse an arrow p from a to b to get an arrow p.reverse from b to a.

Instances
@[instance]
def quiver.symmetrify.has_reverse (V : Type u) [quiver V] :
Equations
def quiver.reverse {V : Type u} [quiver V] {a b : V} :
(a b)(b a)

Reverse the direction of an arrow.

Equations
def quiver.path.reverse {V : Type u} [quiver V] {a b : V} :
b a

Reverse the direction of a path.

Equations
def quiver.zigzag_setoid (V : Type u) [quiver V]  :

Two vertices are related in the zigzag setoid if there is a zigzag of arrows from one to the other.

Equations
def quiver.weakly_connected_component (V : Type u) [quiver V]  :
Type u

The type of weakly connected components of a directed graph. Two vertices are in the same weakly connected component if there is a zigzag of arrows from one to the other.

Equations
def quiver.weakly_connected_component.mk {V : Type u} [quiver V]  :

The weakly connected component corresponding to a vertex.

Equations
@[instance]
Equations
@[instance]
Equations
theorem quiver.weakly_connected_component.eq {V : Type u} [quiver V] (a b : V) :