Documentation

TauCeti.LinearAlgebra.RootSystem.Weyl.Denominator.Integral

The dot alternatization and the Weyl denominator identity for a root datum #

Let P be a root datum, a root pairing over ℤ, with a base and weight lattice M, and let ℤ[M] be its integral group algebra, with e^x the basis element at x. In a root datum the Weyl vector ρ need not be a weight (for PGL₂ it is half a root), but for every Weyl-group element w the difference ρ - w ρ = ∑_{β > 0, w⁻¹ β < 0} β is a sum of roots. This file defines the dot alternatization

J(f) = ∑_{w ∈ W} sgn(w) e^{-(ρ - w ρ)} w(f),

a ℤ-linear endomorphism of ℤ[M] (RootPairing.dotAlternatization). On a basis element it is the alternating sum J(e^x) = ∑_w sgn(w) e^{w ⬝ x} over the dot orbit w ⬝ x = w(x + ρ) - ρ, the Weyl numerator of x (compare TauCeti.weylNumerator, which needs ρ to be a weight). Its basic properties are that it is linear over the Weyl-invariant elements, and that it is antisymmetric for the twisted simple reflections, J(e^{-αᵢ} sᵢ(f)) = -J(f).

The main result is the Weyl denominator identity for a root datum:

J(1) = ∑_{w ∈ W} sgn(w) e^{-(ρ - w ρ)} = ∏_{α > 0} (1 - e^{-α}) = Δ.

The version TauCeti.weylDenominator_eq_weylNumerator_zero is stated for a root system over an ordered ring in which 2 is invertible, so that ρ is a weight and the roots span. Neither holds for a general root datum such as that of GLₙ (roots do not span) or PGL₂ (ρ is not a weight). The identity here is the form needed for the integral Demazure operators of TauCeti.LinearAlgebra.RootSystem.Weyl.Demazure.Basic, which live on such root data.

The argument #

Write T_w(f) = e^{-(ρ - w ρ)} w(f), the twisted reindexing TauCeti.twistedWeylReindex. Since ρ - v w ρ = (ρ - v ρ) + v(ρ - w ρ), the T_w compose like the group, T_v T_w = T_{v w}, and so T_v J = sgn(v) J; also T_w Δ = sgn(w) Δ. Hence J(1) - Δ is alternating for the twisted action. Such an element is determined by its coefficients on the dominant chamber: every weight x has a Weyl translate w ⬝ x with 2(w ⬝ x) + 2ρ = w(2x + 2ρ) dominant, and if w ⬝ x is not itself dominant it pairs to -1 with some simple coroot, so the twisted simple reflection fixes it and changes the sign of its coefficient. Only 2ρ, which is always a weight, enters. On the dominant chamber both J(1) and Δ have only the constant term 1: a weight -(ρ - w ρ) is dominant only for w = 1, because 2ρ is strictly dominant (TauCeti.twoWeylVector_mem_openDominantChamber), and the Weyl denominator has only its constant term there (TauCeti.coeff_weylDenominator_of_mem_dominantChamber).

Main definitions #

Main results #

References #

The shift ρ - w ρ and the twisted reindexing T_w #

The dot alternatization #

source
noncomputable def RootPairing.dotAlternatization {ι : 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] :
AddMonoidAlgebra ℤ M →ₗ[ℤ] AddMonoidAlgebra ℤ M

The dot alternatization J(f) = ∑_{w ∈ W} sgn(w) e^{-(ρ - w ρ)} w(f) of the integral group algebra of a root datum, where ρ - w ρ = ∑_{β > 0, w⁻¹ β < 0} β. On a basis element it is the alternating sum J(e^x) = ∑_w sgn(w) e^{w ⬝ x} over the dot orbit w ⬝ x = w(x + ρ) - ρ (RootPairing.dotAlternatization_single).

Instances For
    source
    theorem RootPairing.dotAlternatization_apply {ι : 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] (f : AddMonoidAlgebra ℤ M) :
    (P.dotAlternatization b) f = ∑ w : ↥P.weylGroup, ↑((TauCeti.weylSign P b) w) • (AddMonoidAlgebra.single (-∑ i ∈ TauCeti.inversionsFinset P b w⁻¹, P.root i) 1 * AddMonoidAlgebra.mapDomain (fun (x : M) => w • x) f)

    The defining formula of RootPairing.dotAlternatization.

    source
    theorem RootPairing.dotAlternatization_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] (x : M) :
    (P.dotAlternatization b) (AddMonoidAlgebra.single x 1) = ∑ w : ↥P.weylGroup, ↑((TauCeti.weylSign P b) w) • AddMonoidAlgebra.single (w • x - ∑ i ∈ TauCeti.inversionsFinset P b w⁻¹, P.root i) 1

    The dot alternatization of a basis element e^x is ∑_w sgn(w) e^{w x - (ρ - w ρ)}, the alternating sum over the dot orbit of x.

    source
    theorem RootPairing.dotAlternatization_mul_of_isWeylInvariant {ι : 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] {g : AddMonoidAlgebra ℤ M} (hg : TauCeti.IsWeylInvariant P g) (f : AddMonoidAlgebra ℤ M) :
    (P.dotAlternatization b) (g * f) = g * (P.dotAlternatization b) f

    The dot alternatization is linear over the Weyl-invariant elements: J(g f) = g J(f).

    source
    theorem RootPairing.dotAlternatization_single_neg_root_mul {ι : 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) (AddMonoidAlgebra.single (-P.root i) 1 * (AddMonoidAlgebra.mapDomainRingEquiv ℤ (P.reflection i).toAddEquiv) f) = -(P.dotAlternatization b) f

    The dot alternatization is antisymmetric for a twisted simple reflection: J(e^{-αᵢ} sᵢ(f)) = -J(f).

    source
    @[simp]
    theorem RootPairing.dotAlternatization_one {ι : 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] :
    (P.dotAlternatization b) 1 = TauCeti.weylDenominator P b

    The Weyl denominator identity for a root datum:

    ∑_{w ∈ W} sgn(w) e^{-(ρ - w ρ)} = ∏_{α > 0} (1 - e^{-α}),

    where ρ - w ρ = ∑_{β > 0, w⁻¹ β < 0} β. Unlike TauCeti.weylDenominator_eq_weylNumerator_zero, this needs neither ρ to be a weight nor the roots to span.