Weyl-invariant elements of the group algebra of a weight space

An element f of the integral group algebra ℤ[M] of the weight space of a root pairing is Weyl-invariant when its coefficients are constant on the orbits of the linear action of the Weyl group, [e^{w x}] f = [e^x] f. The formal character of a finite-dimensional module over a semisimple Lie algebra is the motivating example.

The invariants are closed under the ring operations, and the point of this file is how they interact with the alternating elements of TauCeti/LinearAlgebra/RootSystem/Weyl/Alternating.lean, which transform by the sign character under the shifted dot action w ⬝ x = w(x + ρ) - ρ: multiplying an alternating element by an invariant one leaves it alternating (TauCeti.IsWeylInvariant.mul_isDotAlternating). That is the step by which the Weyl character formula gets started, since the product ch M · Δ of a formal character with the Weyl denominator is exactly such a product, and TauCeti.IsDotAlternating.eq_weylNumerator can then identify it as a Weyl numerator from its coefficients on the open dot chamber alone.

The two actions

The mismatch between the linear and the dot action is only a translation, and that is what makes the multiplication statement work. Writing σ_w for the reindexing of ℤ[M] along x ↦ w x, an invariant element is a fixed point of every σ_w, whereas an alternating element satisfies e^{wρ - ρ} · σ_w g = sgn(w) · g. Since σ_w is a ring homomorphism, the twisted operator h ↦ e^{wρ - ρ} · σ_w h is linear over the invariants, and multiplying the first identity into the second is the whole proof.

Main definitions

• TauCeti.IsWeylInvariant: the coefficients of f are constant on the orbits of the linear Weyl action. TauCeti.isWeylInvariant_iff is the preferred way to introduce it and TauCeti.IsWeylInvariant.coeff_smul the preferred way to eliminate it, so that the definition itself need not be unfolded.
• TauCeti.weylInvariantSubring: the invariant elements as a subring of ℤ[M].

Main results

• TauCeti.IsWeylInvariant.mul_isDotAlternating: an invariant element times an alternating element is alternating.
• TauCeti.isWeylInvariant_zero, TauCeti.isWeylInvariant_one, TauCeti.IsWeylInvariant.add, TauCeti.IsWeylInvariant.neg, TauCeti.IsWeylInvariant.sub, TauCeti.IsWeylInvariant.zsmul, TauCeti.IsWeylInvariant.mul and TauCeti.isWeylInvariant_sum: the invariants are closed under the ring operations of ℤ[M].

References

This is the "a product of a Weyl-invariant and an alternating element" step of the Weyl character formula route fixed by Layer 6 ("the Weyl character, dimension, and Kostant formulas") of TauCetiRoadmap/RepresentationTheory/LieHighestWeight/README.md. As with TauCeti.weylNumerator and TauCeti.weylDenominator, nothing here needs a Lie algebra, so it is stated for an abstract root pairing and the Lie-algebra statement is a specialization rather than a rebuild.

• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, GTM 9, Ch. VI, §24.2.
• J.-P. Serre, Complex Semisimple Lie Algebras, Ch. VII, §7.

Reindexing the group algebra along the linear Weyl action

Weyl invariance

def TauCeti.IsWeylInvariant {ι : 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) (f : AddMonoidAlgebra ℤ M) : Prop

An element of the integral group algebra of the weight space is Weyl-invariant when its coefficients are constant on the orbits of the linear action of the Weyl group, [e^{w x}] f = [e^x] f.

The linear action is used here, not the dot action w ⬝ x = w(x + ρ) - ρ of TauCeti.IsDotAlternating: it is the linear action that the weight multiplicity function of a finite-dimensional module is invariant under.

Equations

• TauCeti.IsWeylInvariant P f = ∀ (w : ↥P.weylGroup) (x : M), f.coeff (w • x) = f.coeff x

theorem TauCeti.isWeylInvariant_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) (f : AddMonoidAlgebra ℤ M) : IsWeylInvariant P f ↔ ∀ (w : ↥P.weylGroup) (x : M), f.coeff (w • x) = f.coeff x

