Components left by deleting a branch vertex of a tree

Deleting a vertex c from a tree separates it into one component for each neighbour of c. When every vertex of the complement has degree at most two there, the resulting components are paths. This is the graph-theoretic extraction step behind the D and E branches of the finite-type Dynkin-diagram classification.

Main results

• TauCeti.IsTree.neighborSetEquivConnectedComponentCompl: the neighbours of a vertex index the connected components left after deleting that vertex from a tree.
• TauCeti.IsTree.exists_equiv_pathGraph_components: deleting a vertex of degree n from a finite tree leaves n components, each a path when the complement has degree at most two.

References

See J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, Section 11.4, for the corresponding extraction in the classification of Dynkin diagrams.

noncomputable def TauCeti.IsTree.neighborSetEquivConnectedComponentCompl {V : Type u_1} {G : SimpleGraph V} (hG : G.IsTree) (c : V) : ↑(G.neighborSet c) ≃ (SimpleGraph.induce {c}ᶜ G).ConnectedComponent

The components of a tree with one vertex deleted are indexed by its neighbours.

The forward map sends a neighbour of c to the component of the graph induced on {c}ᶜ that contains it; the inverse sends a component to the unique neighbour of c that it contains.

Equations

• TauCeti.IsTree.neighborSetEquivConnectedComponentCompl hG c = Equiv.ofBijective (fun (x : ↑(G.neighborSet c)) => (SimpleGraph.induce {c}ᶜ G).connectedComponentMk ⟨↑x, ⋯⟩) ⋯

@[simp]

theorem TauCeti.IsTree.neighborSetEquivConnectedComponentCompl_apply {V : Type u_1} {G : SimpleGraph V} (hG : G.IsTree) (c : V) (x : ↑(G.neighborSet c)) : (neighborSetEquivConnectedComponentCompl hG c) x = (SimpleGraph.induce {c}ᶜ G).connectedComponentMk ⟨↑x, ⋯⟩

The equivalence sends a neighbour to the connected component containing that neighbour.

theorem TauCeti.IsTree.exists_equiv_pathGraph_components {V : Type u_1} {G : SimpleGraph V} [Fintype V] [DecidableEq V] [DecidableRel G.Adj] (hG : G.IsTree) (c : V) {n : ℕ} (hc : G.degree c = n) (hdeg : ∀ (v : ↑{c}ᶜ), (SimpleGraph.induce {c}ᶜ G).degree v ≤ 2) : ∃ (e : Fin n ≃ (SimpleGraph.induce {c}ᶜ G).ConnectedComponent), ∀ (i : Fin n), Nonempty ((e i).toSimpleGraph ≃g SimpleGraph.pathGraph (Nat.card ↑(e i).supp))

Deleting a vertex of degree n from a finite tree leaves n components, and they are paths as soon as the complement has degree at most two.

The equivalence e records which component begins at each neighbour of c. The second conclusion is deliberately componentwise: each component carries its own natural path length, which is the arm length used in the subsequent reindexing onto a star.