Godsil's path tree

The path tree T(G, u) of a graph G at a vertex u has as vertices the paths of G starting at u; two paths are adjacent when one extends the other by one edge. It is a forest (indeed a tree) rooted at the trivial path.

Main definitions

• SimpleGraph.PathFrom G u: the paths of G starting at u, as Σ v, G.Path u v.
• SimpleGraph.Grows a b: b extends a by one edge.
• SimpleGraph.pathTree G u: the path tree.
• SimpleGraph.pathTreeRoot G u: its root, the trivial path.
• SimpleGraph.prependRoot G hub: prepending the edge u b to a path of G - u from b.

Main results

• SimpleGraph.pathTree_isAcyclic: the path tree is acyclic.
• SimpleGraph.Grows.parent_unique: every path has at most one parent.
• SimpleGraph.prependRoot_injective, SimpleGraph.prependRoot_grows: prepending the root edge is injective and preserves the tree structure.

References

• C. D. Godsil, Matchings and walks in graphs, J. Graph Theory 5 (1981) 285–297.

@[reducible, inline]

abbrev SimpleGraph.PathFrom {V : Type u_1} (G : SimpleGraph V) (u : V) : Type u_1

A path of G starting at u (with its endpoint), the vertex type of the path tree. PathFrom G u := Σ v, G.Path u v.

Equations

• G.PathFrom u = ((v : V) × G.Path u v)

@[reducible, inline]

abbrev SimpleGraph.PathFrom.length {V : Type u_1} {G : SimpleGraph V} {u : V} (a : G.PathFrom u) : ℕ

The length (number of edges) of a path-tree vertex.

Equations

• a.length = (↑a.snd).length

def SimpleGraph.Grows {V : Type u_1} {G : SimpleGraph V} {u : V} (a b : G.PathFrom u) : Prop

b grows from a: b is a with one further edge appended at the end. This is the (directed) covering relation of the path tree.

Equations

• SimpleGraph.Grows a b = ∃ (he : G.Adj a.fst b.fst), ↑b.snd = (↑a.snd).concat he

def SimpleGraph.pathTree {V : Type u_1} (G : SimpleGraph V) (u : V) : SimpleGraph (G.PathFrom u)

Godsil's path tree T(G, u). Vertices are paths of G starting at u; two are adjacent when one extends the other by a single edge.

Equations

• G.pathTree u = { Adj := fun (a b : G.PathFrom u) => SimpleGraph.Grows a b ∨ SimpleGraph.Grows b a, symm := ⋯, loopless := ⋯ }

@[simp]

theorem SimpleGraph.pathTree_adj {V : Type u_1} {G : SimpleGraph V} {u : V} (a b : G.PathFrom u) : (G.pathTree u).Adj a b ↔ Grows a b ∨ Grows b a

def SimpleGraph.pathTreeRoot {V : Type u_1} (G : SimpleGraph V) (u : V) : G.PathFrom u

The root of the path tree: the trivial path at u.

Equations

• G.pathTreeRoot u = ⟨u, SimpleGraph.Path.nil⟩

Structural lemmas: length, parent

theorem SimpleGraph.Grows.length_eq {V : Type u_1} {G : SimpleGraph V} {u : V} {a b : G.PathFrom u} (h : Grows a b) : b.length = a.length + 1

Growing adds exactly one edge: length b = length a + 1.

theorem SimpleGraph.pathTree_adj_length {V : Type u_1} {G : SimpleGraph V} {u : V} {a b : G.PathFrom u} (h : (G.pathTree u).Adj a b) : b.length = a.length + 1 ∨ a.length = b.length + 1

Adjacent path-tree vertices differ in length by exactly one.

