Ngo's Fundamental Lemma I: Discriminant, Resultant and the Transfer FactorResearch Paper
## 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](https://doi.org/10.1007/s10240-010-0026-7)), 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
7 thms1 active userReviewed
🏆Completed
Captain: Lucas
Ngo's Fundamental Lemma II: Isogenies of Root Data and Paired GroupsResearch Paper
## Motivation
Waldspurger's **non-standard fundamental lemma** is an identity between stable orbital
integrals on the Lie algebras of two reductive groups that are not isomorphic, and not even
isogenous as algebraic groups, but whose root data become identified after tensoring with
$\mathbb{Q}$. The basic example is the pair $(\mathrm{Sp}_{2n}, \mathrm{SO}_{2n+1})$, whose
root systems $C_n$ and $B_n$ are exchanged by Langlands duality; the identity is what allows
the *twisted* fundamental lemma to be deduced from the ordinary one. Waldspurger formulated
the conjecture in *L'endoscopie tordue n'est pas si tordue* (2008); it is Theorem 1.12.7 of
Bao Chau Ngo, *Le lemme fondamental pour les algebres de Lie*, Publ. Math. IHES **111** (2010),
1-169 ([DOI](https://doi.org/10.1007/s10240-010-0026-7)), proved there in equal characteristic
by the same Hitchin-fibration argument that gives the ordinary fundamental lemma.
Before any of that geometry can start, the two sides have to be compared: one needs a single
Cartan subalgebra, a single Weyl group and a single space of characteristic polynomials serving
both groups at once. Producing that comparison is a self-contained piece of linear algebra over
the root data, carried out in Ngo's §1.12, and it is what this mission asks for.
## Setting
Let $G_1$ and $G_2$ be split reductive groups over a field, pinned, with maximal tori $T_1$ and
$T_2$. Each is determined by its **root datum**
$(X^*(T_i), X_*(T_i), \Phi_i, \Phi_i^\vee, \Delta_i)$, where $\Phi_i$ is the set of roots,
$\Phi_i^\vee$ the set of coroots and $\Delta_i$ the set of simple roots singled out by the
pinning.
An **isogeny of root data** between $G_1$ and $G_2$ (Ngo, Definition 1.12.1) is a pair of
isomorphisms of $\mathbb{Q}$-vector spaces
$$ \psi^* : X^*(T_2)\otimes\mathbb{Q} \longrightarrow X^*(T_1)\otimes\mathbb{Q}, \qquad
\psi_* : X_*(T_1)\otimes\mathbb{Q} \longrightarrow X_*(T_2)\otimes\mathbb{Q} $$
which are transposes of one another, such that $\psi^*$ carries the set of lines
$\mathbb{Q}\alpha_2$ ($\alpha_2 \in \Phi_2$) bijectively onto the set of lines
$\mathbb{Q}\alpha_1$ ($\alpha_1\in\Phi_1$), matching lines of simple roots with lines of simple
roots, and such that $\psi_*$ has the same property for the lines spanned by coroots. Two
semisimple groups with the same adjoint group are isogenous in this sense; so are a group and
its Langlands dual, the interesting cases being $B_n \leftrightarrow C_n$, $F_4$ and $G_2$,
where a short root $\alpha$ is sent to $\check\alpha$ and a long root to $n\check\alpha$ with
$n = |\alpha_{\mathrm{long}}|^2/|\alpha_{\mathrm{short}}|^2$. Groups obtained by twisting a
pair of isogenous pinned groups by a common torsor are called **paired**.
A prime $p$ is **good with respect to $\psi^*$** when it divides neither of the indices
$$ \bigl|X_*(T_1)/(X_*(T_1)\cap X_*(T_2))\bigr| \quad\text{and}\quad
\bigl|X_*(T_2)/(X_*(T_1)\cap X_*(T_2))\bigr|, $$
the two lattices being compared inside the single $\mathbb{Q}$-vector space identified by
$\psi_*$.
## Formalization targets
### Goal (1.12.4 and 1.12.6): the Weyl groups are identified compatibly
$$ \psi_* \, w \, \psi_*^{-1} \in W_2 \quad \text{for all } w \in W_1,
\qquad\text{and conversely,} $$
i.e. conjugation by $\psi_*$ carries the Weyl group $W_1$ acting on
$X_*(T_1)\otimes\mathbb{Q}$ onto the Weyl group $W_2$ acting on $X_*(T_2)\otimes\mathbb{Q}$.
Ngo's reason is that the reflection attached to a root depends only on the line through that
root, so the bijection of root lines transports reflections to reflections. This equivariance
is what makes the induced isomorphism $\mathfrak{t}_1 \to \mathfrak{t}_2$ descend to an
isomorphism $\nu : \mathfrak{c}_{G_1} \to \mathfrak{c}_{G_2}$ of the spaces of characteristic
polynomials, which is Lemme 1.12.6 and which is what allows two points $a_1$ and $a_2$ with
$\nu(a_1) = a_2$ to be compared at all.
### Milestones
Two steps lead there: the reflection computation that makes a matched pair of root lines give
a matched pair of reflections, and the integral statement behind Ngo's good-characteristic
hypothesis — that when the two indices above are invertible in the base ring, the two lattices
become identified after base change.
## Significance
Theorem 1.12.7, the non-standard fundamental lemma, asserts that for two paired groups over
$O_v = k[[\varpi]]$ with residue characteristic exceeding twice the Coxeter numbers, and for
points $a_1$ and $a_2$ corresponding under $\nu$, the stable orbital integrals of the
characteristic functions of $\mathfrak{g}_1(O_v)$ and $\mathfrak{g}_2(O_v)$ agree. Waldspurger
showed that this identity, together with the ordinary fundamental lemma, implies the twisted
fundamental lemma. None of the objects in that statement — reductive group schemes over a
discrete valuation ring, orbital integrals, Haar measures on the centralizer tori — exists in
Mathlib today. The comparison of §1.12 does not need any of them: it is a statement about
lattices, root systems and Weyl groups, and it is a strict prerequisite, since without the
isomorphism $\nu$ the two sides of Theorem 1.12.7 cannot even be matched up.
Beyond this paper, the notion of an isogeny of root data and the good-characteristic base
change of a pair of lattices are reusable: they are the standard bookkeeping behind Langlands
duality for split groups, and neither is currently available.
## Difficulty
The reflection step looks like a one-line computation and is one — but only once the two
proportionality constants are known to agree. If $\psi^*(\alpha_2) = c\,\alpha_1$ and
$\psi_*(\alpha_1^\vee) = c'\,\alpha_2^\vee$, the conjugate of $s_{\alpha_1}$ is $s_{\alpha_2}$
exactly when $c = c'$, and that is forced by transposition together with
$\langle\alpha,\alpha^\vee\rangle = 2$. The genuine difficulty in the goal is different: the
definition only says that $\psi^*$ and $\psi_*$ permute *lines*, so one has to show that the
bijection induced on root lines and the bijection induced on coroot lines are the *same*
bijection. A solver who assumes this without proof has assumed the substance of 1.12.4.
The lattice milestone has its own trap: the quotient $\Lambda_1/(\Lambda_1\cap\Lambda_2)$ must
be shown to have vanishing $\mathrm{Tor}$ after base change, not merely to vanish, or the
inclusion becomes only surjective.
## Formalization scope
Root data are modelled by Mathlib's `RootPairing ι ℚ M N`, with $M$ the character space, $N$
the cocharacter space, and rational coefficients throughout, so that "tensoring with
$\mathbb{Q}$" is built into the ambient objects rather than performed explicitly. A choice of
simple roots is recorded as a subset of the index type rather than as a `RootPairing.Base`;
nothing in the statements depends on that subset beyond its role in the definition of an
isogeny. The Weyl group is the subgroup of linear automorphisms of the cocharacter space
generated by the coreflections, which is the form in which it acts on the Cartan.
The goal is stated as a two-sided intertwining property rather than as an equality of
subgroups: every element of $W_1$ is intertwined by $\psi_*$ with some element of $W_2$ and
conversely. This avoids introducing a conjugation homomorphism, and it is the form in which
the statement is used. Both root pairings in the goal are required to be finite, reduced root
systems, matching Ngo's hypothesis that $G_1$ and $G_2$ are reductive groups.
The good-characteristic condition is formalized exactly as Ngo writes it, by the invertibility
in the base ring of the two indices, each expressed as the cardinality of an explicit quotient
group; the conclusion is the bijectivity of the map induced on the tensor product by the
inclusion of the intersection. If a quotient were infinite its cardinality is reported as $0$,
and invertibility of $0$ then forces the base ring to be trivial, so no false statement hides
in that corner.
No statement here is vacuous: any pair consisting of a root system and itself, with $\psi^*$
and $\psi_*$ the identity, satisfies every hypothesis, and the pair $(B_n, C_n)$ gives the
intended non-trivial instances.
## 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
- J.-L. Waldspurger, *L'endoscopie tordue n'est pas si tordue*, Mem. Amer. Math. Soc. 908 (2008). https://doi.org/10.1090/memo/0908
- J.-L. Waldspurger, *Le lemme fondamental implique le transfert*, Compositio Math. 105 (1997), 153-236. https://doi.org/10.1023/A:1000103112268
- T. A. Springer, *Reductive groups*, in Automorphic Forms, Representations and L-functions, Proc. Sympos. Pure Math. 33 (1979), 3-27. https://doi.org/10.1090/pspum/033.1