mathlib documentation

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] :

The identity morphism between quivers.

Equations
@[simp]
theorem prefunctor.id_map (V : Type u_1) [quiver V] (X Y : V) (f : X Y) :
@[simp]
theorem prefunctor.id_obj (V : Type u_1) [quiver V] (a : V) :
@[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 : prefunctor U V) (G : prefunctor V 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 : prefunctor U V) (G : prefunctor V 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 : prefunctor U V) (G : prefunctor V 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.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]
Equations
@[instance]
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]
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

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

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)

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) :

An arrow viewed as a path of length one.

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

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 : quiver.path a b) (e : b c) :
(p.cons e).length = p.length + 1
def quiver.path.comp {V : Type u} [quiver V] {a b c : V} :
quiver.path a bquiver.path b cquiver.path a c

Composition of paths.

Equations
@[simp]
theorem quiver.path.comp_cons {V : Type u} [quiver V] {a b c d : V} (p : quiver.path a b) (q : quiver.path b 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 : quiver.path a b) :
@[simp]
theorem quiver.path.nil_comp {V : Type u} [quiver V] {a b : V} (p : quiver.path a b) :
@[simp]
theorem quiver.path.comp_assoc {V : Type u} [quiver V] {a b c d : V} (p : quiver.path a b) (q : quiver.path b c) (r : quiver.path c 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 : prefunctor V W) {a b : V} :
quiver.path a 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 : prefunctor V W) (a : V) :
@[simp]
theorem prefunctor.map_path_cons {V : Type u₁} [quiver V] {W : Type u₂} [quiver W] (F : prefunctor V W) {a b c : V} (p : quiver.path a 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 : prefunctor V W) {a b : V} (p : quiver.path a b) {c : V} (q : quiver.path b 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)

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] [quiver.arborescence V] :
V

The root of an arborescence.

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
@[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
@[class]
structure quiver.rooted_connected {V : Type u} [quiver V] (r : V) :
Prop

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) [quiver.rooted_connected r] (b : V) :

A path from r of minimal length.

Equations
theorem quiver.shortest_path_spec {V : Type u} [quiver V] (r : V) [quiver.rooted_connected r] {a : V} (p : quiver.path r a) :

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

A subquiver which by construction is an arborescence.

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
def quiver.reverse {V : Type u} [quiver V] [quiver.has_reverse V] {a b : V} :
(a b)(b a)

Reverse the direction of an arrow.

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

Reverse the direction of a path.

Equations
def quiver.zigzag_setoid (V : Type u) [quiver V] [quiver.has_reverse 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] [quiver.has_reverse 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

The weakly connected component corresponding to a vertex.

Equations