A finite-type component with a double edge has no branch vertex

The double-edge branch of the Cartan--Killing classification is already classified once its diagram is known to be a path. This file supplies the missing global extraction: a connected finite-type diagram containing a double edge has maximum degree two.

Suppose instead that c has degree three. Follow the unique path from c to the farther endpoint of the double edge and retain two unused neighbours of c. These vertices have the shape of the affine diagram B̃ₗ, or its transpose according to the orientation of the double edge. The selected principal submatrix need not equal the affine Cartan matrix: intervening edges might still be multiple. What is enough, and avoids assuming their uniqueness, is that it is entrywise at most the affine matrix. The positive comark vector TauCeti.affineBComark is therefore subdominant for the selected matrix, contradicting finite type.

Combining the degree bound with the existing branchless theorem gives the unrestricted classification of the double-edge case into the B, C, and F₄ shapes.

Main results

• TauCeti.IsFiniteType.degree_le_two_of_reachable_of_apply_mul_apply_eq_two: a finite-type component containing a double edge has no branch vertex.
• TauCeti.IsFiniteType.degree_le_two_of_apply_mul_apply_eq_two: the connected specialization.
• TauCeti.IsFiniteType.exists_equiv_forall_eq_doubleEdgeCartanMatrix_of_apply_mul_apply_eq_two: the component is a double-edge chain of type B, C, or F₄.

References

This is the multiple-edge extraction step in Layer 5 of TauCetiRoadmap/RepresentationTheory/RootSystems/README.md. The affine-diagram exclusion is the argument in J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, Section 11.4, and N. Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Chapter VI, Section 4.

theorem TauCeti.IsFiniteType.degree_le_two_of_reachable_of_apply_mul_apply_eq_two {B : Type u_1} [DecidableEq B] {A : Matrix B B ℤ} [Fintype B] (h : IsFiniteType A) {u v c : B} (hreach : (diagramGraph A).Reachable c u) (huv : A u v * A v u = 2) : (diagramGraph A).degree c ≤ 2

A finite-type component containing a double edge has maximum degree two.

Every vertex reachable from the double edge has degree at most two.

theorem TauCeti.IsFiniteType.degree_le_two_of_apply_mul_apply_eq_two {B : Type u_1} [DecidableEq B] {A : Matrix B B ℤ} [Fintype B] (h : IsFiniteType A) (hconn : (diagramGraph A).Preconnected) {u v : B} (huv : A u v * A v u = 2) (c : B) : (diagramGraph A).degree c ≤ 2

A connected finite-type diagram containing a double edge has maximum degree two.

Thus the component has no branch vertex. This is the extraction step that makes the branchless double-edge classification apply without an extra shape hypothesis.

theorem TauCeti.IsFiniteType.exists_equiv_forall_eq_doubleEdgeCartanMatrix_of_apply_mul_apply_eq_two {B : Type u_1} {A : Matrix B B ℤ} (h : IsFiniteType A) (hconn : (diagramGraph A).Preconnected) {u v : B} (huv : A u v * A v u = 2) : ∃ (p : ℕ) (q : ℕ), 0 < p ∧ 0 < q ∧ (q = 1 ∨ p = 1 ∨ p = 2 ∧ q = 2) ∧ ∃ (e : B ≃ Fin p ⊕ Fin q), ∀ (i j : B), A i j = doubleEdgeCartanMatrix p q (e i) (e j)

Classification of the double-edge case. A connected finite-type diagram containing a double edge reindexes to two nonempty chains of one of the admissible shapes: type C (the second chain is a singleton), type B (the first is a singleton), or type F₄ (both have two vertices).