theorem SimpleGraph.Grows.parent_unique {V : Type u_1} {G : SimpleGraph V} {u : V} {a a' b : G.PathFrom u} (h : Grows a b) (h' : Grows a' b) : a = a'

Uniqueness of the down-neighbour (parent). If b grows from both a and a' then a = a': the parent of a path is unique (it is dropLast). The key reason the path tree branches only upward — the heart of acyclicity.

The path tree is a forest

theorem SimpleGraph.pathTree_isAcyclic {V : Type u_1} (G : SimpleGraph V) (u : V) : (G.pathTree u).IsAcyclic

T(G, u) is acyclic — a forest. Suppose a cycle existed. Rotate it to start at a vertex m of maximal path-length in the cycle. Both cycle-neighbours of m (its snd and penultimate) then have length ≤ m, so — adjacency changing length by exactly one — each has length m − 1, i.e. each grows into m. Hence each is a parent of m; by Grows.parent_unique they coincide. But a cycle's second and penultimate vertices are distinct (IsCycle.snd_ne_penultimate). Contradiction. So no cycle exists, and the path tree is a forest — exactly what makes μ(T(G,u)) the characteristic polynomial of a symmetric matrix, hence real-rooted.

Root decomposition T(G,u) − r ≅ ⊔_{b∼u} T(G−u, b) — the child embedding

Removing the root r = (u) from T(G,u) leaves, hanging from each child (u,b) (b ∼ u), the subtree of paths through that edge. That subtree is T(G−u, b): a path of G from u with second vertex b is exactly u prepended to a path of G−u from b (u is never revisited, so the tail lives in G−u). prependRoot is this injection; assembling it over all b ∼ u (plus the isolated r) gives the decomposition, hence — via matchingPoly_sum — μ(T−r) = X·∏_{b∼u} μ(T(G−u,b)), the product step of Godsil's divisibility.

theorem SimpleGraph.isolated_not_mem_support {W : Type u_2} {H : SimpleGraph W} {x : W} (hx : H.IsIsolated x) {a c : W} (p : H.Walk a c) : a ≠ x → x ∉ p.support

A walk starting at a ≠ x never visits an isolated vertex x.

def SimpleGraph.prependRoot {V : Type u_1} (G : SimpleGraph V) {u b : V} (hub : G.Adj u b) (p : (G.deleteIncidenceSet u).PathFrom b) : G.PathFrom u

Child embedding. Prepend the root edge u–b to a path of G−u starting at b, giving a path of G from u with second vertex b — the branch of T(G,u) hanging from the root's child (u,b), identified with T(G−u, b).

Equations

• G.prependRoot hub p = ⟨p.fst, ⟨SimpleGraph.Walk.cons hub (SimpleGraph.Walk.mapLe ⋯ ↑p.snd), ⋯⟩⟩

theorem SimpleGraph.prependRoot_injective {V : Type u_1} (G : SimpleGraph V) {u b : V} (hub : G.Adj u b) : Function.Injective (G.prependRoot hub)

The child embedding is injective: distinct subtree paths give distinct paths of G.

theorem SimpleGraph.mapLe_concat {W : Type u_2} {H H' : SimpleGraph W} (hle : H ≤ H') {a c d : W} (w : H.Walk a c) (hc : H.Adj c d) (hc' : H'.Adj c d) : Walk.mapLe hle (w.concat hc) = (Walk.mapLe hle w).concat hc'

mapLe distributes over concat (all rfl-glued except map_append); the target edge hc' is supplied at the same endpoints, so no ofLE-coercion leaks into the type.

theorem SimpleGraph.pathFrom_fst_ne {V : Type u_1} (G : SimpleGraph V) {u b : V} (hub : G.Adj u b) (p : (G.deleteIncidenceSet u).PathFrom b) : p.fst ≠ u

An endpoint of a path of G−u from b ∼ u is never u: it lies in the walk's support, and u is isolated in G−u.

theorem SimpleGraph.prependRoot_grows {V : Type u_1} (G : SimpleGraph V) {u b : V} (hub : G.Adj u b) (p q : (G.deleteIncidenceSet u).PathFrom b) : Grows (G.prependRoot hub p) (G.prependRoot hub q) ↔ Grows p q

Grows-compatibility of the child embedding. prependRoot both preserves and reflects the covering relation Grows, so it is an isomorphism of the subtree T(G−u, b) onto the branch of T(G,u) hanging from the root's child (u,b). The forward direction reconciles adjacency (G.Adj p.1 q.1 ⟹ (G−u).Adj p.1 q.1, valid since neither endpoint is u) and cancels the prepended root edge; both use that mapLe commutes with concat.