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

TauCeti.IsFiniteType asks of an integer matrix that it be a generalized Cartan matrix carrying a positive rational symmetriser whose symmetrisation is positive definite. This file certifies the four infinite families of the standard list, Mathlib's CartanMatrix.A, CartanMatrix.B, CartanMatrix.C and CartanMatrix.D, uniformly in the rank and with no appeal to an already constructed root system: only the matrices themselves are involved.

The proof is the Gram-matrix one. The symmetrisation d i * A i j of a Cartan matrix is the matrix of inner products of the simple coroots α_i^∨ = 2 α_i / (α_i, α_i), so it is positive definite as soon as those vectors are linearly independent. Types A, B, and D therefore get explicit rational matrices whose rows are their simple coroots in the standard orthogonal coordinates, and two facts are proved about each: that its Gram matrix is the symmetrisation, and that its rows are independent. Positive definiteness is then Mathlib's Matrix.PosDef.mul_conjTranspose_self. Type C follows from type B because finite type is invariant under transpose.

The coordinates are the classical ones, and the rows are listed in the Bourbaki order carried by Mathlib's matrices, so that the last node is the one the Bₙ/Cₙ double edge ends at.

type	simple coroots	ambient space
Aₙ	eᵢ - eᵢ₊₁	ℚ^{n+1}
Bₙ	eᵢ - eᵢ₊₁, and 2 e_{n-1}	ℚ^n
Dₙ	eᵢ - eᵢ₊₁, and e_{n-2} + e_{n-1}	ℚ^n

Type A is the one family whose ambient space is larger than its rank. A square rational M with M Mᵀ = CartanMatrix.A n would make the determinant of that matrix, which is n + 1, a rational square, so no n-dimensional rational coordinate model exists whenever n + 1 is not a square. The sum-zero hyperplane of ℚ^{n+1} instead gives one uniform model for every n.

Independence of the rows is where the families part company, and it is why type D is handled last. For A and B the matrix is triangular against an increasing choice of coordinates - TauCeti.vecMul_injective_of_submatrix_isUpperTriangular - with a nonzero diagonal. No such choice exists for D, whose two fork coordinates e_{n-2}, e_{n-1} support three rows between them, so that family is treated in two steps: the sum of all coordinates annihilates every row but the fork one, which pins the last coefficient to zero, and the rows that remain are the triangular chain again.

Main results

• TauCeti.isFiniteType_cartanMatrix_A, TauCeti.isFiniteType_cartanMatrix_B, TauCeti.isFiniteType_cartanMatrix_C, TauCeti.isFiniteType_cartanMatrix_D: the standard Cartan matrix of each classical family is of finite type, at every rank. No rank restriction is imposed: the low-rank coincidences B 1 = C 1 = A 1, C 2 = B 2 and D 3 = A 3 are finite-type matrices too, and it is TauCeti.DynkinType.Valid, not this file, that discards them.
• TauCeti.posDef_map_intCast_cartanMatrix_A, TauCeti.posDef_map_intCast_cartanMatrix_D: those two families being simply laced, the constant-one vector is a symmetriser for them, and its symmetrisation is the Cartan matrix itself read over ℚ; so the Gram models give positive definiteness of the Cartan matrix with no symmetriser in the way, and the finite-type statements for A and D are read off these. Types B and C have no such statement at rank 2 and above, where their Cartan matrices are not symmetric; the degenerate ranks 0 and 1, at which they coincide with A 0 and A 1, are handled in TauCeti.LinearAlgebra.RootSystem.FiniteType.SimplyLaced.

Since TauCeti.DynkinType.cartanMatrix is Mathlib's matrix on each of these four constructors, a consumer that needs the standard Cartan matrix of a classical Dynkin type to be nonsingular reaches it through TauCeti.DynkinType.cartanMatrix_A and its siblings together with TauCeti.IsFiniteType.det_ne_zero.

Implementation notes

Every simple system above has each row supported on at most two coordinates, so a private common construction and Gram-matrix calculation are shared by the three coordinate proofs. A row supported on a single coordinate is written with a zero second coefficient rather than with a separate constructor, using the clamped successor Order.succ for its second coordinate. A private helper selects the first coordinate of the type D fork row.

References

This file supplies the classical half of the "finite-type condition" item of Layer 5 of TauCetiRoadmap/RepresentationTheory/RootSystems/README.md. The coordinate models are the standard ones of Bourbaki, Lie Groups and Lie Algebras, Chapters 4-6, plates I-IV, and of J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, section 12.1.

Simple systems supported on two coordinates

Independence of the rows

Type Aₙ

theorem TauCeti.posDef_map_intCast_cartanMatrix_A (n : ℕ) : ((CartanMatrix.A n).map Int.cast).PosDef

The Cartan matrix of type Aₙ is positive definite over ℚ, at every rank: it is the Gram matrix of the simple coroots, which are independent.

theorem TauCeti.isFiniteType_cartanMatrix_A (n : ℕ) : IsFiniteType (CartanMatrix.A n)

The Cartan matrix of type Aₙ is of finite type, at every rank. The family is simply laced, so the constant-one vector is a symmetriser and TauCeti.posDef_map_intCast_cartanMatrix_A is the positive definiteness of its symmetrisation.

Type Bₙ

theorem TauCeti.isFiniteType_cartanMatrix_B (n : ℕ) : IsFiniteType (CartanMatrix.B n)

The Cartan matrix of type Bₙ is of finite type, at every rank.

theorem TauCeti.isFiniteType_cartanMatrix_C (n : ℕ) : IsFiniteType (CartanMatrix.C n)

The Cartan matrix of type Cₙ is of finite type, at every rank.

Type Dₙ

theorem TauCeti.posDef_map_intCast_cartanMatrix_D (n : ℕ) : ((CartanMatrix.D n).map Int.cast).PosDef

The Cartan matrix of type Dₙ is positive definite over ℚ, at every rank: it is the Gram matrix of the simple coroots, which are independent. The coordinate model needs two coordinates for its fork, so the ranks 0 and 1 are handled apart: at rank 0 the matrix is empty and positive definiteness is vacuous, and at rank 1 Mathlib's CartanMatrix.D_one identifies the matrix with A 1.

theorem TauCeti.isFiniteType_cartanMatrix_D (n : ℕ) : IsFiniteType (CartanMatrix.D n)

The Cartan matrix of type Dₙ is of finite type, at every rank. The family is simply laced, so the constant-one vector is a symmetriser and TauCeti.posDef_map_intCast_cartanMatrix_D is the positive definiteness of its symmetrisation.