Rooting trees and parent arrays

Two ways of presenting a rooted tree.

• Rooting a tree. For a tree T on ι and a root r, SimpleGraph.IsTree.pathTo hT r t is the unique path from t to r. SimpleGraph.IsTree.parent hT r t is its second vertex: the neighbour of t on the way to r, or r itself when t = r. Every edge of T joins a vertex to its parent (SimpleGraph.IsTree.adj_iff_parent), and the parent is one step closer to the root (SimpleGraph.IsTree.length_pathTo_parent).
• Parent arrays. A map p : Fin (n + 1) → Fin (n + 1) with p i < i for every i ≠ 0 determines the graph SimpleGraph.parentTree p, which joins each i ≠ 0 to p i. It is a tree (SimpleGraph.parentTree_isTree). In such a tree a preconnected vertex set has at most one vertex whose parent lies outside it (SimpleGraph.eq_of_preconnected_parentTree).

Parent arrays are the input format of tree-decomposition algorithms; rooting is how an arbitrary finite tree is brought into that format.

Main definitions

• SimpleGraph.IsTree.pathTo, SimpleGraph.IsTree.parent: rooting a tree.
• SimpleGraph.parentTree: the tree of a parent array.
• SimpleGraph.parentGraph: the graph of a parent function on any vertex type.

Main results

• SimpleGraph.IsTree.adj_iff_parent: the edges of a rooted tree are the parent edges.
• SimpleGraph.parentTree_isTree: a parent array with p i < i for i ≠ 0 gives a tree.
• SimpleGraph.eq_of_preconnected_parentTree: a preconnected set in a parent-array tree has a unique topmost vertex.
• SimpleGraph.parentTree_eq_parentGraph: the two parent graphs agree when p 0 = 0.

Rooting a tree

noncomputable def SimpleGraph.IsTree.pathTo {ι : Type uι} {T : SimpleGraph ι} (hT : T.IsTree) (r t : ι) : T.Walk t r

The unique path in the tree T from t to the root r.

theorem SimpleGraph.IsTree.isPath_pathTo {ι : Type uι} {T : SimpleGraph ι} (hT : T.IsTree) (r t : ι) : (hT.pathTo r t).IsPath

theorem SimpleGraph.IsTree.eq_pathTo {ι : Type uι} {T : SimpleGraph ι} (hT : T.IsTree) (r : ι) {t : ι} {q : T.Walk t r} (hq : q.IsPath) : q = hT.pathTo r t

noncomputable def SimpleGraph.IsTree.parent {ι : Type uι} {T : SimpleGraph ι} (hT : T.IsTree) (r t : ι) : ι

The parent of t when T is rooted at r: the second vertex of the path from t to r, or r itself when t = r.

@[simp]

theorem SimpleGraph.IsTree.pathTo_self {ι : Type uι} {T : SimpleGraph ι} (hT : T.IsTree) (r : ι) : hT.pathTo r r = Walk.nil

@[simp]

theorem SimpleGraph.IsTree.parent_self {ι : Type uι} {T : SimpleGraph ι} (hT : T.IsTree) (r : ι) : hT.parent r r = r

theorem SimpleGraph.IsTree.adj_parent {ι : Type uι} {T : SimpleGraph ι} (hT : T.IsTree) (r : ι) {t : ι} (ht : t ≠ r) : T.Adj t (hT.parent r t)

theorem SimpleGraph.IsTree.length_pathTo_parent {ι : Type uι} {T : SimpleGraph ι} (hT : T.IsTree) (r : ι) {t : ι} (ht : t ≠ r) : (hT.pathTo r (hT.parent r t)).length + 1 = (hT.pathTo r t).length

The parent of a non-root vertex is one step closer to the root.

theorem SimpleGraph.IsTree.adj_iff_parent {ι : Type uι} {T : SimpleGraph ι} (hT : T.IsTree) (r : ι) {x y : ι} : T.Adj x y ↔ x ≠ r ∧ hT.parent r x = y ∨ y ≠ r ∧ hT.parent r y = x

Every edge of a rooted tree joins a non-root vertex to its parent.

Parent arrays

def SimpleGraph.parentTree {n : ℕ} (p : Fin (n + 1) → Fin (n + 1)) : SimpleGraph (Fin (n + 1))

The graph of a parent array on Fin (n + 1): each i ≠ 0 is joined to p i. When p i < i for every i ≠ 0 this is a tree rooted at 0 (parentTree_isTree).

def SimpleGraph.parentGraph {ι : Type uι} (p : ι → ι) : SimpleGraph ι

The graph of a parent function p : ι → ι on any vertex type: x and y are adjacent when one is the parent of the other. Fixed points of p (roots) give no self-loops. Unlike parentTree, there is no fixed root and no order condition; when p 0 = 0 the two graphs agree (parentTree_eq_parentGraph).

theorem SimpleGraph.parentGraph_adj {ι : Type uι} {p : ι → ι} {x y : ι} : (parentGraph p).Adj x y ↔ x ≠ y ∧ (p x = y ∨ p y = x)

theorem SimpleGraph.parentTree_eq_parentGraph {n : ℕ} {p : Fin (n + 1) → Fin (n + 1)} (h0 : p 0 = 0) : parentTree p = parentGraph p

A parent array whose root 0 is its own parent has the same graph as its parent function.

theorem SimpleGraph.parentTree_adj {n : ℕ} {p : Fin (n + 1) → Fin (n + 1)} (hlt : ∀ (i : Fin (n + 1)), i ≠ 0 → p i < i) {i j : Fin (n + 1)} : (parentTree p).Adj i j ↔ i ≠ 0 ∧ p i = j ∨ j ≠ 0 ∧ p j = i

theorem SimpleGraph.parentTree_adj_self {n : ℕ} {p : Fin (n + 1) → Fin (n + 1)} (hlt : ∀ (i : Fin (n + 1)), i ≠ 0 → p i < i) {i : Fin (n + 1)} (hi : i ≠ 0) : (parentTree p).Adj i (p i)

theorem SimpleGraph.parentTree_isTree {n : ℕ} {p : Fin (n + 1) → Fin (n + 1)} (hlt : ∀ (i : Fin (n + 1)), i ≠ 0 → p i < i) : (parentTree p).IsTree

A parent array with p i < i for every i ≠ 0 describes a tree.

theorem SimpleGraph.eq_of_preconnected_parentTree {n : ℕ} {p : Fin (n + 1) → Fin (n + 1)} (h0 : p 0 = 0) (hlt : ∀ (i : Fin (n + 1)), i ≠ 0 → p i < i) {S : Set (Fin (n + 1))} (hS : (induce S (parentTree p)).Preconnected) {a b : Fin (n + 1)} (ha : a ∈ S) (hat : a = 0 ∨ p a ∉ S) (hb : b ∈ S) (hbt : b = 0 ∨ p b ∉ S) : a = b

In a parent-array tree, a preconnected vertex set has at most one topmost element: one that is the root 0 or whose parent lies outside the set.