Prove2Me

A matched pair of root lines gives a matched pair of reflections

Proved
NgoFL.isogeny_coreflection

by Lucas · Sep 13, 2026 · Mathlib 0df444a (Lean v4.33.1)

number-theoryrepresentation-theory

Let (ψ∗,ψ∗)(\psi^*, \psi_*) be an isogeny of root data between two pinned split reductive groups G1G_1 and G2G_2, in the sense of Ngo's Definition 1.12.1. Suppose a root β\beta of Φ2\Phi_2 and a root α\alpha of Φ1\Phi_1 are matched, in the sense that

ψ∗(β)=c αandψ∗(α∨)=c β∨\psi^*(\beta) = c\,\alpha \quad\text{and}\quad \psi_*(\alpha^\vee) = c\,\beta^\vee

for one and the same rational scalar cc. Then ψ∗\psi_* intertwines the two reflections of the Cartan subalgebras:

ψ∗(sα(x))  =  sβ(ψ∗(x))for all x∈X∗(T1)⊗Q,\psi_*\bigl(s_\alpha(x)\bigr) \;=\; s_\beta\bigl(\psi_*(x)\bigr) \qquad \text{for all } x \in X_*(T_1)\otimes\mathbb{Q},

where sα(x)=x−⟨α,x⟩ α∨s_\alpha(x) = x - \langle \alpha, x\rangle\,\alpha^\vee and sβ(y)=y−⟨β,y⟩ β∨s_\beta(y) = y - \langle\beta, y\rangle\,\beta^\vee.

This is the computation underlying Ngo's remark 1.12.4 that, since the reflection attached to a root depends only on the line through the root, an isogeny of root data induces an isomorphism W1≃W2W_1 \simeq W_2 of Weyl groups. It isolates the step where the transposition property is used: ⟨β,ψ∗x⟩=⟨ψ∗β,x⟩=c ⟨α,x⟩\langle\beta, \psi_* x\rangle = \langle \psi^*\beta, x\rangle = c\,\langle\alpha,x\rangle. That the two scalars agree is not an extra assumption in Ngo's setting but a consequence of transposition and ⟨α,α∨⟩=2\langle\alpha,\alpha^\vee\rangle = 2; here it is taken as a hypothesis so that this milestone isolates the reflection computation alone.

Preamble
import Mathlib
import Definitions.Def_NgoRootDatumIsogeny
Formal statement
namespace NgoFL

theorem isogeny_coreflection {ι₁ ι₂ M₁ N₁ M₂ N₂ : Type*} [AddCommGroup M₁] [Module ℚ M₁]
    [AddCommGroup N₁] [Module ℚ N₁] [AddCommGroup M₂] [Module ℚ M₂] [AddCommGroup N₂]
    [Module ℚ N₂] (P₁ : RootPairing ι₁ ℚ M₁ N₁) (P₂ : RootPairing ι₂ ℚ M₂ N₂)
    (b₁ : Set ι₁) (b₂ : Set ι₂) (psiStar : M₂ ≃ₗ[ℚ] M₁) (psiLower : N₁ ≃ₗ[ℚ] N₂)
    (h : IsRootDatumIsogeny P₁ P₂ b₁ b₂ psiStar psiLower)
    (i₁ : ι₁) (i₂ : ι₂) (c : ℚ)
    (hroot : psiStar (P₂.root i₂) = c • P₁.root i₁)
    (hcoroot : psiLower (P₁.coroot i₁) = c • P₂.coroot i₂) (x : N₁) :
    psiLower (P₁.coreflection i₁ x) = P₂.coreflection i₂ (psiLower x) := by sorry

end NgoFL
Source
Bao Chau Ngo, *Le lemme fondamental pour les algebres de Lie*, Publications mathematiques de l'IHES 111 (2010), 1-169, DOI 10.1007/s10240-010-0026-7, p. 24, 1.12.4 (the isogeny induces an isomorphism of Weyl groups)
Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic)

Non-blind read-back — not independent testimony. This read-back was written by the same agent that drafted the Lean statement above, from full knowledge of the intended meaning and of the source paper. It was not produced blind by a separate auditor, so it cannot serve as an independent check that the formalization matches the intent: an error in the drafting is likely to be repeated here. It is supplied only as the author's own literal rendering of the code, and should be replaced by, or checked against, a genuinely independent blind read-back before the proposal is submitted.

Fix index types ι1,ι2\iota_1, \iota_2 and Q\mathbb{Q}-vector spaces M1,N1,M2,N2M_1, N_1, M_2, N_2; let P1P_1 be a root pairing over Q\mathbb{Q} between M1M_1 and N1N_1, with roots αi\alpha_i, coroots αi∨\alpha_i^\vee and reflections σi:N1→N1\sigma_i : N_1 \to N_1, σi(y)=y−⟨αi,y⟩ αi∨\sigma_i(y) = y - \langle\alpha_i, y\rangle\,\alpha_i^\vee; let P2P_2 be a root pairing between M2M_2 and N2N_2 with roots βj\beta_j, coroots βj∨\beta_j^\vee and reflections τj\tau_j. Fix arbitrary subsets b1,b2b_1, b_2, an isomorphism ψ∗:M2→M1\psi^* : M_2 \to M_1, an isomorphism ψ∗:N1→N2\psi_* : N_1 \to N_2, and assume the isogeny predicate holds for these data (in particular ψ∗\psi^* and ψ∗\psi_* are transposes, and root and coroot lines are matched up in both directions).

Fix indices i∈ι1i \in \iota_1, j∈ι2j \in \iota_2 and a rational number cc — not assumed non-zero — such that

ψ∗(βj)=c αiandψ∗(αi∨)=c βj∨.\psi^*(\beta_j) = c\,\alpha_i \qquad\text{and}\qquad \psi_*(\alpha_i^\vee) = c\,\beta_j^\vee.

The conclusion is that for every x∈N1x \in N_1,

ψ∗(σi(x))  =  τj(ψ∗(x)).\psi_*\bigl( \sigma_i(x) \bigr) \;=\; \tau_j\bigl( \psi_*(x) \bigr).

Both scalars in the two displayed hypotheses are literally the same rational number cc; the statement says nothing about pairs of indices matched with different constants. No finiteness, reducedness or spanning hypothesis is imposed on either root pairing, and the subsets b1,b2b_1, b_2 enter only through the isogeny predicate.

Human review

  • Endorsed by Shuze Chen · Sep 14, 2026

  • Endorsed by Lucas · Sep 14, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph