Weyl orbit sums and the expansion of an invariant element

Let P be a root pairing with weight space M and a finite Weyl group. The orbit sum of a weight x is the element m_x = ∑_{y ∈ W x} e^y of the integral group algebra ℤ[M], each distinct weight of the Weyl orbit of x occurring once, with no stabilizer multiplicity. Orbit sums are the simplest Weyl-invariant elements, and this file shows that they are enough: a Weyl-invariant element of ℤ[M] whose support lies below a weight lam and is integral on the simple coroots is the combination

f = ∑_{mu} f(mu) · m_mu,

the sum running over the dominant integral weights mu below lam, which form a finite set. This is the orbit-sum expansion of a formal character: applied to the character of the irreducible module L(lam) it gives ch L(lam) = m_lam + ∑_{mu < lam} c_mu m_mu, unitriangular with respect to the dominance order. That specialization is TauCeti.formalCharacter_eq_orbitSum_add_lower in TauCeti/Algebra/Lie/HighestWeight/OrbitSum.lean; nothing here needs a Lie algebra.

Dominance is the order-free condition that every simple coroot takes a natural value, so the results apply over any characteristic-zero domain, in particular over the algebraically closed field of a Lie algebra, which carries no ordering.

The argument

The expansion compares coefficients at a weight y. Every term f(mu) · m_mu with y in the orbit of mu contributes f(mu) = f(y), by invariance. If f(y) ≠ 0, the support of f is a set of weights below lam, integral on the simple coroots and stable under the simple reflections, so y has a dominant Weyl translate inside it (TauCeti.exists_weylGroup_smul_dominant_of_forall_reflection_mem_of_sub_mem_posRootCone); and a Weyl orbit contains at most one dominant integral weight (TauCeti.weylGroup_smul_eq_self_of_dominantIntegral). So exactly one term contributes, and it contributes f(y).

Main definitions

• RootPairing.weylWeightOrbit: the finite set of the distinct weights in the Weyl orbit of a weight.
• RootPairing.weightOrbitSum: the orbit sum m_x = ∑_{y ∈ W x} e^y.

The finite set of the dominant integral weights below lam over which the expansion runs is RootPairing.dominantWeightsBelow, from TauCeti/LinearAlgebra/RootSystem/DominantCone.lean.

Main results

• RootPairing.coeff_weightOrbitSum: the coefficients of m_x are 1 on the orbit of x and 0 elsewhere, and RootPairing.isWeylInvariant_weightOrbitSum: m_x is Weyl-invariant.
• RootPairing.isWeylInvariant_sum_single_smul: the sum ∑_w e^{w x} of all Weyl translates of x, counted with repetition, is Weyl-invariant.
• TauCeti.IsWeylInvariant.eq_sum_coeff_smul_weightOrbitSum: a Weyl-invariant element supported below lam on integral weights is the combination of the orbit sums of the dominant integral weights below lam, with its own coefficients.

References

• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, GTM 9, §13.2 and §22.5.
• N. Bourbaki, Lie Groups and Lie Algebras, Chapters 7-9, Ch. VIII, §7.

Weyl orbits and orbit sums

noncomputable def RootPairing.weylWeightOrbit {ι : 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 ↥P.weylGroup] (x : M) : Finset M

The Weyl orbit of a weight x, as the finite set of its distinct Weyl translates w • x. As a set it is Mathlib's MulAction.orbit (RootPairing.coe_weylWeightOrbit).

noncomputable def RootPairing.weightOrbitSum {ι : 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 ↥P.weylGroup] (x : M) : AddMonoidAlgebra ℤ M

The orbit sum m_x = ∑_{y ∈ W x} e^y of a weight x in the integral group algebra ℤ[M]: every distinct weight of the Weyl orbit of x occurs once, with coefficient 1.

@[simp]

theorem RootPairing.mem_weylWeightOrbit {ι : 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 ↥P.weylGroup] {x y : M} : y ∈ P.weylWeightOrbit x ↔ ∃ (w : ↥P.weylGroup), w • x = y

A weight lies in the Weyl orbit of x exactly when it is a Weyl translate of x.

@[simp]

theorem RootPairing.coe_weylWeightOrbit {ι : 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 ↥P.weylGroup] (x : M) : ↑(P.weylWeightOrbit x) = MulAction.orbit (↥P.weylGroup) x

The Weyl orbit of x, as a set, is the orbit of x under the action of the Weyl group.

theorem RootPairing.smul_mem_weylWeightOrbit {ι : 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 ↥P.weylGroup] (w : ↥P.weylGroup) (x : M) : w • x ∈ P.weylWeightOrbit x

Every Weyl translate of x lies in the Weyl orbit of x.

theorem RootPairing.self_mem_weylWeightOrbit {ι : 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 ↥P.weylGroup] (x : M) : x ∈ P.weylWeightOrbit x

