Eigenvalues of Cartan matrices

Stream: maths

[Oliver Nash]

Does anyone know an elementary proof of that fact that 4 is never an eigenvalue of a Cartan matrix?

[Oliver Nash]

The background is that I've recently been working to formalise various parts of a nice paper of Geck "On the construction of semisimple Lie algebras and Chevalley groups".

(e.g., Lemma 2.6 is docs#RootPairing.chainBotCoeff_mul_chainTopCoeff)

One of the results I want to include is Lemma 4.2 and this needs the fact that 4 is never an eigenvalue of a Cartan matrix.

[Oliver Nash]

Geck's proof of this is just to invoke the classification of Cartan matrices. I could do this too but it would mean I'd have to delay proving Lemma 4.2 until we had the classification (as well as introducing a dependency).

I believe stronger results are true, e.g., if $p$ is the characteristic polynomial of a Cartan matrix then I've just convinced myself that $p(4 - λ) = p(λ)$ (I don't have a reference, but I expect this is in Bourbaki, at least implicitly). I don't know if this is useful to me though: as I just need the weaker result mentioned.

[Oliver Nash]

My guess is that there is a proof of what I need that does not need the classification but I haven't yet found / thought of one.

[Damiano Testa]

I wonder if you could use the Perron-Frobenius theorem to bound the spectral radius of Cartan matrices and deduce what you want. I have not tried to see what you get as an answer, though.

[Oliver Nash]

Interesting idea! I believe the spectral radius of a Cartan matrix is strictly less than 4, though I can't immediately see if I can use PF here. I'm out of time for now but I'll think some more this evening.

[Kevin Buzzard]

What do we know about Cartan matrices? Square matrix, integer entries, diagonal entries are all 2, non-diagonal entries are 0 or -1 or -2 or -3, det is positive, are all of those right? Anything else?

[Oliver Nash]

Yes we know all of the above (modulo the detail that Mathlib only knows the det is non-zero but it would be very easy to sharpen to the fact that it is positive). The only other things Mathlib currently knows about a Cartan matrix $A$ are:

• Off-diagonal entries satisfy a further constraint: if $i \ne j$ then $(A_{ij}, A_{ji}) \in \{(0, 0), (-1, -1), (-1, -2), (-2, -1), (-1, -3), (-3, -1)\}$. (In other words the $A_{ij} = 0 \iff A_{ji} = 0$ and $A_{ij}A_{ji} < 4$.)
• If the matrix has rank > 2 then the value -3 cannot occur.
• There exists a diagonal matrix $D$ (with strictly positive entries) of the same size as $A$ and a symmetric positive-definite matrix $S$ such that $A = DS$.

[Oliver Nash]

FWIW I think that $\begin{bmatrix}2 & -1 & -1 & 0\\-1 & 2 & -1 & -1\\-1 & -1 & 2 & -1\\0 & -2 & -2 & 2\end{bmatrix}$ satisfies all the conditions except the last one and has eigenvalues $-1, 2, 3, 4$. EDIT: oh wait, it has negative determinant :man_facepalming:

[Oliver Nash]

I'll stop spamming this channel now and do some thinking instead.

[Kevin Buzzard]

