A finite-type Cartan inequality has finitely many natural solutions

Let A be an integer matrix of finite type, that is a generalized Cartan matrix carrying a positive symmetrizer whose symmetrization is positive definite (Ado.IsFiniteType). This file proves that for every integer vector y the system of inequalities

∑ j, A i j * c j ≤ y i (for every index i)

has only finitely many solutions c in the nonnegative integers.

The system is the shape in which dominance bounds a weight from below. A weight mu lying under lam is lam - ∑ j, c j • αⱼ for natural numbers c j, and its value on the simple coroot αᵢ^∨ is lam (αᵢ^∨) - ∑ j, c j * ⟨αⱼ, αᵢ^∨⟩; asking that value to be a natural number is exactly the displayed inequality for the transposed Cartan matrix. Finiteness of the solution set is therefore finiteness of the set of dominant weights under lam, which is how TauCeti/LinearAlgebra/RootSystem/DominantCone.lean uses it.

Main results

• Ado.finite_setOf_forall_sum_mul_le: an inequality whose matrix has a positive symmetrizer has finitely many natural solutions.

The argument

Everything happens in the rational bilinear form F u v = u ⬝ᵥ S *ᵥ v of the symmetrization S i j = d i * A i j, which is symmetric and positive definite. Positive definiteness makes S invertible, so every linear functional on B → ℚ is F (·) w for some w; the two functionals this file represents that way are c ↦ ∑ i, d i * y i * c i and, for each index k, the k-th coordinate.

• Because the entries of c are nonnegative and the symmetrizer is positive, the inequalities sum to F x x ≤ F x z, where x is c viewed rationally and z represents the first functional. Cauchy-Schwarz for a positive semidefinite symmetric form (LinearMap.BilinForm.apply_sq_le_of_symm) turns that into F x x ≤ F z z: a bound on the length of x that does not depend on c.
• Cauchy-Schwarz applied a second time, against the vector representing the k-th coordinate, bounds each c k in terms of F x x. So the solutions lie in a product of finite intervals.

No compactness, completeness or eigenvalue theory enters; the two applications of Cauchy-Schwarz replace them, which is what keeps the argument inside ℚ.

References

This supplies the root-system half of the "weight-cone bound" milestone of Layer 4, "the classification of finite-dimensional irreducibles", of TauCetiRoadmap/RepresentationTheory/LieHighestWeight/README.md.

• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, GTM 9, §13.2, Lemma B.

theorem Ado.finite_setOf_forall_sum_mul_le {B : Type u_1} [Fintype B] {A : Matrix B B ℤ} (d : B → ℚ) (hd : ∀ (i : B), 0 < d i) (hpd : (Matrix.of fun (i j : B) => d i * ↑(A i j)).PosDef) (y : B → ℤ) : {c : B → ℕ | ∀ (i : B), ∑ j : B, A i j * ↑(c j) ≤ y i}.Finite

A positively symmetrized matrix inequality has finitely many natural solutions. Let d be a positive rational vector such that the matrix with entries d i * A i j is positive definite. For any integer vector y, only finitely many vectors c of natural numbers satisfy ∑ j, A i j * c j ≤ y i at every index i.

Positive definiteness of the symmetrization of A is what makes the solution set bounded: the inequalities force the length of c in the symmetrized form to stay below a bound read off from y alone.