Simply-laced Cartan matrices are positive definite #
TauCeti.IsFiniteType carries a positive definite symmetrization, but behind an existential over
the symmetrizer, so it says nothing directly about the matrix itself. For a simply-laced Cartan
matrix the constant-one vector is a symmetrizer, and its symmetrization is the matrix itself read
over ℚ, so positive definiteness holds on the nose. The per-family statements are proved beside
the coordinate models they use, in TauCeti.LinearAlgebra.RootSystem.FiniteType.Classical and
TauCeti.LinearAlgebra.RootSystem.FiniteType.Dynkin; this file collects them into the statement a
consumer indexing over TauCeti.DynkinType wants, so that nobody repeats the case split.
The hypothesis is placed on the matrix rather than on the type. By
TauCeti.DynkinType.isSimplyLaced_cartanMatrix_iff that is the weaker of the two: besides the
simply-laced types A, D, E₆, E₇ and E₈ it admits B 0, B 1, C 0 and C 1, whose
matrices are the empty matrix and A 1. The statement for a simply-laced type is the corollary
TauCeti.DynkinType.IsSimplyLaced.posDef_map_intCast_cartanMatrix.
Main results #
TauCeti.DynkinType.posDef_map_intCast_cartanMatrix_of_isSimplyLaced: a simply-laced standard Cartan matrix is positive definite overℚ.TauCeti.DynkinType.IsSimplyLaced.posDef_map_intCast_cartanMatrix: the Cartan matrix of a simply-laced Dynkin type is positive definite overℚ.
A simply-laced standard Cartan matrix is positive definite over ℚ. The types whose
matrix is simply laced are A, D, E₆, E₇, E₈ and the degenerate B 0, B 1, C 0,
C 1 (TauCeti.DynkinType.isSimplyLaced_cartanMatrix_iff); the last four have the empty matrix or
A 1 as their Cartan matrix.
The Cartan matrix of a simply-laced Dynkin type is positive definite over ℚ. The
simply-laced types are exactly A, D, E₆, E₇ and E₈.