Reindexing a simply-laced branch diagram onto a star

Deleting the unique branch vertex of a simply-laced diagram which is a tree of maximum degree three leaves three path components. This file roots each path at the neighbour of the deleted vertex and joins the three rooted paths back to their centre. The resulting simultaneous row-and-column relabelling identifies the original matrix with TauCeti.starCartanMatrix.

Only the Cartan-matrix normalization, the symmetric vanishing pattern and the shape of the diagram are used, exactly as in the type Aₙ relabelling of TauCeti.LinearAlgebra.RootSystem.FiniteType.TypeA, so the relabelling also applies to diagrams not yet known to be of finite type. A connected simply-laced finite-type diagram with a branch vertex has that shape, and the model-star classification then applies to it, completing the D and E branch of the finite-type Cartan-matrix classification.

Main results

• TauCeti.exists_equiv_forall_eq_starCartanMatrix_of_isTree_of_isSimplyLaced: a simply-laced matrix with diagonal entries 2 whose diagram is a tree of maximum degree three with a unique vertex of degree three is a three-armed star.
• IsFiniteType.exists_equiv_forall_eq_starCartanMatrix_of_isSimplyLaced_of_degree_eq_three: a connected simply-laced finite-type matrix with a branch vertex is a three-armed star.
• TauCeti.IsFiniteType.existsUnique_dynkinType_of_isSimplyLaced_of_degree_eq_three: such a matrix carries a unique valid Dynkin type.
• TauCeti.existsUnique_dynkinType_of_isSimplyLaced_of_degree_eq_three: the corresponding classification statement for the base of an irreducible root system.

References

This is the reindexing step in the "classification of finite-type Cartan matrices" target of Layer 5 of TauCetiRoadmap/RepresentationTheory/RootSystems/README.md. 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_equiv_forall_eq_starCartanMatrix_of_isTree_of_isSimplyLaced {B : Type u_1} [Fintype B] {A : Matrix B B ℤ} [DecidableEq B] (htree : (diagramGraph A).IsTree) (hdiag : ∀ (i : B), A i i = 2) (hzero : ∀ (i j : B), A i j = 0 ↔ A j i = 0) (hsl : A.IsSimplyLaced) (hdeg : ∀ (i : B), (diagramGraph A).degree i ≤ 3) {c : B} (hc : (diagramGraph A).degree c = 3) (huniq : ∀ (i : B), (diagramGraph A).degree i = 3 → i = c) : ∃ (ℓ : Fin 3 → ℕ) (e : B ≃ StarIndex ℓ), (∀ (i : Fin 3), ℓ i ≠ 0) ∧ e c = none ∧ ∀ (i j : B), A i j = starCartanMatrix ℓ (e i) (e j)

A simply-laced matrix with diagonal entries 2 whose diagram is a tree of maximum degree three, with a unique vertex of degree three, is a three-armed star.

The arm lengths are the cardinalities of the three components left after deleting the branch vertex. They are nonzero, and the equivalence sends the branch vertex to the centre and roots each arm at its unique neighbour of the centre.

Only the Cartan-matrix normalization, the symmetric vanishing pattern and the shape of the diagram are needed here, rather than positive definiteness or the other finite-type hypotheses.

theorem TauCeti.IsFiniteType.exists_equiv_forall_eq_starCartanMatrix_of_isSimplyLaced_of_degree_eq_three {B : Type u_1} [Fintype B] {A : Matrix B B ℤ} (h : IsFiniteType A) (hconn : (diagramGraph A).Connected) (hsl : A.IsSimplyLaced) {c : B} (hc : (diagramGraph A).degree c = 3) : ∃ (ℓ : Fin 3 → ℕ) (e : B ≃ StarIndex ℓ), (∀ (i : Fin 3), ℓ i ≠ 0) ∧ e c = none ∧ ∀ (i j : B), A i j = starCartanMatrix ℓ (e i) (e j)

A connected simply-laced finite-type matrix with a branch vertex is a three-armed star.

The arm lengths are the cardinalities of the three components left after deleting the branch vertex. They are nonzero, and the equivalence sends the branch vertex to the centre and roots each arm at its unique neighbour of the centre.

theorem TauCeti.IsFiniteType.existsUnique_dynkinType_of_isSimplyLaced_of_degree_eq_three {B : Type u_1} [Fintype B] {A : Matrix B B ℤ} (h : IsFiniteType A) (hconn : (diagramGraph A).Connected) (hsl : A.IsSimplyLaced) {c : B} (hc : (diagramGraph A).degree c = 3) : ∃! t : DynkinType, t.Valid ∧ ∃ (e : B ≃ Fin t.rank), ∀ (i j : B), A i j = t.cartanMatrix (e i) (e j)

The simply-laced branch case of the finite-type Cartan-matrix classification. A connected simply-laced finite-type matrix with a vertex of degree three has exactly one valid Dynkin type. It is consequently one of Dₙ, E₆, E₇, or E₈, as determined by the three arm lengths in TauCeti.IsFiniteType.existsUnique_dynkinType_of_star.

theorem TauCeti.existsUnique_dynkinType_of_isSimplyLaced_of_degree_eq_three {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} [Finite ι] [CharZero R] [IsDomain R] [P.IsRootSystem] [P.IsCrystallographic] [P.IsReduced] [P.IsIrreducible] (b : P.Base) (hsl : b.cartanMatrix.IsSimplyLaced) {c : ↥b.support} (hc : (diagramGraph b.cartanMatrix).degree c = 3) : ∃! t : DynkinType, t.Valid ∧ HasCartanType P b t

An irreducible simply-laced root system with a branch vertex has a unique valid Dynkin type. The type is Dₙ, E₆, E₇, or E₈, with the three arms of the branch diagram determining which one.