The Weyl denominator moved by a Weyl-group element

A Weyl-group element w acts on the integral group algebra ℤ[M] of the weight space through its linear action on the exponents. It sends the Weyl denominator Δ = ∏_{α > 0} (1 - e^{-α}) to w Δ = ∏_{α > 0} (1 - e^{-w α}), and this file computes that product exactly, factor by factor:

w Δ = (-1)^{ℓ} e^{∑_{β > 0, w⁻¹ β < 0} β} Δ,

where ℓ is the number of positive roots β with w⁻¹ β < 0. The factors of the positive roots that w keeps positive are permuted among the factors of Δ. Each positive root α that w inverts gives β = -w α, a positive root that w⁻¹ inverts, and its factor is inverted: 1 - e^{β} = -e^{β} (1 - e^{-β}). Every inverted factor contributes one sign and one shift by its root, and neither the crystallographic nor the reduced hypothesis is used.

With the Weyl vector ρ, the shift is ρ - w ρ (TauCeti.smul_weylVector_sub_weylVector) and the sign is sgn(w), so w Δ = sgn(w) e^{ρ - w ρ} Δ. Multiplied by e^{w λ} this says

e^{w λ} Δ = sgn(w) e^{w ⬝ λ} (w Δ),

the denominator-free form of e^{w λ} / ∏_{α > 0} (1 - e^{-w α}) = sgn(w) e^{w ⬝ λ} / Δ. Summed over W, the right-hand sides add up to the Weyl numerator over Δ, which is how the fixed-point form ∑_{w ∈ W} e^{w λ} / ∏_{α > 0} (1 - e^{-w α}) of the Weyl character formula is compared with its normalized form ∑_{w ∈ W} sgn(w) e^{w(λ + ρ) - ρ} / ∏_{α > 0} (1 - e^{-α}).

Main results

• RootPairing.mapDomain_smul_weylDenominator_eq_prod: w Δ = ∏_{α > 0} (1 - e^{-w α}).
• TauCeti.mapDomain_smul_weylDenominator: w Δ = (-1)^{ℓ} e^{∑_{β > 0, w⁻¹ β < 0} β} Δ.
• TauCeti.coeff_weylDenominator_of_mem_dominantChamber: over a linearly ordered coefficient ring, the constant term 1 is the only coefficient of Δ on the dominant chamber, since a dominant weight in the negative cone is 0.
• TauCeti.mapDomain_smul_weylDenominator_eq_zsmul: w Δ = sgn(w) e^{ρ - w ρ} Δ.
• TauCeti.coeff_weylDenominator_dotAction: the coefficient function of Δ transforms by the sign character under the dot action of the whole Weyl group.
• TauCeti.single_smul_mul_weylDenominator: e^{w λ} Δ = sgn(w) e^{w ⬝ λ} (w Δ).
• RootPairing.map_mapDomain_smul_weylDenominator_ne_zero: f (w Δ) ≠ 0 when f Δ ≠ 0, for any ring homomorphism f out of ℤ[M].

References

• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, GTM 9, Ch. VI, §24.1.
• N. Bourbaki, Lie Groups and Lie Algebras, Chapters 4–6, Ch. VI, §3.

