Documentation

Mathlib.Combinatorics.Quiver.Arborescence

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 #

• Quiver.Arborescence V: a typeclass asserting that V is an arborescence
• arborescenceMk: a convenient way of proving that a quiver is an arborescence
• RootedConnected r: a typeclass asserting that there is at least one path from r to b for every b.
• geodesicSubtree r: given [RootedConntected r], this is a subquiver of V which contains just enough edges to include a shortest path from r to b for every b.
• geodesicArborescence : Arborescence (geodesicSubtree r): an instance saying that the geodesic subtree is an arborescence. This proves the directed analogue of 'every connected graph has a spanning tree'. This proof avoids the use of Zorn's lemma.
class Quiver.Arborescence (V : Type u) [inst : ] :
Type (maxuv)
• The root of the arborescence.

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

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

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) [inst : ] [inst : ] :
V

The root of an arborescence.

Equations
• = Quiver.Arborescence.root
instance Quiver.instUniquePathRoot {V : Type u} [inst : ] [inst : ] (b : V) :
Equations
noncomputable def Quiver.arborescenceMk {V : Type u} [inst : ] (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.
Equations
• One or more equations did not get rendered due to their size.
class Quiver.RootedConnected {V : Type u} [inst : ] (r : V) :
• nonempty_path : ∀ (b : V), Nonempty ()

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

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

A path from r of minimal length.

Equations
theorem Quiver.shortest_path_spec {V : Type u} [inst : ] (r : V) [inst : ] {a : V} (p : ) :

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

def Quiver.geodesicSubtree {V : Type u} [inst : ] (r : V) [inst : ] :

A subquiver which by construction is an arborescence.

Equations
• = { e | p, }
noncomputable instance Quiver.geodesicArborescence {V : Type u} [inst : ] (r : V) [inst : ] :
Equations
• One or more equations did not get rendered due to their size.