Reflection representations of a Coxeter group

See #19934 for a more detailed exposition of the conditions needed to define reflection representations of a Coxeter group.

Let $W$ be a Coxeter group with simple generators $s_i$ and Coxeter matrix $(M_{i, i'})_{i, i'}$.

The traditional way to construct geometric representations

Traditionally, a geometric representation of $W$ is defined in the following way. (For example, see https://www.math.cuhk.edu.hk/course_builder/2223/math6032/lecture-notes-coxeter.pdf, page 9.) Fix any matrix $(k_{i, i})_{i, i'}$ satisfying the following conditions for all $i, i'$:

1. $k_{i, i} = 2$
2. $k_{i, i'} = 0$ if and only if $M_{i, i'} = 2$
3. $k_{i, i'} \leq 0$ for $i \neq i'$
4. $k_{i, i'} k_{i', i} = 4 \cos^2 (\pi / M_{i, i'})$ if $M_{i, i'} < \infty$
5. $k_{i, i'} k_{i', i} \geq 4$ if $M_{i, i'} = \infty$.

Let $V$ be the free $\mathbb{R}$-vector space on $\alpha_{i}$, and define the element $\alpha_i^\vee \in V^*$ by $\alpha_i^\vee (\alpha_{i'}) = k_{i, i'}$. Then, one may construct a representation $\rho \colon W \to GL(V)$ which satisfies
$$\rho(s_i) v = v - \alpha_i^\vee(v) \alpha_i$$ for all $i$ and all $v \in V$. This construction requires a rather involved linear algebra computation. It is not unlike the computation in #13270, but it involves a lot of sines and cosines and complex exponentials rather than Chebyshev polynomials.

There are several downsides to the traditional approach that make me think that it is not suitable for mathlib.

It only works over $\mathbb{R}$

Suppose that all of the entries of the Coxeter matrix $M$ are in the set $\{1, 2, 3, 4, 6, \infty\}$. Then, the numbers $4 \cos^2 (\pi / M_{i, i'})$ appearing in condition $4$ are all integers, and it is possible to do the entire construction over $\mathbb{Z}$ instead of $\mathbb{R}$. This yields a so-called crystallographic geometric representation of $W$. I believe that geometric representations of a Coxeter group should be constructed in a way that simply works over $\mathbb{Z}$ (and other ordered rings, such as real cyclotomic fields) to begin with.

The vector space is fixed

The traditional approach can be used to construct "the" geometric representation of $W$ (corresponding to a specific generalized Cartan matrix $(k_{i, i})_{i, i'}$). In "the" geometric representation of $W$, the underlying vector space is "the" free vector space $\bigoplus_i \mathbb{R} \alpha_i$.

This is not great. For example, let $W = S_n$ (the symmetric group, not the Chebyshev $S$-polynomial). This is a Coxeter group generated by the simple transpositions $s_i = (i, i+1)$ for $1 \leq i \leq n - 1$. Let $V$ be the subspace of $\mathbb{R}^n$ consisting of all vectors whose components sum to $0$. Then $V$ is a $W$-module in the usual way. It is common in the informal literature to call the representation $\rho \colon W \to GL(V)$ "the" (standard) geometric representation of $W$, but it isn't. The geometric representation of $W$ has underlying vector space $\bigoplus_i \mathbb{R} \alpha_i = \mathbb{R}^{n-1}$, not $V$. Of course, the two representations are isomorphic, but they are not equal.

In order to get around this issue, we ought to define not only "the" geometric representation of $W$, but also "a" geometric representation of $W$. (See https://arxiv.org/pdf/2405.10387.)

It's hard to formalize

The linear algebra computations involved in constructing geometric representations of $W$ are, simply put, quite involved. See the proof of Lemma 20 of https://www.math.cuhk.edu.hk/course_builder/2223/math6032/lecture-notes-coxeter.pdf, which involves computing complex eigenvalues of a 2 x 2 matrix, diagonalizing it, and several other things that would be a nightmare to formalize.

What should we do instead?

Let $\rho \colon W \to GL(V)$ be any representation, where $V$ is any module over a commutative ring. Let us say that $\rho$ is a reflection representation if it sends every simple reflection of $W$ to a reflection in $GL(V)$. That means that there exist elements $\alpha_i \in V$ and $\alpha_i^\vee \in V^*$ such that for all $i$, we have $\alpha_i^\vee (\alpha_i) = 2$, and for all $i$ and all $v \in V$, we have
$$\rho(s_i) v = v - \alpha_i^\vee(v) \alpha_i.$$

How does one construct a reflection representation? By the results of #13270, it is possible to choose the vectors $\alpha_i \in V$ and $\alpha_i^\vee \in V^*$ to be anything, as long as
$$S_{\left\lfloor \frac{m-2}{2} \right \rfloor}(t) (S_{\left\lfloor \frac{m-1}{2} \right \rfloor}(t) + S_{\left\lfloor \frac{m-3}{2} \right \rfloor}(t)) = S_{\left\lfloor \frac{m-1}{2} \right \rfloor}(t) (S_{\left\lfloor \frac{m}{2} \right \rfloor}(t) + S_{\left\lfloor \frac{m-2}{2} \right \rfloor}(t)) = 0 ,$$
for all $i, i'$, where $t = \alpha_i^\vee(\alpha_{i'}) \alpha_{i'}^\vee(\alpha_{i}) - 2$ and $m = M_{i, i'}$. Over the real numbers, it suffices that $\alpha_i^\vee(\alpha_{i'}) \alpha_{i'}^\vee(\alpha_{i}) = 4 \cos^2(j \pi / m)$, where $0 < j < m$.

Suppose that the ring $R$ is ordered. Let us say that $\rho$ is a geometric representation if it is a reflection representation, the $\alpha_i$ are linearly independent, and for all $i, i'$ and all integers $k$ with $0 \leq j < M_{i, i'}$, we have that
$$\rho(\underbrace{\cdots s_i s_{i'} s_i s_{i'}}_{j})\alpha_i$$
is a nonnegative linear combination of $\alpha_i$ and $\alpha_{i'}$. Here, there are $j$ terms in the product $\cdots s_i s_{i'} s_i s_{i'}$.

How does one construct a geometric representation? Again, by the results of #13270, it suffices that for all $i, i'$, we have $\alpha_i^\vee(\alpha_{i'}) \leq 0$, and $S_j(t) \geq 0$ for $j \leq M_{i, i'} / 2 - 1$, where again $t = \alpha_i^\vee(\alpha_{i'}) \alpha_{i'}^\vee(\alpha_{i}) - 2$. Over the real numbers, this is equivalent to the condition that the numbers $k_{i, i'} = \alpha_i^\vee(\alpha_{i'})$ satisfy the conditions 1–5 above.

With these definitions and lemmas, it should still be possible to construct geometric representations in the traditional way, but there will be a more general notion of "a" geometric representation, and the construction can be done over any ring.

• #13133
• #13195
• #13270
• Define a structure for matrices that satisfy a suitable generalization of conditions 1–5 above to any ordered ring. Provide definitions for constructing such matrices over $\mathbb{R}$ and $\mathbb{Z}$. Also, define the "standard" matrix over $\mathbb{R}$, with entries $-2 \cos(\pi / M_{i, i'})$. Current progress: https://github.com/leanprover-community/mathlib4/compare/master...trivial1711-generalized-cartan
• Define reflection representations.
• Define "a" geometric representation and the associated matrix. Also define "the" geometric representation with an associated matrix.
• Generalize #12880 to all geometric representations.
• (Optional) Define what it means for a generalized Cartan matrix to be symmetrizable and show that in this case, the corresponding geometric representation has an invariant bilinear form.
• (Later) Define the set of roots of a geometric representation and use them to prove the exchange properties. Maybe it's best to leave this to https://github.com/NUS-Math-Formalization/coxeter.

Start with the unchecked generalized-Cartan-matrix item and the results of #13270; the issue's current progress is in the trivial1711-generalized-cartan comparison. Define the suitable ordered-ring matrix structure and its constructions over ℝ and ℤ, then continue with the separately listed reflection and geometric representation work.