Arborescences #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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
arborescence_mk: a convenient way of proving that a quiver is an arborescence
rooted_connected r: a typeclass asserting that there is at least one path from r to b for every b.
geodesic_subtree r: given [rooted_conntected r], this is a subquiver of V which contains just enough edges to include a shortest path from r to b for every b.
geodesic_arborescence : arborescence (geodesic_subtree 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.

source

@[class]

structure quiver.arborescence (V : Type u) [quiver V] :

Type (max u v)

root : V
unique_path : Π (b : V), unique (quiver.path quiver.arborescence.root b)

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

Instances of this typeclass

quiver.geodesic_arborescence

Instances of other typeclasses for quiver.arborescence

quiver.arborescence.has_sizeof_inst

source

def quiver.root (V : Type u) [quiver V] [quiver.arborescence V] :

The root of an arborescence.

Equations

quiver.root V = quiver.arborescence.root

source

@[protected, instance]

def quiver.path.unique {V : Type u} [quiver V] [quiver.arborescence V] (b : V) :

unique (quiver.path (quiver.root V) b)

Equations

quiver.path.unique b = quiver.arborescence.unique_path b

source

noncomputable def quiver.arborescence_mk {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 ∧ 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.arborescence_mk r height height_lt unique_arrow root_or_arrow = {root := r, unique_path := λ (b : V), {to_inhabited := classical.inhabited_of_nonempty _, uniq := _}}

source

@[class]

structure quiver.rooted_connected {V : Type u} [quiver V] (r : V) :

Prop

nonempty_path : ∀ (b : V), nonempty (quiver.path r b)

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

Instances of this typeclass

is_free_groupoid.generators_connected

source

noncomputable def quiver.shortest_path {V : Type u} [quiver V] (r : V) [quiver.rooted_connected r] (b : V) :

quiver.path r b

A path from r of minimal length.

Equations

quiver.shortest_path r b = _.min set.univ _

source

theorem quiver.shortest_path_spec {V : Type u} [quiver V] (r : V) [quiver.rooted_connected r] {a : V} (p : quiver.path r a) :

(quiver.shortest_path r a).length ≤ p.length

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

source

def quiver.geodesic_subtree {V : Type u} [quiver V] (r : V) [quiver.rooted_connected r] :

wide_subquiver V

A subquiver which by construction is an arborescence.

Equations

quiver.geodesic_subtree r = λ (a b : V), {e : a ⟶ b | ∃ (p : quiver.path r a), quiver.shortest_path r b = p.cons e}

Instances for ↥quiver.geodesic_subtree

quiver.geodesic_arborescence

source

@[protected, instance]

noncomputable def quiver.geodesic_arborescence {V : Type u} [quiver V] (r : V) [quiver.rooted_connected r] :

quiver.arborescence ↥(quiver.geodesic_subtree r)

Equations

quiver.geodesic_arborescence r = quiver.arborescence_mk r (λ (a : ↥(quiver.geodesic_subtree r)), (quiver.shortest_path r a).length) _ _ _