A weight lies in its own Weyl orbit.

@[simp]

theorem RootPairing.weylWeightOrbit_smul {ι : 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 ↥P.weylGroup] (w : ↥P.weylGroup) (x : M) : P.weylWeightOrbit (w • x) = P.weylWeightOrbit x

Weyl-conjugate weights have the same Weyl orbit.

theorem RootPairing.weylWeightOrbit_eq_of_mem {ι : 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 ↥P.weylGroup] {x y : M} (h : y ∈ P.weylWeightOrbit x) : P.weylWeightOrbit y = P.weylWeightOrbit x

The Weyl orbit of a weight is the Weyl orbit of any of its members.

theorem RootPairing.smul_mem_weylWeightOrbit_iff {ι : 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 ↥P.weylGroup] {x y : M} (w : ↥P.weylGroup) : w • y ∈ P.weylWeightOrbit x ↔ y ∈ P.weylWeightOrbit x

A Weyl translate of y lies in the Weyl orbit of x exactly when y does.

@[simp]

theorem RootPairing.weylWeightOrbit_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 ↥P.weylGroup] : P.weylWeightOrbit 0 = {0}

The Weyl orbit of the zero weight is {0}.

@[simp]

theorem RootPairing.coeff_weightOrbitSum {ι : 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 ↥P.weylGroup] [DecidableEq M] (x y : M) : (P.weightOrbitSum x).coeff y = if y ∈ P.weylWeightOrbit x then 1 else 0

The coefficients of an orbit sum: m_x has coefficient 1 at every weight of the Weyl orbit of x and 0 at every other weight.

theorem RootPairing.coeff_weightOrbitSum_of_mem {ι : 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 ↥P.weylGroup] {x y : M} (h : y ∈ P.weylWeightOrbit x) : (P.weightOrbitSum x).coeff y = 1

The orbit sum of x has coefficient 1 on the Weyl orbit of x.

theorem RootPairing.coeff_weightOrbitSum_of_notMem {ι : 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 ↥P.weylGroup] {x y : M} (h : y ∉ P.weylWeightOrbit x) : (P.weightOrbitSum x).coeff y = 0

The orbit sum of x has coefficient 0 off the Weyl orbit of x.

@[simp]

theorem RootPairing.weightOrbitSum_smul {ι : 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 ↥P.weylGroup] (w : ↥P.weylGroup) (x : M) : P.weightOrbitSum (w • x) = P.weightOrbitSum x

Weyl-conjugate weights have the same orbit sum.

@[simp]

theorem RootPairing.weightOrbitSum_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 ↥P.weylGroup] : P.weightOrbitSum 0 = 1

The orbit sum of the zero weight is the unit e^0 = 1 of ℤ[M].

theorem RootPairing.isWeylInvariant_weightOrbitSum {ι : 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 ↥P.weylGroup] (x : M) : TauCeti.IsWeylInvariant P (P.weightOrbitSum x)

An orbit sum is Weyl-invariant.

theorem RootPairing.isWeylInvariant_sum_single_smul {ι : 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} [Fintype ↥P.weylGroup] (x : M) : TauCeti.IsWeylInvariant P (∑ w : ↥P.weylGroup, AddMonoidAlgebra.single (w • x) 1)

The sum of all Weyl translates of a weight is Weyl-invariant. In ∑_w e^{w x} each weight of the Weyl orbit of x occurs once for every Weyl group element sending x to it, and translating by a Weyl group element permutes those elements.

The orbit-sum expansion

theorem TauCeti.IsWeylInvariant.eq_sum_coeff_smul_weightOrbitSum {ι : 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] [IsDomain R] [P.IsRootSystem] [P.IsCrystallographic] {b : P.Base} [P.IsReduced] [Finite ↥P.weylGroup] {f : AddMonoidAlgebra ℤ M} {lam : M} (hf : IsWeylInvariant P f) (hcone : ∀ (y : M), f.coeff y ≠ 0 → lam - y ∈ posRootCone P b) (hint : ∀ (y : M), f.coeff y ≠ 0 → ∀ i ∈ b.support, ∃ (z : ℤ), (P.coroot' i) y = ↑z) : f = ∑ mu ∈ P.dominantWeightsBelow b lam, f.coeff mu • P.weightOrbitSum mu

The orbit-sum expansion of a Weyl-invariant element. Let f ∈ ℤ[M] be Weyl-invariant, with every weight in its support lying below lam and integral on the simple coroots. Then f is the combination of the orbit sums of the dominant integral weights below lam, each weighted by its own coefficient in f:

f = ∑_{mu ∈ dominantWeightsBelow lam} f(mu) · m_mu.

Each Weyl orbit in the support of f contains exactly one dominant integral weight, which lies below lam, so the orbit sums of these weights account for every coefficient of f once.