Exceptional Cartan matrices are of finite type, and the simply-laced ones positive definite

This file proves that the five exceptional Cartan matrices in TauCeti.DynkinType are of finite type, and that the three simply-laced ones are positive definite over ℚ -- for those the constant-one vector is a symmetriser, whose symmetrisation is the Cartan matrix itself read over ℚ, so the Gram model below proves positive definiteness of the Cartan matrix directly. The proof exhibits each symmetrized Cartan matrix as Bᴴ * B for an explicit rational matrix B and reads off positive definiteness from TauCeti.isFiniteType_of_conjTranspose_mul_self_of_det_ne_zero, or, for E₈, from TauCeti.Matrix.posDef_conjTranspose_mul_self_of_isUnit followed by TauCeti.isFiniteType_of_posDef_map_intCast.

The columns of B are the simple coroots αᵢ^∨ = 2 αᵢ / (αᵢ, αᵢ), in orthonormal rational coordinates and up to one common positive scale, rather than the simple roots themselves. That is forced by the symmetrizer: the symmetrization dᵢ Aᵢⱼ is symmetric exactly when dᵢ is proportional to 1 / (αᵢ, αᵢ), and then dᵢ Aᵢⱼ is proportional to (αᵢ^∨, αⱼ^∨). The two readings agree for the simply-laced E₈, where all roots have the same length, and differ for F₄ and G₂, where a column of B is longest exactly where the corresponding root is shortest. Node numbering is Bourbaki's throughout: column i belongs to node i of TauCeti.DynkinType.

Only E₈ needs a coordinate model among the simply-laced types: the E₆ and E₇ Cartan matrices are the principal submatrices of the E₈ one on the first six and seven indices, so TauCeti.IsFiniteType.submatrix delivers them. That one model is not tabulated here but taken from TauCeti.LinearAlgebra.RootSystem.E8Coordinates, whose integral table has twice the simple roots as its rows; halving and transposing it gives the B above. The nonsimply-laced types use the integral symmetrizers (1, 1, 2, 2) for F₄ and (3, 1) for G₂, the inverse root lengths recorded in TauCeti.DynkinType.rootLength_F4 and TauCeti.DynkinType.rootLength_G2.

Main results

• TauCeti.DynkinType.isFiniteType_cartanMatrix_E8
• TauCeti.DynkinType.isFiniteType_cartanMatrix_E6
• TauCeti.DynkinType.isFiniteType_cartanMatrix_E7
• TauCeti.DynkinType.isFiniteType_cartanMatrix_F4
• TauCeti.DynkinType.isFiniteType_cartanMatrix_G2
• TauCeti.posDef_map_intCast_cartanMatrix_E6, TauCeti.posDef_map_intCast_cartanMatrix_E7 and TauCeti.posDef_map_intCast_cartanMatrix_E8: the exceptional simply-laced Cartan matrices CartanMatrix.E 6, CartanMatrix.E 7 and CartanMatrix.E 8 are positive definite over ℚ, E₆ and E₇ as principal submatrices of E₈. Like TauCeti.posDef_map_intCast_cartanMatrix_A these are stated for Mathlib's matrices and live in the TauCeti namespace, not in TauCeti.DynkinType.
• TauCeti.DynkinType.cartanMatrix_E6_eq_submatrix_E8 and TauCeti.DynkinType.cartanMatrix_E7_eq_submatrix_E8: the nesting E₆ ⊂ E₇ ⊂ E₈ at the level of Cartan matrices, which is what makes the two derivations above possible.

References

This file advances the "classification of finite-type Cartan matrices" target in Layer 5 of TauCetiRoadmap/RepresentationTheory/RootSystems/README.md. The E₈ model is the list of simple roots of Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, plate VII; the F₄ and G₂ models are the coroots dual to the simple roots of plates VIII and IX. See also Humphreys, Introduction to Lie Algebras and Representation Theory, Chapter 11.

theorem TauCeti.posDef_map_intCast_cartanMatrix_E8 : ((CartanMatrix.E 8).map Int.cast).PosDef

The E₈ Cartan matrix is positive definite over ℚ: it is the Gram matrix of the coordinate model, and it is nonsingular.

theorem TauCeti.DynkinType.isFiniteType_cartanMatrix_E8 : IsFiniteType E8.cartanMatrix

The standard Cartan matrix of type E₈ is of finite type: the family is simply laced, so the constant-one vector is a symmetriser and TauCeti.posDef_map_intCast_cartanMatrix_E8 is the positive definiteness of its symmetrisation.

theorem TauCeti.DynkinType.cartanMatrix_E6_eq_submatrix_E8 : CartanMatrix.E 6 = (CartanMatrix.E 8).submatrix (Fin.castAdd 2) (Fin.castAdd 2)

The E₆ Cartan matrix is the principal submatrix of the E₈ one on the first six nodes: in Bourbaki's numbering the exceptional E diagrams are nested, E₆ ⊂ E₇ ⊂ E₈.

theorem TauCeti.DynkinType.cartanMatrix_E7_eq_submatrix_E8 : CartanMatrix.E 7 = (CartanMatrix.E 8).submatrix (Fin.castAdd 1) (Fin.castAdd 1)

The E₇ Cartan matrix is the principal submatrix of the E₈ one on the first seven nodes: in Bourbaki's numbering the exceptional E diagrams are nested, E₆ ⊂ E₇ ⊂ E₈.

theorem TauCeti.DynkinType.isFiniteType_cartanMatrix_E6 : IsFiniteType E6.cartanMatrix

The standard Cartan matrix of type E₆ is of finite type: it is the principal submatrix of the E₈ Cartan matrix on the first six indices.

theorem TauCeti.DynkinType.isFiniteType_cartanMatrix_E7 : IsFiniteType E7.cartanMatrix

The standard Cartan matrix of type E₇ is of finite type: it is the principal submatrix of the E₈ Cartan matrix on the first seven indices.

theorem TauCeti.posDef_map_intCast_cartanMatrix_E6 : ((CartanMatrix.E 6).map Int.cast).PosDef

The E₆ Cartan matrix is positive definite over ℚ: it is a principal submatrix of the E₈ one.

theorem TauCeti.posDef_map_intCast_cartanMatrix_E7 : ((CartanMatrix.E 7).map Int.cast).PosDef

The E₇ Cartan matrix is positive definite over ℚ: it is a principal submatrix of the E₈ one.

theorem TauCeti.DynkinType.isFiniteType_cartanMatrix_F4 : IsFiniteType F4.cartanMatrix

The standard Cartan matrix of type F₄ is of finite type.

theorem TauCeti.DynkinType.isFiniteType_cartanMatrix_G2 : IsFiniteType G2.cartanMatrix

The standard Bourbaki-numbered Cartan matrix of type G₂ is of finite type.