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 [RootedConnected 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) [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.

• 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.

def Quiver.root (V : Type u) [Quiver V] [Quiver.Arborescence V] : V

The root of an arborescence.

Equations

• Quiver.root V = Quiver.Arborescence.root

instance Quiver.instUniquePathRoot {V : Type u} [Quiver V] [Quiver.Arborescence V] (b : V) : Unique (Quiver.Path (Quiver.root V) b)

Equations

• Quiver.instUniquePathRoot b = Quiver.Arborescence.uniquePath b

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 : 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.arborescenceMk r height height_lt unique_arrow root_or_arrow = { root := r, uniquePath := fun (b : V) => { toInhabited := Classical.inhabited_of_nonempty ⋯, uniq := ⋯ } }

class Quiver.RootedConnected {V : Type u} [Quiver V] (r : V) : Prop

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

• nonempty_path : ∀ (b : V), Nonempty (Quiver.Path r b)

theorem Quiver.RootedConnected.nonempty_path {V : Type u} : ∀ {inst : Quiver V} {r : V} [self : Quiver.RootedConnected r] (b : V), Nonempty (Quiver.Path r b)

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

A path from r of minimal length.

Equations

• Quiver.shortestPath r b = ⋯.min Set.univ ⋯

theorem Quiver.shortest_path_spec {V : Type u} [Quiver V] (r : V) [Quiver.RootedConnected r] {a : V} (p : Quiver.Path r a) : (Quiver.shortestPath r a).length ≤ p.length

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

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

A subquiver which by construction is an arborescence.

Equations

• Quiver.geodesicSubtree r a b = {e : a ⟶ b | ∃ (p : Quiver.Path r a), Quiver.shortestPath r b = p.cons e}

noncomputable instance Quiver.geodesicArborescence {V : Type u} [Quiver V] (r : V) [Quiver.RootedConnected r] : Quiver.Arborescence (WideSubquiver.toType V (Quiver.geodesicSubtree r))

Equations

• Quiver.geodesicArborescence r = Quiver.arborescenceMk r (fun (a : WideSubquiver.toType V (Quiver.geodesicSubtree r)) => (Quiver.shortestPath r a).length) ⋯ ⋯ ⋯