Weyl Groups

The Weyl group \(W\) of a root system (or root datum, or reductive group) is the finite group generated by the reflections through the roots. It is the symmetry group of the combinatorial structure of the group and controls almost every refined invariant: character formula, Bruhat decomposition, Hecke algebra, geometry of the flag variety.

Definition (abstract)

Let \(\Phi \subseteq V\) be a root system in a Euclidean space \(V\). The Weyl group of \(\Phi\) is the subgroup \[ W \;=\; W(\Phi) \;\subseteq\; O(V) \] generated by the reflections \[ s_\alpha(x) \;=\; x - \langle x, \alpha^\vee \rangle \alpha, \qquad \alpha \in \Phi. \]

By the root-string axioms, \(W\) permutes \(\Phi\); since \(\Phi\) is finite, \(W \hookrightarrow \mathrm{Sym}(\Phi)\) is finite.

Simple reflections and Coxeter presentation

Fix a base \(\Delta = \{\alpha_1, \dots, \alpha_r\}\) and let \(s_i = s_{\alpha_i}\). Then:

\(W\) is generated by \(\{s_1, \dots, s_r\}\) (the simple reflections).
The relations are: \[ s_i^2 = 1, \qquad (s_i s_j)^{m_{ij}} = 1 \] where \(m_{ij}\) is the order of \(s_i s_j\), determined by the angle between \(\alpha_i\) and \(\alpha_j\): \[ m_{ij} \in \{2, 3, 4, 6\} \quad \text{for } i \ne j. \]

Thus \((W, \{s_i\})\) is a Coxeter system.

Definition (from a reductive group)

For a connected reductive group \(G\) over a field \(k\) with maximal torus \(T\) and normaliser \(N_G(T)\): \[ W(G, T) \;=\; N_G(T) / T. \]

Theorem. For \(G\) split, the abstract Weyl group of the root datum and the geometric Weyl group \(N_G(T)/T\) are canonically isomorphic.

For \(G\) non-split, the rational Weyl group is \(W(G, T)(k) = (N_G(T)/T)(k)\), often a proper subgroup of the absolute one and equal to the \(\Gamma\)-invariants of the absolute Weyl group.

Length function and Bruhat order

For \(w \in W\), the length \(\ell(w)\) is the minimum number of simple reflections needed to write \(w = s_{i_1} \cdots s_{i_\ell}\). Equivalently: \[ \ell(w) \;=\; \#\{\alpha \in \Phi^+ : w(\alpha) \in \Phi^-\}. \]

The Bruhat order \(\le\) on \(W\) is generated by: \[ v \le w \iff v \text{ can be obtained from } w \text{ by deleting letters in some reduced expression}. \]

\((W, \le)\) is a finite, ranked, self-dual poset with rank function \(\ell\). The Hasse diagram of \((W, \le)\) is the Bruhat order diagram.

The longest element

There is a unique element \(w_0 \in W\) of maximal length \(\ell(w_0) = \#\Phi^+\). It satisfies \(w_0^2 = 1\) and \(w_0(\Phi^+) = \Phi^-\). For \(\mathrm{GL}_n\), \(w_0 = (n, n-1, \dots, 1)\) (the reverse permutation).

Examples

Type	\(W\)	\(\|W\|\)
\(A_{n-1}\)	\(S_n\)	\(n!\)
\(B_n\), \(C_n\)	hyperoctahedral \(B_n = \{\pm 1\}^n \rtimes S_n\)	\(2^n n!\)
\(D_n\)	subgroup of \(B_n\) with even sign changes	\(2^{n-1} n!\)
\(G_2\)	dihedral of order 12	12
\(F_4\)	order 1152	1152
\(E_6\)	order 51840	51840
\(E_7\)	order 2903040	2903040
\(E_8\)	order 696729600	696729600

Affine Weyl group

For a reductive group over a local field, the affine Weyl group is \[ W_{\mathrm{aff}} \;=\; W \ltimes \mathbb{Z}\Phi^\vee, \] the semi-direct product of \(W\) with the coroot lattice. It is the Weyl group of the affine root system.

The extended affine Weyl group \(\tilde W = W \ltimes X_*\) includes all translations by cocharacters.

Role

Bruhat decomposition. \(G = \sqcup_{w \in W} BwB\); cells indexed by \(W\), dimensions by \(\ell\).
Schubert calculus. Cohomology of \(G/B\) has basis indexed by \(W\); intersection products encoded by Schubert structure constants.
Character formula. Weyl character formula uses the alternating sum over \(W\) and the longest element \(w_0\).
Hecke algebras. Iwahori–Hecke algebra \(\mathcal{H}(W)\) is a deformation of the group algebra \(\mathbb{Z}[W]\), foundational for Kazhdan–Lusztig theory.
Demazure operators. Operators \(\partial_{s_i}\) on the character ring, used to construct irreducible characters and resolutions of Schubert varieties.

Mathlib coverage and formalization gaps

Present in Mathlib4:

RootPairing.weylGroup — the Weyl group defined as the subgroup of Aut(M) generated by the simple reflections {s_i}. Located in Mathlib.LinearAlgebra.RootSystem.WeylGroup and related modules.
Permutation representation: The action of weylGroup on the root index set ι (via reflectionPerm) is proved to give a group homomorphism weylGroup →* Sym(ι).
CoxeterSystem — an independent abstract Coxeter group framework in Mathlib.GroupTheory.Coxeter.Basic, with generators and Coxeter relations defined abstractly.

Formalization gaps (explicit TODOs):

Finiteness: The statement "RootPairing.weylGroup is finite" is an explicit TODO. The proof would use the embedding into Sym(ι) (since the root index set ι is finite for a finite root pairing), but this embedding is not yet established.
Faithfulness: The permutation representation weylGroup →* Sym(ι) is not yet proved to be injective (faithful). This is an explicit TODO.
No connection to CoxeterSystem: There is currently no theorem in Mathlib4 connecting RootPairing.weylGroup to CoxeterSystem. The isomorphism between the Weyl group (defined geometrically from the root pairing) and the abstract Coxeter group (defined by the Coxeter matrix from the Dynkin diagram) is not formalized.
Matsumoto's theorem (any two reduced expressions for \(w\) are related by braid relations) is stated as a TODO in Mathlib.GroupTheory.Coxeter.Basic.

For a detailed discussion of these gaps and the Coxeter presentation theorem, see Weyl Groups as Coxeter Groups.