The defining condition of TauCeti.IsWeylInvariant, as an Iff: this is the preferred way to introduce the predicate, and TauCeti.IsWeylInvariant.coeff_smul the preferred way to eliminate it, so that callers need not unfold the definition.

Not a simp lemma: unfolding the predicate would dissolve IsWeylInvariant out of the goals its own API is stated about.

theorem TauCeti.isWeylInvariant_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) : IsWeylInvariant P 0

The zero element is invariant.

theorem TauCeti.isWeylInvariant_one {ι : 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) : IsWeylInvariant P 1

The unit of ℤ[M] is invariant: it sits at the weight 0, which every Weyl-group element fixes.

theorem TauCeti.IsWeylInvariant.coeff_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} {f : AddMonoidAlgebra ℤ M} (hf : IsWeylInvariant P f) (w : ↥P.weylGroup) (x : M) : f.coeff (w • x) = f.coeff x

The defining identity of an invariant element, as an elimination rule.

theorem TauCeti.IsWeylInvariant.add {ι : 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} {f g : AddMonoidAlgebra ℤ M} (hf : IsWeylInvariant P f) (hg : IsWeylInvariant P g) : IsWeylInvariant P (f + g)

A sum of invariant elements is invariant.

theorem TauCeti.IsWeylInvariant.neg {ι : 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} {f : AddMonoidAlgebra ℤ M} (hf : IsWeylInvariant P f) : IsWeylInvariant P (-f)

The negative of an invariant element is invariant.

theorem TauCeti.IsWeylInvariant.sub {ι : 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} {f g : AddMonoidAlgebra ℤ M} (hf : IsWeylInvariant P f) (hg : IsWeylInvariant P g) : IsWeylInvariant P (f - g)

A difference of invariant elements is invariant.

theorem TauCeti.IsWeylInvariant.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} {f : AddMonoidAlgebra ℤ M} (hf : IsWeylInvariant P f) (c : ℤ) : IsWeylInvariant P (c • f)

An integer multiple of an invariant element is invariant.

theorem TauCeti.IsWeylInvariant.mul {ι : 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} {f g : AddMonoidAlgebra ℤ M} (hf : IsWeylInvariant P f) (hg : IsWeylInvariant P g) : IsWeylInvariant P (f * g)

A product of invariant elements is invariant.

theorem TauCeti.isWeylInvariant_sum {ι : 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} {α : Type u_1} {s : Finset α} {g : α → AddMonoidAlgebra ℤ M} (hg : ∀ a ∈ s, IsWeylInvariant P (g a)) : IsWeylInvariant P (∑ a ∈ s, g a)

A finite sum of invariant elements is invariant.

def TauCeti.weylInvariantSubring {ι : 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) : Subring (AddMonoidAlgebra ℤ M)

The Weyl-invariant elements of the integral group algebra ℤ[M], as a subring. The closure properties are TauCeti.isWeylInvariant_zero, TauCeti.isWeylInvariant_one, TauCeti.IsWeylInvariant.add, TauCeti.IsWeylInvariant.neg and TauCeti.IsWeylInvariant.mul.

Equations

• TauCeti.weylInvariantSubring P = { carrier := {f : AddMonoidAlgebra ℤ M | TauCeti.IsWeylInvariant P f}, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }

@[simp]

theorem TauCeti.mem_weylInvariantSubring {ι : 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} {f : AddMonoidAlgebra ℤ M} : f ∈ weylInvariantSubring P ↔ IsWeylInvariant P f

Membership in TauCeti.weylInvariantSubring is Weyl invariance.

Invariant multiples of alternating elements

theorem TauCeti.IsWeylInvariant.mul_isDotAlternating {ι : 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] [Invertible 2] [P.IsCrystallographic] [P.IsReduced] {b : P.Base} {f g : AddMonoidAlgebra ℤ M} (hf : IsWeylInvariant P f) (hg : IsDotAlternating P b g) : IsDotAlternating P b (f * g)

A Weyl-invariant element times an alternating element is alternating.

This is the mechanism that starts the Weyl character formula: the formal character of a finite-dimensional module is invariant and the Weyl denominator is alternating (TauCeti.isDotAlternating_weylDenominator), so their product is alternating, which is the hypothesis TauCeti.IsDotAlternating.eq_weylNumerator consumes.