Arborescences #

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 #

class Quiver.Arborescence (V : Type u) [Quiver V] :
Type (max u v)
  • root : V

    The root of the arborescence.

  • uniquePath : (b : V) → Unique (Quiver.Path Quiver.Arborescence.root b)

    There is a unique path from the root to any other vertex.

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


    The root of an arborescence.

    Instances For
      noncomputable def Quiver.arborescenceMk {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 HEq e f) (root_or_arrow : ∀ (b : V), b = r a, 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.
      Instances For
        class Quiver.RootedConnected {V : Type u} [Quiver V] (r : V) :

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

          noncomputable def Quiver.shortestPath {V : Type u} [Quiver V] (r : V) [Quiver.RootedConnected r] (b : V) :

          A path from r of minimal length.

          Instances For

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

            A subquiver which by construction is an arborescence.

            Instances For