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

The root of the arborescence.

root : VThere 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

The root of an arborescence.

## Equations

- Quiver.root V = Quiver.Arborescence.root

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

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

## Equations

noncomputable def
Quiver.arborescenceMk
{V : Type u}
[inst : 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.

## Equations

- One or more equations did not get rendered due to their size.

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

`RootedConnected r`

means that there is a path from `r`

to any other vertex.

## Instances

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

Quiver.Path r b

A path from `r`

of minimal length.

## Equations

- Quiver.shortestPath r b = WellFounded.min (_ : WellFounded WellFoundedRelation.rel) Set.univ (_ : Set.Nonempty Set.univ)

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

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

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

A subquiver which by construction is an arborescence.

## Equations

- Quiver.geodesicSubtree r a b = { e | ∃ p, Quiver.shortestPath r b = Quiver.Path.cons p e }

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

## Equations

- One or more equations did not get rendered due to their size.