If X is your counterexample then X oplus X will have positive determinant :-( (PS typo (-2,1) -> (-2,-1) in your list above)

[Antoine Chambert-Loir]

Proposition 1 expresses the characteristic polynomial of Cartan matrices of simple Lie algebras as Chebyshev polynomials. But the proof is a case by case analysis using the Cartan-Killing classification.

[Antoine Chambert-Loir]

Then, the symmetry $A \leftrightarrow 4-A$ that appears in Geck's paper comes from the fact that $2-A$ is the adjacency matrix of the Coxeter diagram.

[Antoine Chambert-Loir]

(I don't know whether that helps.)

[Oliver Nash]

Thank you all for these remarks, all of which are very helpful.

I believe that Damiano's suggestion to use Perron-Frobenius works, though it needs to be the version for non-negative irreducible matrices. Here's a sketch:

If $A$ is a Cartan matrix, let $M = 2I - A$ and note that $M$ non-negative and irreducible. By PF, the spectral radius $\rho$ of $M$ is an eigenvalue. Let $v$ be a corresponding eigenvector. Let $S$ and $D$ be positive-definite matrices such that $S = DA$ where $S$ is symmetric and $D$ is diagonal. Now calculate $0 < v^tSv = v^tDAv = v^tD(2I - M)v = (2-\rho)v^tDv$. Since $0 < v^tDv$ this gives $\rho < 2$. Thus any eigenvalue $\mu$ of $M$ satisfies $|\mu| < 2$ and thus if $\lambda = 2 - \mu$ is an eigenvector of $A$ we must have $|\lambda| < 4$.

[Oliver Nash]

I need to spend my time on other things for the next couple of days so it might not be till next week that I can think more about this. One question that immediately occurs to me is whether it might be able to prove this without PF since (again, by PF) the $\rho$-eigenspace is 1-dimensional and thus $v$ should should up as some "geometric" object in the root space.

[Oliver Nash]

Come to think of it, I think it's easy to see that $A$ must have real eigenvalues and so the argument I sketched goes through without PF. OK I really need to focus my other work now.

[Damiano Testa]

I am so glad that PF works! It is one of my favourite results, not just in linear algebra, but in maths!

[Damiano Testa]

(I also understand if you prefer to find an alternative argument that bypasses: I am still happy that it could be used!)

[Damiano Testa]

Another thing that PF gives you, is that the eigenvector has positive entries. It has been a while since I thought about Lie theory, but I am thinking of Casimir-something now...

[Patrick Massot]

What is the issue with using Perron-Frobenius? It’s a lot less work than the classification you are trying to avoid, right?

[Oliver Nash]

There's no issue, and I agree that PF would be much less work than classifying Cartan matrices (and calculating from there). It's just that I can't help suspecting that there might be an argument that is more intrinsic to the root system (and hopefully short and slick). For example, I learned yesterday that the spectral radius of a Cartan matrix is $2 + 2\cos(\pi/h)$ where $h$ is the Coxeter number (i.e., the order of an element of the Weyl group which can be written as a product of all the reflections in a base). So this is an example of a more "intrinsic" fact. Of course proving this is probably more work than classifying Cartan matrices, and certainly much more work than proving PF, but then it's more than we need. Perhaps there is a slick argument that gives $\rho < 4$. The most promising approach seems to be proving the symmetry of eigenvalues under $\lambda \mapsto 4 - \lambda$ and I also learned yesterday there is a nice proof of this in a 1989 paper of Berman, Lee, and Moody but even after that I still think PF is the easiest approach.

[Oliver Nash]

But I'm supposed to be writing a talk about AI in math so I really shouldn't have been delving into the literature yesterday and I've promised myself not to allow a repeat today. The Lie theory will have to wait till next week.

[Kalle Kytölä]

Patrick Massot said:

What is the issue with using Perron-Frobenius? It’s a lot less work than the classification you are trying to avoid, right?

I would fully agree with this point --- I see no issue using Perron-Frobenius.

But I just note that perhaps the Mathlib-appropriate proof of Perron-Frobenius theorem should be a special case of Krein-Rutman theorem, and this does not necessarily look like "a lot less work". (A student in my course is formalizing one complex analysis lemma that goes into the proof of Krein-Rutman, but my estimate is that Mathlib has too little on Larent-expansions of resolvents to finish Krein-Rutman with a reasonable amount of work.)

I am also, of course, hugely symphathetic to the idea of avoiding the use of the classification wherever possible. :heart:

[Mr Proof]

I thought the idea is the Cartan matrix entries give the angles between roots from the formula:

$$\theta = acos(-\sqrt{N}/2)$$

with N the entry (0,1,2,3) Since you want theta<180 degrees then N<4. Although you can have generalised Cartan matrices with any integers. Not sure if that helps or it just pushes the proof to why roots have an angle < 180.

[Oliver Nash]

@Mr Proof Perhaps I misunderstand but you seem to be outlining a reason why the entries of a Cartan matrix cannot exceed 4 (in magnitude) rather than saying something about the topic of this thread, which is about the eigenvalues.

[Oliver Nash]

(The result about entries is indeed easier and already in mathlib as docs#RootPairing.Base.cartanMatrix_mem_of_ne)

[Mr Proof]

@Oliver Nash You are correct. I apologise for my oversight. :pensive: