Motivation

The fundamental lemma is a family of identities between orbital integrals on a reductive group and stable orbital integrals on a smaller group attached to it, its endoscopic group. Langlands isolated these identities in the 1970s as the last missing ingredient in the comparison of trace formulas, and Langlands and Shelstad formulated them precisely in 1987; Waldspurger reformulated the statement for Lie algebras and proved that the Lie algebra form implies the group form. The Lie algebra statement was proved in equal characteristic by Bao Chau Ngo in Le lemme fondamental pour les algebres de Lie, Publ. Math. IHES 111 (2010), 1-169 (DOI), by a global geometric argument built on the Hitchin fibration; Waldspurger's earlier work transfers the result to mixed characteristic. The identity is the engine behind the stabilization of the trace formula and behind the computation of the cohomology of Shimura varieties.

Both sides of the identity carry a normalizing factor built from the discriminant, and the exact power of $q$ relating the two normalizations is fixed by a purely root-theoretic computation carried out in Ngo's §1.10-§1.11. That computation is the subject of this mission. It is self-contained, it uses no geometry, and it is the first piece of the paper that can be stated in Lean today.

Setting

Let $G$ be a split reductive group over a field with maximal torus $T$, character lattice $X^*(T)$, cocharacter lattice $X_*(T)$, root system $\Phi \subset X^*(T)$ and Weyl group $W$. Write $\mathfrak{t}$ for the Cartan subalgebra, so that each root $\alpha$ has a differential $d\alpha$, a linear form on $\mathfrak{t}$. Ngô's discriminant is the product

$$D_G \;=\; \prod_{\alpha \in \Phi} d\alpha ,$$

a $W$-invariant polynomial function on $\mathfrak{t}$ and hence a function on the space $\mathfrak{c} = \mathfrak{t} /\!/ W$ of characteristic polynomials.

An endoscopic datum is an element $\kappa$ of the dual torus $\hat{T} = \operatorname{Hom}(X_*(T), \mathbb{G}_m)$. The endoscopic group $H$ attached to it is the group whose root system is

$$\Phi_H \;=\; \{\alpha \in \Phi \;:\; \kappa(\alpha^\vee) = 1\} ,$$

with Weyl group $W_H \subset W$ and its own discriminant $D_H = \prod_{\alpha \in \Phi_H} d\alpha$. Choose a subset $\Lambda \subset \Phi - \Phi_H$ containing exactly one root out of each pair $\{\alpha, -\alpha\}$ of opposite roots outside $\Phi_H$, and set

$$R^G_H \;=\; \prod_{\alpha \in \Lambda} d\alpha .$$

Finally let $F$ be a non-archimedean local field with valuation $v$ and residue cardinality $q$, and recall Ngô's normalizing factors $\Delta_G(a) = q^{-v(D_G(a))/2}$ and $\Delta_H(a_H) = q^{-v(D_H(a_H))/2}$.

Formalization targets

Goal (1.11.3): the transfer factor identity

$$v\bigl(D_G(a)\bigr) \;=\; v\bigl(D_H(a_H)\bigr) \;+\; 2\, v\bigl(R^G_H(a_H)\bigr)$$

for a point $a_H$ of the endoscopic Cartan with image $a$. Equivalently $\Delta_H(a_H)\Delta_G(a)^{-1} = q^{\,r}$ with $r = v(R^G_H(a_H))$: this is exactly what lets one pass between the two forms of the fundamental lemma, $O^{\kappa}_a(\mathbf{1}_{\mathfrak{g}}) = q^{\,r} SO_{a_H}(\mathbf{1}_{\mathfrak{h}})$ and $\Delta_G(a) O^{\kappa}_a(\mathbf{1}_{\mathfrak{g}}) = \Delta_H(a_H) SO_{a_H}(\mathbf{1}_{\mathfrak{h}})$.

Milestones

The identity above is the image under $v$ of the divisor identity $\nu^* D_G = D_H + 2 R^G_H$ of 1.10.3, which in turn rests on the fact that $R^G_H$ — which depends on a choice of $\Lambda$ — is nevertheless $W_H$-invariant, and on the fact that $\Phi_H$ really is a root subsystem. The milestone list follows that order.

Significance

Theorem 1 of Ngô's paper, the Langlands-Shelstad conjecture for Lie algebras, is the identity $\Delta_G(a) O^{\kappa}_a(\mathbf{1}_{\mathfrak{g}}, dt) = \Delta_H(a_H) SO_{a_H}(\mathbf{1}_{\mathfrak{h}}, dt)$ for corresponding regular semisimple stable classes, under the hypothesis that twice the Coxeter number of $G$ is smaller than the residue characteristic. Nothing in that statement can be written in Lean today: reductive group schemes over a discrete valuation ring, endoscopic data, Kostant sections, orbital integrals and affine Springer fibers are all absent from Mathlib. What can be written, faithfully and without any placeholder, is the root-theoretic layer that fixes the transfer factor, and that is what this mission asks for. It is a genuine prerequisite: the two displayed forms of Theorem 1 differ precisely by the identity above.

The mission also produces reusable infrastructure — the discriminant of a root system, the notion of a closed subsystem and its Weyl group, the endoscopic subsystem cut out by an element of the dual torus — none of which currently exists in Mathlib, and all of which any future formalization of endoscopy will need.

Difficulty

Only one of the four milestones is a routine manipulation. Splitting $\Phi - \Phi_H$ into pairs $\{\alpha,-\alpha\}$ and collecting squares is bookkeeping; that $D_G$ is $W$-invariant is immediate because $W$ permutes $\Phi$. The content is in Lemma 1.10.2: $\Lambda$ is not stable under $W_H$, so $w \in W_H$ carries $\prod_{\alpha\in\Lambda} d\alpha$ to $(-1)^{m(w)} \prod_{\alpha\in\Lambda} d\alpha$, where $m(w)$ counts the roots of $\Lambda$ sent into $-\Lambda$; the claim is that $m(w)$ is always even. The naive attempt — check it on the generating reflections of $W_H$ — is exactly where a careless argument goes wrong, since it is false for reflections in roots outside $\Phi_H$. Ngô's argument identifies the sign with $(-1)^{\ell_G(w)} (-1)^{\ell_H(w)}$, the ratio of the sign characters of $W$ and $W_H$, and observes that both compute the determinant of $w$ acting on the same reflection representation.

Formalization scope

Root systems are modelled with Mathlib's RootPairing ι R M N: the module $M$ plays the role of $X^*(T)$, the module $N$ the role of $X_*(T)$ and of the Cartan on which the differentials $d\alpha$ are evaluated, and $P.root' i$ is the linear form $d\alpha$. The endoscopic subsystem is cut out by an element $\kappa$ of the dual torus, taken as a group homomorphism from the cocharacter lattice to an arbitrary commutative group, and is expressed over $\mathbb{Z}$ coefficients as in the definition of a root datum. Products over $\Phi$ and $\Phi_H$ are finite products over a Fintype index, and a choice $\Lambda$ is a Finset satisfying an exclusive-or condition, which automatically rules out the degenerate case $\alpha = -\alpha$.

The identity 1.10.3 is stated as an identity of functions on the Cartan rather than as an identity of divisors, so the unit $(-1)^{|\Lambda|}$ is carried explicitly rather than discarded. Lemma 1.10.2 is stated over $\mathbb{Q}$ for an honest root system, since the sign argument uses the reflection representation. The goal 1.11.3 is stated for an additive valuation with values in $\mathbb{Z} \cup \{\infty\}$, which is what makes the two sides comparable when a discriminant vanishes.

There is no trivializing formalization here: the hypotheses of every item are satisfiable — any root system with any closed subsystem and any choice of $\Lambda$ gives an instance — so none of the statements is vacuous, and none of them is an identity between two occurrences of the same expression.

Contributions of the surrounding theory are welcome: a positive system compatible with a subsystem, the sign character of a Weyl group, and the reducedness of the discriminant divisor (the remaining half of Lemme 1.10.1) are all natural next steps.

Selected references

• Bao Chau Ngo, Le lemme fondamental pour les algebres de Lie, Publ. Math. IHES 111 (2010), 1-169. https://doi.org/10.1007/s10240-010-0026-7
• R. Langlands, D. Shelstad, On the definition of transfer factors, Math. Ann. 278 (1987), 219-271. https://doi.org/10.1007/BF01458070
• J.-L. Waldspurger, Endoscopie et changement de caracteristique, J. Inst. Math. Jussieu 5 (2006), 423-525. https://doi.org/10.1017/S1474748006000041
• R. Kottwitz, Transfer factors for Lie algebras, Represent. Theory 3 (1999), 127-138. https://doi.org/10.1090/S1088-4165-99-00077-6
• T. Hales, A statement of the fundamental lemma, in Harmonic Analysis, the Trace Formula, and Shimura Varieties, Clay Math. Proc. 4 (2005), 643-658. https://arxiv.org/abs/math/0312227