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

prefunctor.id V = {obj := id V, map := λ (X Y : V) (f : X ⟶ Y), f}

@[simp]

theorem prefunctor.id_map (V : Type u_1) [quiver V] (X Y : V) (f : X ⟶ Y) :

(prefunctor.id V).map f = f

@[simp]

theorem prefunctor.id_obj (V : Type u_1) [quiver V] (a : V) :

(prefunctor.id V).obj a = id a

@[protected, instance]

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

inhabited (prefunctor V V)

Equations

prefunctor.inhabited V = {default := prefunctor.id V _inst_1}

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

F.comp G = {obj := λ (X : U), G.obj (F.obj X), map := λ (X Y : U) (f : X ⟶ Y), G.map (F.map f)}

@[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

wide_subquiver V = Π (a b : V), set (a ⟶ b)

@[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

wide_subquiver.to_Type V H = V

@[protected, instance]

def wide_subquiver_has_coe_to_sort {V : Type u} [quiver V] :

has_coe_to_sort (wide_subquiver V) (Type u)

Equations

wide_subquiver_has_coe_to_sort = {coe := λ (H : wide_subquiver V), wide_subquiver.to_Type V H}

@[protected, 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

H.quiver = {hom := λ (a b : ↥H), ↥(H a b)}

@[nolint]

def quiver.empty (V : Type u) :

Type u

A type synonym for a quiver with no arrows.

Equations

quiver.empty V = V

@[protected, instance]

def quiver.empty_quiver (V : Type u) :

quiver (quiver.empty V)

Equations

quiver.empty_quiver V = {hom := λ (a b : quiver.empty V), pempty}

@[simp]

theorem quiver.empty_arrow {V : Type u} (a b : quiver.empty V) :

(a ⟶ b) = pempty

@[protected, instance]

def quiver.wide_subquiver.has_bot {V : Type u_1} [quiver V] :

has_bot (wide_subquiver V)

Equations

quiver.wide_subquiver.has_bot = {bot := λ (a b : V), ∅}

@[protected, instance]

def quiver.wide_subquiver.has_top {V : Type u_1} [quiver V] :

has_top (wide_subquiver V)

Equations

quiver.wide_subquiver.has_top = {top := λ (a b : V), set.univ}

@[protected, instance]

def quiver.wide_subquiver.inhabited {V : Type u_1} [quiver V] :

inhabited (wide_subquiver V)

Equations

quiver.wide_subquiver.inhabited = {default := ⊤}

@[protected, instance]

def quiver.opposite {V : Type u_1} [quiver V] :

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

Equations

quiver.opposite = {hom := λ (a b : Vᵒᵖ), opposite.unop b ⟶ opposite.unop a}

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

f.op = f

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

f.unop = f

@[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

quiver.symmetrify V = V

@[protected, instance]

def quiver.symmetrify_quiver (V : Type u) [quiver V] :

quiver (quiver.symmetrify V)

Equations

quiver.symmetrify_quiver V = {hom := λ (a b : V), (a ⟶ b) ⊕ (b ⟶ a)}

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)

left : V
right : V
hom : self.left ⟶ self.right

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

wide_subquiver (quiver.symmetrify V) → wide_subquiver 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

quiver.wide_subquiver_symmetrify = λ (H : wide_subquiver (quiver.symmetrify V)) (a b : V), {e : a ⟶ b | sum.inl e ∈ H a b ∨ sum.inr e ∈ H b a}

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

wide_subquiver V ≃ set (quiver.total V)

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

Equations

quiver.wide_subquiver_equiv_set_total = {to_fun := λ (H : wide_subquiver V), {e : quiver.total V | e.hom ∈ H e.left e.right}, inv_fun := λ (S : set (quiver.total V)) (a b : V), {e : a ⟶ b | {left := a, right := b, hom := e} ∈ S}, left_inv := _, right_inv := _}

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), quiver.path a a
cons : Π {V : Type u} [_inst_1 : quiver V] (a : V) {b c : V}, quiver.path a b → (b ⟶ c) → quiver.path a 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) :

quiver.path a b

An arrow viewed as a path of length one.

Equations

e.to_path = quiver.path.nil.cons e

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

quiver.path a b → ℕ

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

Equations

(p.cons _x_1).length = p.length + 1
quiver.path.nil.length = 0

@[simp]

theorem quiver.path.length_nil {V : Type u} [quiver V] {a : V} :

quiver.path.nil.length = 0

@[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 b → quiver.path b c → quiver.path a c

Composition of paths.

Equations

p.comp (q.cons e) = (p.comp q).cons e
p.comp quiver.path.nil = p

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

p.comp quiver.path.nil = p

@[simp]

theorem quiver.path.nil_comp {V : Type u} [quiver V] {a b : V} (p : quiver.path a b) :

quiver.path.nil.comp p = p

@[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 b → quiver.path (F.obj a) (F.obj b)

The image of a path under a prefunctor.

Equations

F.map_path (p.cons e) = (F.map_path p).cons (F.map e)
F.map_path quiver.path.nil = quiver.path.nil

@[simp]

theorem prefunctor.map_path_nil {V : Type u₁} [quiver V] {W : Type u₂} [quiver W] (F : prefunctor V W) (a : V) :

F.map_path quiver.path.nil = quiver.path.nil

@[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)

root : V
unique_path : Π (b : V), unique (quiver.path quiver.arborescence.root b)

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

Instances

quiver.geodesic_arborescence

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

V

The root of an arborescence.

Equations

quiver.root V = quiver.arborescence.root

@[protected, instance]

def quiver.path.unique {V : Type u} [quiver V] [quiver.arborescence V] (b : V) :

unique (quiver.path (quiver.root V) b)

Equations

quiver.path.unique b = quiver.arborescence.unique_path b

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

quiver.labelling V L = Π ⦃a b : V⦄, (a ⟶ b) → L

@[protected, instance]

def quiver.labelling.inhabited {V : Type u} [quiver V] (L : Sort u_2) [inhabited L] :

inhabited (quiver.labelling V L)

Equations

quiver.labelling.inhabited L = {default := λ (a b : V) (e : a ⟶ b), default L}

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

quiver.arborescence V

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

quiver.arborescence_mk r height height_lt unique_arrow root_or_arrow = {root := r, unique_path := λ (b : V), {to_inhabited := classical.inhabited_of_nonempty _, uniq := _}}

@[class]

structure quiver.rooted_connected {V : Type u} [quiver V] (r : V) :

Prop

nonempty_path : ∀ (b : V), nonempty (quiver.path r b)

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

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

quiver.path r b

A path from r of minimal length.

Equations

quiver.shortest_path r b = _.min set.univ _

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

(quiver.shortest_path r a).length ≤ p.length

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

wide_subquiver V

A subquiver which by construction is an arborescence.

Equations

quiver.geodesic_subtree r = λ (a b : V), {e : a ⟶ b | ∃ (p : quiver.path r a), quiver.shortest_path r b = p.cons e}

@[protected, instance]

noncomputable def quiver.geodesic_arborescence {V : Type u} [quiver V] (r : V) [quiver.rooted_connected r] :

quiver.arborescence ↥(quiver.geodesic_subtree r)

Equations

quiver.geodesic_arborescence r = quiver.arborescence_mk r (λ (a : ↥(quiver.geodesic_subtree r)), (quiver.shortest_path r a).length) _ _ _

@[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

quiver.symmetrify.has_reverse

@[protected, instance]

def quiver.symmetrify.has_reverse (V : Type u) [quiver V] :

quiver.has_reverse (quiver.symmetrify V)

Equations

quiver.symmetrify.has_reverse V = {reverse' := λ (a b : quiver.symmetrify V) (e : a ⟶ b), sum.swap e}

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

quiver.reverse = quiver.has_reverse.reverse'

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

quiver.path a b → quiver.path b a

Reverse the direction of a path.

Equations

(p.cons e).reverse = (quiver.reverse e).to_path.comp p.reverse
quiver.path.nil.reverse = quiver.path.nil

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

quiver.zigzag_setoid V = {r := λ (a b : V), nonempty (quiver.path a b), iseqv := _}

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

quiver.weakly_connected_component V = quotient (quiver.zigzag_setoid V)

@[protected]

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

V → quiver.weakly_connected_component V

The weakly connected component corresponding to a vertex.

Equations

quiver.weakly_connected_component.mk = quotient.mk'

@[protected, instance]

def quiver.weakly_connected_component.has_coe_t {V : Type u} [quiver V] [quiver.has_reverse V] :

has_coe_t V (quiver.weakly_connected_component V)

Equations

quiver.weakly_connected_component.has_coe_t = {coe := quiver.weakly_connected_component.mk _inst_2}

@[protected, instance]

def quiver.weakly_connected_component.inhabited {V : Type u} [quiver V] [quiver.has_reverse V] [inhabited V] :

inhabited (quiver.weakly_connected_component V)

Equations

quiver.weakly_connected_component.inhabited = {default := ↑(default V)}

@[protected]

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

↑a = ↑b ↔ nonempty (quiver.path a b)