mathlib3 documentation


Arborescences #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

A quiver V is an arborescence (or directed rooted tree) when we have a root vertex root : V such that for every b : V there is a unique path from root to b.

Main definitions #

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 of this typeclass
Instances of other typeclasses for quiver.arborescence
  • quiver.arborescence.has_sizeof_inst
def quiver.root (V : Type u) [quiver V] [quiver.arborescence V] :

The root of an arborescence.

@[protected, instance]
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)) :

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

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

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

A path from r of minimal length.

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.

Instances for quiver.geodesic_subtree