Demazure's character formula for the longest element

Let P be a root datum with a base, weight lattice M and Weyl group W, and let Dᵢ be the integral Demazure operator of the simple root αᵢ on ℤ[M] (RootPairing.demazureOperator). For a reduced word ω = (i₁, …, iᵣ) of the longest element w₀ of W write D_{w₀} = D_{i₁} ⋯ D_{iᵣ}; by word independence (RootPairing.prod_map_demazureOperator_eq_of_wordProd_eq) it does not depend on ω. This file proves Demazure's formula

Δ · D_{w₀}(f) = ∑_{w ∈ W} sgn(w) e^{-(ρ - w ρ)} w(f),

where Δ = ∏_{α > 0} (1 - e^{-α}) is the Weyl denominator and the right-hand side is the dot alternatization J(f) of TauCeti.LinearAlgebra.RootSystem.Weyl.Denominator.Integral. For f = e^λ the right-hand side is ∑_w sgn(w) e^{w ⬝ λ}, so D_{w₀}(e^λ) is Weyl's quotient ∑_w sgn(w) e^{w ⬝ λ} / Δ. This is the combinatorial side of the Weyl character formula and of the longest-word case of the Demazure character formula; identifying D_{w₀}(e^λ) with a formal character (of a module, or of the sections of a line bundle on the flag variety) is not done here.

The argument

Three facts combine.

