The triple-edge case of the finite-type classification

A triple edge in a finite-type Cartan matrix is isolated: neither endpoint can have another neighbour. This file combines that local obstruction with preconnectedness. If the whole diagram is preconnected, the two endpoints are therefore all its vertices. The rank-two classification then identifies the matrix, up to one simultaneous relabelling of rows and columns, with the standard Bourbaki Cartan matrix of type G₂.

The point of the result is the passage from the local estimate to a complete classification branch. TauCeti.IsFiniteType.apply_eq_zero_of_apply_mul_apply_eq_three alone allows other connected components, while the theorem here says that an indecomposable finite-type matrix containing a triple edge is precisely G₂.

Main results

• TauCeti.IsFiniteType.eq_or_eq_of_apply_mul_apply_eq_three: every vertex of a preconnected finite-type diagram containing a triple edge is one of its endpoints.
• TauCeti.IsFiniteType.card_eq_two_of_apply_mul_apply_eq_three: such a diagram has two vertices.
• TauCeti.IsFiniteType.exists_equiv_cartanMatrix_eq_G2_of_apply_mul_apply_eq_three: the matrix reindexes to the standard Cartan matrix of type G₂.
• TauCeti.IsFiniteType.exists_apply_mul_apply_eq_three_iff_exists_equiv_cartanMatrix_eq_G2: a preconnected finite-type matrix has a triple edge exactly when it has Cartan type G₂.

References

This is the triple-edge branch of the classification of finite-type Cartan matrices in Layer 5 of TauCetiRoadmap/RepresentationTheory/RootSystems/README.md. See N. Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Chapter VI, §4, and J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, §11.4. The convention is Bourbaki's G₂ matrix !![2, -1; -3, 2], with the short simple root first.

theorem TauCeti.IsFiniteType.eq_or_eq_of_apply_mul_apply_eq_three {B : Type u_1} {A : Matrix B B ℤ} (h : IsFiniteType A) (hconn : (diagramGraph A).Preconnected) {i j : B} (hij : A i j * A j i = 3) (k : B) : k = i ∨ k = j

A preconnected finite-type diagram containing a triple edge consists only of its endpoints.

Both endpoints have no other neighbour by TauCeti.IsFiniteType.apply_eq_zero_of_apply_mul_apply_eq_three. The induced subgraph on the two endpoints is therefore closed under taking neighbours. Preconnectedness forces every vertex into that induced subgraph.

theorem TauCeti.IsFiniteType.card_eq_two_of_apply_mul_apply_eq_three {B : Type u_1} {A : Matrix B B ℤ} [Fintype B] (h : IsFiniteType A) (hconn : (diagramGraph A).Preconnected) {i j : B} (hij : A i j * A j i = 3) : Fintype.card B = 2

A preconnected finite-type diagram containing a triple edge has exactly two vertices.

theorem TauCeti.IsFiniteType.exists_equiv_cartanMatrix_eq_G2_of_apply_mul_apply_eq_three {B : Type u_1} {A : Matrix B B ℤ} (h : IsFiniteType A) (hconn : (diagramGraph A).Preconnected) {i j : B} (hij : A i j * A j i = 3) : ∃ (e : B ≃ Fin DynkinType.G2.rank), ∀ (x y : B), A x y = DynkinType.G2.cartanMatrix (e x) (e y)

The triple-edge branch of the finite-type classification is G₂.

For a preconnected finite-type matrix, a Cartan product of three first forces the index type to have two elements. Rank-two classification supplies its unique valid Dynkin type. The Cartan product is invariant under relabelling and distinguishes G₂ from A₂ and B₂.

theorem TauCeti.IsFiniteType.exists_apply_mul_apply_eq_three_iff_exists_equiv_cartanMatrix_eq_G2 {B : Type u_1} {A : Matrix B B ℤ} (h : IsFiniteType A) (hconn : (diagramGraph A).Preconnected) : (∃ (i : B) (j : B), A i j * A j i = 3) ↔ ∃ (e : B ≃ Fin DynkinType.G2.rank), ∀ (x y : B), A x y = DynkinType.G2.cartanMatrix (e x) (e y)

A preconnected finite-type matrix contains a triple edge exactly when it has type G₂.

The right side uses the same simultaneous row-and-column relabelling as HasCartanType. No orientation is imposed on the witness edge on the left: reversing its endpoints does not change the Cartan product.