The three arms of a branch diagram

A diagram which is a tree of maximum degree three, with a single vertex of degree three, becomes three paths when that vertex is deleted: the general tree decomposition from TauCeti.Combinatorics.SimpleGraph.BranchComponents applies, because deleting the branch vertex leaves every other vertex with degree at most two.

For a connected simply-laced finite-type diagram with a branch vertex the hypotheses hold: the finite-type degree bound supplies degree at most three, and the affine D obstruction in TauCeti.LinearAlgebra.RootSystem.FiniteType.Star.UniqueBranch says that the branch vertex is the only vertex of degree three. The statement is kept free of the finite-type hypothesis so that it also applies to diagrams not yet known to be of finite type.

This is the extraction step connecting branch diagrams to the model stars classified in TauCeti.LinearAlgebra.RootSystem.FiniteType.Star.Classification. The next step attaches each path to the deleted vertex and reindexes the matrix onto starCartanMatrix.

Main result

• TauCeti.exists_three_path_components_of_isTree: deleting the unique branch vertex from a diagram which is a tree of maximum degree three leaves three path components.

References

This is the simply-laced extraction step in Layer 5 of the root-systems roadmap. See J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, Section 11.4, and Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Chapter VI, Section 4.

theorem TauCeti.exists_three_path_components_of_isTree {B : Type u_1} [Fintype B] [DecidableEq B] {A : Matrix B B ℤ} (htree : (diagramGraph A).IsTree) (hdeg : ∀ (v : B), (diagramGraph A).degree v ≤ 3) {c : B} (hc : (diagramGraph A).degree c = 3) (huniq : ∀ (v : B), (diagramGraph A).degree v = 3 → v = c) : ∃ (e : Fin 3 ≃ (SimpleGraph.induce {c}ᶜ (diagramGraph A)).ConnectedComponent), ∀ (i : Fin 3), Nonempty ((e i).toSimpleGraph ≃g SimpleGraph.pathGraph (Nat.card ↥(e i)))

Deleting the branch vertex of a tree diagram of maximum degree three leaves three paths.

The branch vertex c is assumed to be the only vertex of degree three. The equivalence indexes the components by Fin 3; the component at i is a path graph on its own number of vertices. These cardinalities are the three arm lengths in the subsequent reindexing onto TauCeti.starCartanMatrix.