• J ∘ Dᵢ = J. Put u = Dᵢ f. The localization identity (1 - e^{-αᵢ}) u = f - e^{-αᵢ} sᵢ(f) and the invariance sᵢ(u) = u give u - e^{-αᵢ} sᵢ(u) = f - e^{-αᵢ} sᵢ(f). Since J(e^{-αᵢ} sᵢ(g)) = -J(g), applying J gives 2 J(u) = 2 J(f).
• D_{w₀}(f) is Weyl-invariant. Each simple reflection sᵢ is a left descent of w₀, so w₀ has a reduced word beginning with i, and D_{w₀} = Dᵢ D_{w'} has image fixed by sᵢ.
• J is linear over the Weyl-invariant elements and J(1) = Δ (RootPairing.dotAlternatization_one).

Hence J(f) = J(D_{w₀} f) = D_{w₀}(f) · J(1) = Δ · D_{w₀}(f).

The longest element is described by the property used, that every simple reflection is a left descent; a reduced word with this property exists (RootPairing.exists_isReduced_forall_isLeftDescent).

Main results

• RootPairing.dotAlternatization_demazureOperator: J(Dᵢ f) = J(f).
• RootPairing.dotAlternatization_prod_map_demazureOperator: J(D_{i₁} ⋯ D_{iᵣ} f) = J(f) for every word.
• RootPairing.isWeylInvariant_prod_map_demazureOperator: D_{w₀}(f) is Weyl-invariant.
• RootPairing.weylDenominator_mul_prod_map_demazureOperator: Demazure's formula Δ · D_{w₀}(f) = J(f), and RootPairing.weylDenominator_mul_prod_map_demazureOperator_single, its value on e^λ.

References

• M. Demazure, Désingularisation des variétés de Schubert généralisées, Ann. Sci. École Norm. Sup. (4) 7 (1974), §2.
• J. C. Jantzen, Representations of Algebraic Groups, 2nd ed., Part II, §14.
• S. Kumar, Kac–Moody Groups, their Flag Varieties and Representation Theory, §8.2.

theorem RootPairing.isWeylInvariant_prod_map_demazureOperator {ι : Type u_1} {M : Type u_2} {N : Type u_3} [AddCommGroup M] [AddCommGroup N] (P : RootPairing ι ℤ M N) [Finite ι] (b : P.Base) [P.IsReduced] {ω : List ↥b.support} (hω : (TauCeti.weylCoxeterSystem P b).IsReduced ω) (hdesc : ∀ (i : ↥b.support), (TauCeti.weylCoxeterSystem P b).IsLeftDescent ((TauCeti.weylCoxeterSystem P b).wordProd ω) i) (f : AddMonoidAlgebra ℤ M) : TauCeti.IsWeylInvariant P ((List.map (fun (m : ↥b.support) => P.demazureOperator ↑m) ω).prod f)

The longest-element Demazure operator has Weyl-invariant image: the product of the Demazure operators along a reduced word of the longest element w₀ (an element of which every simple reflection is a left descent) sends every element of ℤ[M] to a Weyl-invariant one.

@[simp]

theorem RootPairing.dotAlternatization_demazureOperator {ι : Type u_1} {M : Type u_2} {N : Type u_3} [AddCommGroup M] [AddCommGroup N] (P : RootPairing ι ℤ M N) [Finite ι] (b : P.Base) [P.IsReduced] [Fintype ↥P.weylGroup] {i : ι} (hi : i ∈ b.support) (f : AddMonoidAlgebra ℤ M) : (P.dotAlternatization b) ((P.demazureOperator i) f) = (P.dotAlternatization b) f

The dot alternatization absorbs the Demazure operators: J(Dᵢ f) = J(f) for a simple root αᵢ.

theorem RootPairing.dotAlternatization_prod_map_demazureOperator {ι : Type u_1} {M : Type u_2} {N : Type u_3} [AddCommGroup M] [AddCommGroup N] (P : RootPairing ι ℤ M N) [Finite ι] (b : P.Base) [P.IsReduced] [Fintype ↥P.weylGroup] (ω : List ↥b.support) (f : AddMonoidAlgebra ℤ M) : (P.dotAlternatization b) ((List.map (fun (m : ↥b.support) => P.demazureOperator ↑m) ω).prod f) = (P.dotAlternatization b) f

The dot alternatization absorbs every product of Demazure operators of simple roots, J(D_{i₁} ⋯ D_{iᵣ} f) = J(f), whether or not the word is reduced.

theorem RootPairing.weylDenominator_mul_prod_map_demazureOperator {ι : Type u_1} {M : Type u_2} {N : Type u_3} [AddCommGroup M] [AddCommGroup N] (P : RootPairing ι ℤ M N) [Finite ι] (b : P.Base) [P.IsReduced] [Fintype ↥P.weylGroup] {ω : List ↥b.support} (hω : (TauCeti.weylCoxeterSystem P b).IsReduced ω) (hdesc : ∀ (i : ↥b.support), (TauCeti.weylCoxeterSystem P b).IsLeftDescent ((TauCeti.weylCoxeterSystem P b).wordProd ω) i) (f : AddMonoidAlgebra ℤ M) : TauCeti.weylDenominator P b * (List.map (fun (m : ↥b.support) => P.demazureOperator ↑m) ω).prod f = (P.dotAlternatization b) f

Demazure's formula for the longest element: for a reduced word ω of the longest element w₀ (an element of which every simple reflection is a left descent),

Δ · D_{w₀}(f) = ∑_{w ∈ W} sgn(w) e^{-(ρ - w ρ)} w(f),

where D_{w₀} is the product of the Demazure operators along ω, Δ is the Weyl denominator and the right-hand side is the dot alternatization (RootPairing.dotAlternatization_apply). Since Δ is not a zero divisor, this determines D_{w₀}(f).

theorem RootPairing.weylDenominator_mul_prod_map_demazureOperator_single {ι : Type u_1} {M : Type u_2} {N : Type u_3} [AddCommGroup M] [AddCommGroup N] (P : RootPairing ι ℤ M N) [Finite ι] (b : P.Base) [P.IsReduced] [Fintype ↥P.weylGroup] {ω : List ↥b.support} (hω : (TauCeti.weylCoxeterSystem P b).IsReduced ω) (hdesc : ∀ (i : ↥b.support), (TauCeti.weylCoxeterSystem P b).IsLeftDescent ((TauCeti.weylCoxeterSystem P b).wordProd ω) i) (lam : M) : TauCeti.weylDenominator P b * (List.map (fun (m : ↥b.support) => P.demazureOperator ↑m) ω).prod (AddMonoidAlgebra.single lam 1) = ∑ w : ↥P.weylGroup, ↑((TauCeti.weylSign P b) w) • AddMonoidAlgebra.single (w • lam - ∑ i ∈ TauCeti.inversionsFinset P b w⁻¹, P.root i) 1

Demazure's formula on a basis element: D_{w₀}(e^λ) is Weyl's quotient. For a reduced word ω of the longest element w₀ and a weight λ,

Δ · D_{w₀}(e^λ) = ∑_{w ∈ W} sgn(w) e^{w λ - (ρ - w ρ)},

the alternating sum over the dot orbit w ⬝ λ = w(λ + ρ) - ρ.