The Weyl dimension formula for a root pairing

The Weyl character formula ch · Δ = N(λ) is an identity in the group algebra ℤ[M] of the weight space of a root pairing, between a formal character ch, the Weyl denominator Δ = ∏_{α>0}(1 - e^{-α}) and the Weyl numerator N(λ) = ∑_w sgn(w) e^{w ⬝ λ}. The Weyl dimension formula extracts from it the sum of the coefficients of ch, the dimension of the module whose character it is:

dim · ∏_{α>0} ⟨ρ, α^∨⟩ = ∏_{α>0} ⟨λ + ρ, α^∨⟩.

This file proves the extraction with no Lie algebra in sight, for any f ∈ ℤ[M] with f · Δ = N(λ), given an invariant form on the root pairing. The character formula for the zero weight, g · Δ = N(0), is taken as a second input rather than assumed to be the denominator identity Δ = N(0): that identity is proved here only over ordered coefficient rings (TauCeti.weylDenominator_eq_weylNumerator_zero), whereas a Lie algebra over an algebraically closed field supplies g = ch L(0) from the character formula itself. The conclusion is then (∑ f) · ∏ ⟨ρ, α^∨⟩ = (∑ g) · ∏ ⟨λ + ρ, α^∨⟩, and ∑ g = 1 in the application.

The argument

Apply the exponential specialization θ_μ = AddMonoidAlgebra.expAlgHom (B μ) along the invariant form, e^ν ↦ e^{⟨μ, ν⟩ X}, which is a ring homomorphism ℤ[M] → R⟦X⟧.

• θ_μ(Δ) = ∏_{α>0} (1 - e^{-⟨μ, α⟩ X}) is a product of |Φ⁺| series with zero constant coefficient and linear coefficient ⟨μ, α⟩, so any multiple h · θ_μ(Δ) has coefficient h(0) · ∏_{α>0} ⟨μ, α⟩ in degree |Φ⁺| (TauCeti.coeff_card_mul_expAlgHom_weylDenominator).
• e^{⟨μ, ρ⟩ X} θ_μ(N(λ)) = ∑_w sgn(w) e^{⟨μ, w(λ+ρ)⟩ X} is symmetric in μ and λ + ρ, by the Weyl invariance of the form and the reindexing w ↦ w⁻¹ (TauCeti.rescale_mul_expAlgHom_weylNumerator_eq).

With μ = ρ the second point turns θ_ρ(f) θ_ρ(Δ) = θ_ρ(N(λ)) into e^{⟨ρ, ρ⟩ X} θ_ρ(f) θ_ρ(Δ) = e^{⟨λ+ρ, ρ⟩ X} θ_{λ+ρ}(N(0)) = e^{⟨λ+ρ, ρ⟩ X} θ_{λ+ρ}(g) θ_{λ+ρ}(Δ), and the first point reads off the coefficients of degree |Φ⁺| on both sides: (∑ f) ∏_{α>0} ⟨ρ, α⟩ = (∑ g) ∏_{α>0} ⟨λ+ρ, α⟩. The normalisation 2 ⟨x, α⟩ = ⟨x, α^∨⟩ ⟨α, α⟩ of the form against the coroots (RootPairing.InvariantForm.two_mul_apply_root) converts this to the coroot form.

Main results

• TauCeti.sum_coeff_mul_prod_form_weylVector_root_eq: the dimension formula in terms of the invariant form, (∑ f) ∏_{α>0} ⟨ρ, α⟩ = (∑ g) ∏_{α>0} ⟨λ+ρ, α⟩.
• TauCeti.sum_coeff_mul_prod_coroot'_weylVector_eq: the Weyl dimension formula in its coroot form, (∑ f) ∏_{α>0} ⟨ρ, α^∨⟩ = (∑ g) ∏_{α>0} ⟨λ+ρ, α^∨⟩.

References

• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, GTM 9, §24.3, where the dimension formula is obtained from the character formula by the homomorphism e^ν ↦ e^{⟨ν, ρ⟩ X} and the symmetry of ∑_w sgn(w) e^{⟨μ, w ν⟩ X} in μ and ν.
• W. Fulton and J. Harris, Representation Theory: A First Course, GTM 129, §24.2.

The exponential specialization of the Weyl denominator

theorem TauCeti.expAlgHom_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) [Algebra ℚ R] (φ : M →+ R) : (AddMonoidAlgebra.expAlgHom φ) (weylDenominator P b) = ∏ i ∈ posRootsFinset P b, (1 - (PowerSeries.rescale (-φ (P.root i))) (PowerSeries.exp R))

The exponential specialization of the Weyl denominator along an additive map φ is ∏_{α>0} (1 - e^{-φ(α) X}).

theorem TauCeti.coeff_card_mul_expAlgHom_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) [Algebra ℚ R] (φ : M →+ R) (h : PowerSeries R) : (PowerSeries.coeff (posRootsFinset P b).card) (h * (AddMonoidAlgebra.expAlgHom φ) (weylDenominator P b)) = PowerSeries.constantCoeff h * ∏ i ∈ posRootsFinset P b, φ (P.root i)

The lowest coefficient of a multiple of the specialized Weyl denominator. Each factor 1 - e^{-φ(α) X} has zero constant coefficient and linear coefficient φ(α), so h · θ_φ(Δ) has coefficient h(0) ∏_{α>0} φ(α) in degree |Φ⁺|.

The exponential specialization of the Weyl numerator

