Cartan matrices and their myriad generalizations

This is part of the effort to add reflection representations of Coxeter groups to mathlib. See also #13291, which expounds some of the issues regarding ordered rings other than the real numbers, as well as the distinction between "the" reflection representation and "a" reflection representation.

For the sake of exposition, let us work over the real numbers for now. Using Chebyshev polynomials, it is possible to make all of this work over any ordered ring; more details can be found in #13291.

Let $$M$$ be a Coxeter matrix and let $$W$$ be the corresponding Coxeter group. (See Mathlib/GroupTheory/Coxeter/Matrix.lean
and Mathlib/GroupTheory/Coxeter/Basic.lean for the definitions of these terms.) Let $$k$$ be a matrix of real numbers with the same dimensions as $$M$$. Consider the following conditions that the matrix $$k$$ could satisfy.

1. For all $$i$$, we have $$k_{i, i} = 2$$.
2. For all $$i, i'$$ with $$1 < M_{i, i'} < \infty$$, the number $$k_{i,i'}k_{i', i}$$ is of the form $$4 \cos^2(\pi \ell / M_{i, i'})$$, where $$\ell$$ is an integer with $$0 < \ell \leq M_{i, i'} / 2$$.
3. For all $$i, i'$$, we have $$k_{i, i'} = 0$$ if and only if $$k_{i', i} = 0$$.
4. (strengthening of 2) For all $$i, i'$$ with $$M_{i, i'} < \infty$$, we have $$k_{i,i'}k_{i', i} = 4 \cos^2(\pi / M_{i, i'})$$.
5. For all $$i, i'$$ with $$M_{i, i'} = \infty$$, we have $$k_{i,i'}k_{i', i} \geq 4$$.
6. For all $$i \neq i'$$, we have $$k_{i, i'} \leq 0$$.
7. The entries of $$k$$ are all integers.
8. The matrix $$k$$ is symmetrizable; that is, it can be written as $$DS$$, where $$D$$ is diagonal with positive entries and $$S$$ is symmetric.
9. (strengthening of 8) The matrix $$k$$ can be written as $$DS$$, where $$D$$ is diagonal with positive entries and $$S$$ is symmetric and positive definite.

It is not difficult to see that $$k$$ is a Cartan matrix if and only if it satisfies all nine of these properties. (What I mean by this is that a matrix $$k$$ is a Cartan matrix if and only if there exists a Coxeter matrix $$M$$ for which all nine properties hold, and if so, the Coxeter matrix $$M$$ is unique.) Any Cartan matrix can be used to construct a reflection representation of the Coxeter group $$W$$. It can be described as follows.

• The representation is on a real vector space $$V$$, called the root space.
• There are elements $$\alpha_i \in V$$, called the simple roots. The simple roots form a basis of $$V$$.
• There are elements $$\alpha^\vee_i \in V^*$$, called the simple coroots. They are given by $$k_{i, i'} = \alpha^\vee_i(\alpha_{i'})$$ for all $$i, i'$$.
• The simple reflection $$s_i$$ acts by a reflection: $$s_i v = v - \alpha^\vee_i (v)\alpha_i$$.

This is all well-known and standardized. However, here is something that, as far as I can tell, is not. We do not actually need the matrix $$k$$ to satisfy all 10 of the above properties in order to get a reflection representation of $$W$$ as above. Namely:

• Only properties 1, 2, and 3 are necessary for the matrix $$k$$ to actually yield a reflection representation of $$W$$.
• If $$k$$ satisfies properties 1, 2, 3, 4, 5, 6, then this reflection representation is a geometric representation. That is, every element $$w \alpha_i \in V$$ is either a nonpositive linear combination of the simple roots or a nonnegative linear combination of the simple roots, according to whether $$s_i$$ is a right descent of $$w$$ or not. (This implies that the representation is faithful.)
• If $$k$$ satisfies properties 1, 2, 3, and 7, then this reflection representation is crystallographic. That is, it fixes the root lattice $$\bigoplus_i\mathbb{Z} \alpha_i$$.
• If $$k$$ satisfies properties 1, 2, 3, and 8, then this reflection representation comes with its own invariant bilinear form. This bilinear form, considered as a linear map $$V \to V^*$$, sends each simple root $$\alpha_i$$ to a positive multiple of the corresponding simple coroot $$\alpha^\vee_i$$.
• If $$k$$ satisfies properties 1, 2, 3, 8, and 9, then the aforementioned bilinear form is an inner product on $$V$$. (If $$k$$ satisfies properties 1, 2, 3, 4, 5, 6, 8, and 9, then this implies that the group $$W$$ is finite.)

Matrices satisfying properties 1, 2, 3, 4, 5, and 6 are of particular interest. They appear in a few different references on Coxeter groups. (See Combinatorics of Coxeter Groups by Björner and Brenti or page 9 here.) Note that the matrix $$k_{i, i'} = -2 \cos(\pi / M_{i, i'})$$ satisfies properties 1, 2, 3, 4, 5, 6, 8, and 9; this yields the so-called standard geometric representation of $$W$$ over the real numbers. The standard geometric representation has the additional property that its positive roots (i.e. the elements of the form $w \alpha_i$ that can be written as a nonnegative linear combination of simple roots) correspond to the reflections of $W$.

See here for current progress. It is not quite ready for review.

https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Progress.20on.20Coxeter.20groups/near/488774778

Start with Mathlib/GroupTheory/Coxeter/Matrix.lean and Mathlib/GroupTheory/Coxeter/Basic.lean, then inspect the linked generalized-cartan comparison and Zulip progress. Done means the agreed Cartan-matrix generalizations and associated reflection-representation work are formalized consistently with the stated conditions.