theorem RootPairing.mapDomain_smul_weylDenominator_eq_prod {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [Finite ι] [CharZero R] (b : P.Base) (w : ↥P.weylGroup) : AddMonoidAlgebra.mapDomain (fun (x : M) => w • x) (TauCeti.weylDenominator P b) = ∏ i ∈ TauCeti.posRootsFinset P b, (1 - AddMonoidAlgebra.single (-(w • P.root i)) 1)

A Weyl-group element moves the Weyl denominator factor by factor: w Δ = ∏_{α > 0} (1 - e^{-w α}).

theorem TauCeti.mapDomain_smul_weylDenominator {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [Finite ι] [CharZero R] (b : P.Base) (w : ↥P.weylGroup) : AddMonoidAlgebra.mapDomain (fun (x : M) => w • x) (weylDenominator P b) = AddMonoidAlgebra.single (∑ i ∈ inversionsFinset P b w⁻¹, P.root i) ((-1) ^ (inversionsFinset P b w⁻¹).card) * weylDenominator P b

A Weyl-group element sends the Weyl denominator to a signed monomial multiple of itself: w Δ = (-1)^{ℓ} e^{∑_{β > 0, w⁻¹ β < 0} β} Δ, where ℓ is the number of positive roots β with w⁻¹ β < 0.

theorem TauCeti.coeff_weylDenominator_of_mem_dominantChamber {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [Finite ι] [CharZero R] (b : P.Base) [LinearOrder R] [IsStrictOrderedRing R] [P.IsCrystallographic] [P.IsReduced] [P.flip.IsReduced] {y : M} (hy : y ∈ P.dominantChamber b) : (weylDenominator P b).coeff y = (AddMonoidAlgebra.coeff 1) y

On the dominant chamber the Weyl denominator has only its constant term 1. A weight carrying a nonzero coefficient of Δ is minus a member of the positive root cone, and a dominant such weight is 0 (TauCeti.eq_zero_of_mem_dominantChamber_of_neg_mem_posRootCone).

theorem TauCeti.mapDomain_smul_weylDenominator_eq_zsmul {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [Finite ι] [CharZero R] (b : P.Base) (w : ↥P.weylGroup) [IsDomain R] [P.IsCrystallographic] [P.IsReduced] [Invertible 2] : AddMonoidAlgebra.mapDomain (fun (x : M) => w • x) (weylDenominator P b) = ↑((weylSign P b) w) • (AddMonoidAlgebra.single (weylVector P b - w • weylVector P b) 1 * weylDenominator P b)

A Weyl-group element multiplies the Weyl denominator by its sign and a shift by the Weyl vector: w Δ = sgn(w) e^{ρ - w ρ} Δ.

theorem TauCeti.single_smul_mul_weylDenominator {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [Finite ι] [CharZero R] (b : P.Base) (w : ↥P.weylGroup) [IsDomain R] [P.IsCrystallographic] [P.IsReduced] [Invertible 2] (lam : M) : AddMonoidAlgebra.single (w • lam) 1 * weylDenominator P b = ↑((weylSign P b) w) • (AddMonoidAlgebra.single (dotAction P b w lam) 1 * AddMonoidAlgebra.mapDomain (fun (x : M) => w • x) (weylDenominator P b))

The fixed-point term against the normalized term: e^{w λ} Δ = sgn(w) e^{w ⬝ λ} (w Δ). This is the denominator-free form of e^{w λ} / ∏_{α > 0} (1 - e^{-w α}) = sgn(w) e^{w(λ + ρ) - ρ} / ∏_{α > 0} (1 - e^{-α}).

@[simp]

theorem TauCeti.coeff_weylDenominator_dotAction {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [Finite ι] [CharZero R] (b : P.Base) [IsDomain R] [P.IsCrystallographic] [P.IsReduced] [Invertible 2] (w : ↥P.weylGroup) (x : M) : (weylDenominator P b).coeff (dotAction P b w x) = ↑((weylSign P b) w) * (weylDenominator P b).coeff x

The coefficients of the Weyl denominator transform by the sign character under the dot action of the whole Weyl group: [e^{w ⬝ x}] Δ = sgn(w) [e^x] Δ.

theorem RootPairing.map_mapDomain_smul_weylDenominator_ne_zero {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [Finite ι] [CharZero R] (b : P.Base) {S : Type y} [Semiring S] (f : AddMonoidAlgebra ℤ M →+* S) (hf : f (TauCeti.weylDenominator P b) ≠ 0) (w : ↥P.weylGroup) : f (AddMonoidAlgebra.mapDomain (fun (x : M) => w • x) (TauCeti.weylDenominator P b)) ≠ 0

The moved Weyl denominator does not vanish where the Weyl denominator does not: for a ring homomorphism f into a semiring, if f Δ ≠ 0 then f (w Δ) ≠ 0, since w Δ is Δ times a signed exponential, a unit of ℤ[M].