theorem TauCeti.rescale_mul_expAlgHom_weylNumerator {ι : 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) [Algebra ℚ R] [IsDomain R] [Invertible 2] [P.IsCrystallographic] [P.IsReduced] [Fintype ↥P.weylGroup] (φ : M →+ R) (lam : M) : (PowerSeries.rescale (φ (weylVector P b))) (PowerSeries.exp R) * (AddMonoidAlgebra.expAlgHom φ) (weylNumerator P b lam) = ∑ w : ↥P.weylGroup, ↑↑((weylSign P b) w) * (PowerSeries.rescale (φ (w • (lam + weylVector P b)))) (PowerSeries.exp R)

The exponential specialization of the Weyl numerator, after multiplication by e^{φ(ρ) X}, is the alternating sum ∑_w sgn(w) e^{φ(w(λ+ρ)) X} over the linear orbit of λ + ρ: the ρ-shift of the dot action is absorbed by the exponential.

theorem TauCeti.sum_weylSign_mul_rescale_form_smul_comm {ι : 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) [Algebra ℚ R] [IsDomain R] [P.IsCrystallographic] [P.IsReduced] [Fintype ↥P.weylGroup] (B : P.InvariantForm) (mu nu : M) : ∑ w : ↥P.weylGroup, ↑↑((weylSign P b) w) * (PowerSeries.rescale ((B.form mu) (w • nu))) (PowerSeries.exp R) = ∑ w : ↥P.weylGroup, ↑↑((weylSign P b) w) * (PowerSeries.rescale ((B.form nu) (w • mu))) (PowerSeries.exp R)

The symmetry of the alternating exponential sum. For an invariant form B, the sum ∑_w sgn(w) e^{⟨μ, w ν⟩ X} is symmetric in μ and ν: Weyl invariance moves w across the form, where it becomes w⁻¹, and inversion permutes the Weyl group without changing signs.

theorem TauCeti.rescale_mul_expAlgHom_weylNumerator_eq {ι : 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) [Algebra ℚ R] [IsDomain R] [Invertible 2] [P.IsCrystallographic] [P.IsReduced] [Fintype ↥P.weylGroup] (B : P.InvariantForm) (mu lam : M) : (PowerSeries.rescale ((B.form mu) (weylVector P b))) (PowerSeries.exp R) * (AddMonoidAlgebra.expAlgHom (B.form mu).toAddMonoidHom) (weylNumerator P b lam) = (PowerSeries.rescale ((B.form (lam + weylVector P b)) (weylVector P b))) (PowerSeries.exp R) * (AddMonoidAlgebra.expAlgHom (B.form (lam + weylVector P b)).toAddMonoidHom) (weylNumerator P b (mu - weylVector P b))

The exponential specialization of the Weyl numerator is symmetric in μ and λ + ρ: e^{⟨μ, ρ⟩ X} θ_μ(N(λ)) = e^{⟨λ+ρ, ρ⟩ X} θ_{λ+ρ}(N(μ - ρ)), both sides being the alternating sum ∑_w sgn(w) e^{⟨μ, w(λ+ρ)⟩ X}.

The dimension formula

theorem TauCeti.sum_coeff_mul_prod_form_weylVector_root_eq {ι : 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) [Algebra ℚ R] [IsDomain R] [Invertible 2] [P.IsCrystallographic] [P.IsReduced] [Fintype ↥P.weylGroup] (B : P.InvariantForm) {f g : AddMonoidAlgebra ℤ M} {lam : M} (hf : f * weylDenominator P b = weylNumerator P b lam) (hg : g * weylDenominator P b = weylNumerator P b 0) : ↑(f.coeff.sum fun (x : M) (n : ℤ) => n) * ∏ i ∈ posRootsFinset P b, (B.form (weylVector P b)) (P.root i) = ↑(g.coeff.sum fun (x : M) (n : ℤ) => n) * ∏ i ∈ posRootsFinset P b, (B.form (lam + weylVector P b)) (P.root i)

The Weyl dimension formula, in terms of an invariant form. If f · Δ = N(λ) and g · Δ = N(0) in ℤ[M], then the sums of the coefficients of f and g satisfy (∑ f) ∏_{α>0} ⟨ρ, α⟩ = (∑ g) ∏_{α>0} ⟨λ+ρ, α⟩.

theorem TauCeti.sum_coeff_mul_prod_coroot'_weylVector_eq {ι : 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) [Algebra ℚ R] [IsDomain R] [Invertible 2] [P.IsCrystallographic] [P.IsReduced] [Fintype ↥P.weylGroup] (B : P.InvariantForm) {f g : AddMonoidAlgebra ℤ M} {lam : M} (hf : f * weylDenominator P b = weylNumerator P b lam) (hg : g * weylDenominator P b = weylNumerator P b 0) : ↑(f.coeff.sum fun (x : M) (n : ℤ) => n) * ∏ i ∈ posRootsFinset P b, (P.coroot' i) (weylVector P b) = ↑(g.coeff.sum fun (x : M) (n : ℤ) => n) * ∏ i ∈ posRootsFinset P b, (P.coroot' i) (lam + weylVector P b)

The Weyl dimension formula. If f · Δ = N(λ) and g · Δ = N(0) in ℤ[M], then the sums of the coefficients of f and g satisfy

(∑ f) ∏_{α>0} ⟨ρ, α^∨⟩ = (∑ g) ∏_{α>0} ⟨λ+ρ, α^∨⟩.

For the formal character f = ch L(λ) of an irreducible module and g = ch L(0) = 1 this is dim L(λ) ∏_{α>0} ⟨ρ, α^∨⟩ = ∏_{α>0} ⟨λ+ρ, α^∨⟩, the division-free form of dim L(λ) = ∏_{α>0} ⟨λ+ρ, α^∨⟩ / ⟨ρ, α^∨⟩. An invariant form on the root pairing is needed for the proof, though it does not appear in the statement.