Dynkin types #

The Cartan-Killing classification says that an irreducible reduced crystallographic finite root system is described by one of a short list of combinatorial types. This file introduces those types as a plain enumeration TauCeti.DynkinType, equips it with a rank, a validity predicate carving out the rank ranges in which the types are pairwise distinct and irreducible, and attaches to each type its standard integer Cartan matrix, taken from Mathlib's CartanMatrix family and numbered by Bourbaki's node labels, with node i at index i - 1. The predicate TauCeti.HasCartanType then says that the Cartan matrix of a base agrees with the standard matrix of a given type under a single simultaneous relabelling of rows and columns.

The enumeration is deliberately plain: the rank ranges A n (1 ≤ n), B n (2 ≤ n), C n (3 ≤ n), D n (4 ≤ n) are carried by TauCeti.DynkinType.Valid rather than baked into the constructors. Those bounds remove two different kinds of redundancy. The rank-zero types A 0, B 0, C 0, D 0 have empty Cartan matrices, and D 2 has the reducible matrix of A₁ × A₁, so none of these names an irreducible root system at all. The other excluded types are low-rank coincidences: B 1, C 1 and D 1 are A 1, C 2 is B 2, and D 3 is A 3, so each of them does name an irreducible root system, but one the list already carries under a valid name. What the bounds secure is therefore uniqueness of the type, not the existence of a root system realizing it. Note in particular that Valid is not preserved by exchanging B n and C n: B 2 is valid while C 2 is not, precisely because they name the same root system.

The matching in TauCeti.HasCartanType is oriented, using one relabelling e on both indices rather than allowing the matrix to be transposed. This is what keeps Bₙ and Cₙ apart from rank 3 on, where they are different root systems whose standard Cartan matrices are transposes of one another (CartanMatrix.B_transpose) and an unoriented match would identify them. At rank at most 2 the orientation carries no information about these matrices: relabelling by the swap of two indices transposes the off-diagonal entries but exchanges the diagonal ones as well, and every diagonal entry of a standard Cartan matrix is 2, so here transposition is itself a simultaneous relabelling. Hence B 2 and C 2 match exactly the same bases, in keeping with their naming the same root system; Valid keeps only B 2 of those two names.

Main definitions #

TauCeti.DynkinType: the enumeration A n, B n, C n, D n, E6, E7, E8, F4, G2.
TauCeti.DynkinType.rank: the number of simple roots of a type.
TauCeti.DynkinType.Valid: the rank ranges on which the types are the classification list.
TauCeti.DynkinType.IsSimplyLaced: the types A, D, E with only single edges.
TauCeti.DynkinType.cartanMatrix: the standard integer Cartan matrix of a type.
TauCeti.HasCartanType: a base whose Cartan matrix reindexes to a standard one.

Main results #

TauCeti.DynkinType.cartanMatrix_apply_same and TauCeti.DynkinType.cartanMatrix_apply_le_zero_of_ne: the standard matrices have diagonal 2 and nonpositive off-diagonal entries.
TauCeti.DynkinType.cartanMatrix_apply_eq_zero_iff_symm: their zero pattern is symmetric, so each is a generalized Cartan matrix.
TauCeti.DynkinType.cartanMatrix_C_two_apply_eq_cartanMatrix_B_two: the matrices of B 2 and C 2 are exchanged by the swap of the two Bourbaki nodes.
TauCeti.DynkinType.isSimplyLaced_cartanMatrix_iff: the standard Cartan matrix of a type is simply laced exactly when the type is or has rank at most one; rank at most one also holds of A 0, A 1, D 0 and D 1, but the types the second alternative adds to the first are precisely the degenerate B 0, B 1, C 0 and C 1, whose matrices have no off-diagonal entries to constrain.
TauCeti.DynkinType.isSimplyLaced_cartanMatrix_iff_of_valid: among valid types the simply-laced Cartan matrices are therefore exactly those of types A, D and E.
TauCeti.HasCartanType.isSimplyLaced_iff and TauCeti.HasCartanType.isSimplyLaced_iff_of_valid: both statements transferred to a base of Cartan type t.
TauCeti.HasCartanType.exists_supportEquiv_cartanMatrix_eq: two bases of the same Cartan type are related by a relabelling of their supports that matches their Cartan matrices.

References #

This file implements the DynkinType enumeration of Layer 5 of TauCetiRoadmap/RepresentationTheory/RootSystems/README.md, following the target signatures in TauCetiRoadmap/RepresentationTheory/RootSystems/Suggested.lean. See Bourbaki, Lie Groups and Lie Algebras, Chapters 4-6, plates I-IX, and Humphreys, Introduction to Lie Algebras and Representation Theory, Chapter 11, for the standard Cartan matrices.