Weyl Groups as Coxeter Groups

The Weyl group of a finite root system, generated by simple reflections, satisfies the Coxeter presentation. This connects the concrete definition (reflections in a Euclidean space) with the abstract combinatorial structure of Coxeter groups.

The Coxeter presentation theorem

Theorem. Let \(\Phi\) be a finite root system with simple roots \(\Delta = \{\alpha_1, \dots, \alpha_n\}\) and simple reflections \(s_i = s_{\alpha_i}\). The Weyl group \(W\) is isomorphic, as an abstract group, to the Coxeter group with generators \(\{s_1, \dots, s_n\}\) and relations \[ (s_i s_j)^{m_{ij}} = 1, \] where the Coxeter exponents \(m_{ij}\) are determined by the Cartan integers \(\langle \alpha_i, \alpha_j^\vee \rangle \cdot \langle \alpha_j, \alpha_i^\vee \rangle\):

Coxeter weight	Bond type	\(m_{ij}\)
0	No bond (orthogonal)	2
1	Single bond	3
2	Double bond (\(B/C\))	4
3	Triple bond (\(G_2\))	6

Here \(m_{ii} = 1\) (so \(s_i^2 = 1\)) is included in the convention. The Coxeter matrix \((m_{ij})\) is symmetric with \(m_{ij} \ge 2\) for \(i \ne j\).

This theorem asserts two things: (1) the listed relations hold in \(W\) (easy, follows from the geometry of reflections), and (2) these are all relations — i.e., the natural map from the abstract Coxeter group to \(W\) is an isomorphism (the hard part, requiring analysis of reduced expressions).

Matsumoto's theorem

Theorem (Matsumoto 1964). Any two reduced expressions for the same element \(w \in W\) are related by a finite sequence of braid relations: \[ s_i s_j s_i \cdots = s_j s_i s_j \cdots \qquad (m_{ij} \text{ factors on each side}). \]

Equivalently, the length function \(\ell: W \to \mathbb{Z}_{\ge 0}\), defined as the minimum number of simple reflections in any expression for \(w\), is well-defined and satisfies: \[ \ell(w) \;=\; |\mathrm{Inv}(w)| \;=\; \#\{\alpha \in \Phi^+ : w(\alpha) \in \Phi^-\}. \] This is the equality between the combinatorial length (word length in the generators) and the geometric length (inversion count).

Matsumoto's theorem implies that the Hecke algebra \(\mathcal{H}(W, q)\) is well-defined: the elements \(T_w\) indexed by \(w \in W\) do not depend on the choice of reduced expression.

Bruhat order

The Bruhat order (Chevalley–Bruhat order) on \(W\) is defined by: \[ v \le w \iff \text{some (equivalently, every) reduced expression for } v \text{ appears as a subword of some reduced expression for } w. \]

This poset structure on \(W\) is distinct from — but related to — the closure order on Schubert varieties \(\overline{BwB/B}\) in the flag variety \(G/B\): one has \(v \le w\) if and only if \(BvB/B \subseteq \overline{BwB/B}\), so the two orders coincide.

The height function RootPairing.Base.height in Mathlib assigns to each positive root \(\alpha \in \Phi^+\) the total coefficient in the simple root expansion \(\alpha = \sum_i c_i \alpha_i\): \(\mathrm{ht}(\alpha) = \sum_i c_i\).

Formalization status in Mathlib4: EXPLICIT GAPS

Mathlib4 coverage (present):

RootPairing.weylGroup — the Weyl group defined as a subgroup of \(\mathrm{Aut}(M)\) generated by the simple reflections.
The permutation representation of weylGroup on the root set is proved.
CoxeterSystem — an independent, abstract Coxeter group infrastructure in Mathlib.GroupTheory.Coxeter.Basic.
RootPairing.Base.height — the height function on the positive root set.

Known formalization gaps:

Finiteness of weylGroup: The theorem "RootPairing.weylGroup is a finite group" is an explicit TODO in Mathlib4's root system files. The proof would follow from the fact that weylGroup embeds into Sym(ι) (the finite symmetric group on the index type), but this embedding is not yet established in full generality.
Faithfulness: The statement that weylGroup acts faithfully on the root set (i.e.\ the permutation representation is injective) is an explicit TODO.
Connection to CoxeterSystem: There is currently no theorem in Mathlib4 connecting RootPairing.weylGroup to the abstract CoxeterSystem framework. The isomorphism between the Weyl group (as defined from the root pairing) and the Coxeter group (as defined abstractly from the Coxeter matrix) is not proved.
Matsumoto's theorem: Matsumoto's theorem (any two reduced expressions are related by braid relations) is stated as a TODO in Mathlib.GroupTheory.Coxeter.Basic.

These gaps are significant for any application that requires using Weyl groups as Coxeter groups (e.g.\ defining Kazhdan–Lusztig polynomials, Hecke algebras, or the Bruhat order via subword characterizations in Mathlib).

References