A finite tree of maximum degree two is a path graph #

A finite connected graph in which every vertex has at most two neighbours is a path or a cycle, and acyclicity leaves the path. This file proves that identification in the form a consumer wants: a finite tree of maximum degree two is isomorphic to Mathlib's SimpleGraph.pathGraph on as many vertices as it has, so its vertices can be numbered 0, …, n - 1 with two of them adjacent exactly when their numbers are consecutive.

The proof takes a path p of greatest length in the graph, which Mathlib's SimpleGraph.exists_isPath_forall_isPath_length_le_length supplies. Every neighbour of a vertex of p again lies on p: at an interior vertex because the two neighbours along p already exhaust the degree bound, and at an endpoint because a neighbour off p could be prepended, contradicting maximality. The vertices of p therefore admit no boundary edge, so connectedness makes them all of the vertices, and a count of edges finishes the argument: a tree has one edge fewer than it has vertices, p already supplies that many distinct edges, and so every edge of the graph is an edge of p. The subgraph spanned by p is therefore all of G, and Mathlib's SimpleGraph.Walk.IsPath.pathGraphIsoToSubgraph identifies it with a path graph.

Main results #

TauCeti.IsTree.nonempty_iso_pathGraph_of_degree_le_two: a finite tree of maximum degree two is isomorphic to the path graph on its vertices.
TauCeti.adj_iff_of_iso_pathGraph: adjacency read through such a numbering is consecutiveness of the numbers.
TauCeti.pathGraphRevIso: the reversal automorphism of a path graph, which reverses a numbering.

References #

The argument is the standard one; see R. Diestel, Graph Theory, 5th ed., Ch. 1.5, for trees and their edge count.

Numbering a graph as a path #

source

theorem TauCeti.adj_iff_of_iso_pathGraph {V : Type u_1} {G : SimpleGraph V} {n : ℕ} (f : G ≃g SimpleGraph.pathGraph n) (i j : V) :

G.Adj i j ↔ ↑(f i) + 1 = ↑(f j) ∨ ↑(f j) + 1 = ↑(f i)

Adjacency read through a numbering of a graph as a path: two vertices are adjacent exactly when their numbers are consecutive.

source

def TauCeti.pathGraphRevIso (n : ℕ) :

SimpleGraph.pathGraph n ≃g SimpleGraph.pathGraph n

Reversal is an automorphism of a path graph. Composing with it reverses a numbering of a graph as a path. The body is exported unexposed, so pathGraphRevIso_apply is the interface an importing module computes with.

Equations

TauCeti.pathGraphRevIso n = { toEquiv := Fin.revPerm, map_rel_iff' := ⋯ }

Instances For

source

@[simp]

theorem TauCeti.pathGraphRevIso_apply {n : ℕ} (i : Fin n) :

(pathGraphRevIso n) i = i.rev