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

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.

## Instances

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

Unique (Quiver.Path (Quiver.root V) b)

## Equations

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

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 := ⋯ } }

## Instances For

`RootedConnected r`

means that there is a path from `r`

to any other vertex.

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

## Instances

theorem
Quiver.RootedConnected.nonempty_path
{V : Type u}
[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 ⋯

## Instances For

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

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}

## Instances For

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

## Equations

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