Alternating 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 alternating for the dot action when its coefficients transform by the sign character,

[e^{w ⬝ x}] f = sgn(w) · [e^x] f.

Both universal elements of the Weyl character formula are alternating: the Weyl denominator Δ = ∏_{α>0}(1 - e^{-α}) (TauCeti.coeff_weylDenominator_dotAction) and the Weyl numerator N(λ) = ∑_{w} sgn(w) e^{w ⬝ λ} of any weight. This file proves that the numerators exhaust them: an alternating element is the sign-symmetrization of its coefficients on a fundamental domain, so that ℤ[M]'s alternating elements are freely spanned by the numerators. That is the step by which the Weyl character formula is concluded: the product ch L(λ) · Δ is alternating, being a product of a Weyl-invariant and an alternating element, and the formula is then the identification of which combination of numerators it is.

The Weyl denominator identity Δ = N(0) (TauCeti.weylDenominator_eq_weylNumerator_zero) is that identification carried out for Δ itself, and is the case λ = 0 of the character formula.

The fundamental domain

The dot action w ⬝ x = w(x + ρ) - ρ has its walls at ⟨x, αᵢ^∨⟩ = -1, so its open chamber is TauCeti.openDotDominantChamber, the weights whose ρ-shift is strictly dominant, which for a general coefficient ring may be strictly larger than the closed dominant chamber. Two facts about it drive everything here. The dot action is free on it, so a numerator N(μ) with μ in the chamber has coefficient 1 at μ and 0 at every other point of the chamber. And every weight is carried into the closed shifted chamber by some Weyl-group element, whose boundary is a union of walls, where an alternating element vanishes because an odd element fixes the point. Together these say an alternating element is determined by its restriction to the open dot chamber (TauCeti.IsDotAlternating.eq_of_coeff_openDotDominantChamber_eq), which is the mechanism behind every result below.

Main definitions

• TauCeti.IsDotAlternating: the coefficients of f transform by the sign character under the dot action. TauCeti.isDotAlternating_iff is the preferred way to introduce it and TauCeti.IsDotAlternating.coeff_dotAction the preferred way to eliminate it, so that the definition itself need not be unfolded.
• TauCeti.dotAlternatingSubmodule: the alternating elements as a ℤ-submodule of ℤ[M].
• TauCeti.weylNumeratorBasis: its basis of Weyl numerators, indexed by the open dot chamber, whose coordinates are read off by TauCeti.weylNumeratorBasis_repr_apply.

Main results

• TauCeti.isDotAlternating_weylNumerator and TauCeti.isDotAlternating_weylDenominator: the Weyl numerator of any weight, and the Weyl denominator, are alternating.
• TauCeti.IsDotAlternating.eq_of_coeff_openDotDominantChamber_eq: an alternating element is determined by its coefficients on the open chamber of the dot action.
• TauCeti.IsDotAlternating.eq_sum_weylNumerator: an alternating element is the sum of the Weyl numerators of the points of the open dot chamber in its support, weighted by its coefficients there, and TauCeti.eq_zero_of_sum_smul_weylNumerator_eq_zero: those weights are unique. Together they are the spanning and independence halves of TauCeti.weylNumeratorBasis.
• TauCeti.IsDotAlternating.eq_weylNumerator: an alternating element whose only nonvanishing coefficient on the open dot chamber is a 1 at λ is N(λ), the form in which the Weyl character formula consumes all of this.

References

This is the "concluding by Weyl alternation" 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.

def TauCeti.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] (b : P.Base) [IsDomain R] [Invertible 2] [P.IsCrystallographic] [P.IsReduced] (f : AddMonoidAlgebra ℤ M) : Prop

An element of the integral group algebra of the weight space is alternating for the dot action when its coefficients transform by the sign character of the Weyl group, [e^{w ⬝ x}] f = sgn(w) · [e^x] f.

The dot action w ⬝ x = w(x + ρ) - ρ is used rather than the linear one because that is the normalization in which the Weyl denominator ∏_{α>0}(1 - e^{-α}) is alternating: the linear action sends it to sgn(w) e^{w(ρ) - ρ} times itself.

Equations

• TauCeti.IsDotAlternating P b f = ∀ (w : ↥P.weylGroup) (x : M), f.coeff (TauCeti.dotAction P b w x) = ↑((TauCeti.weylSign P b) w) * f.coeff x

theorem TauCeti.isDotAlternating_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 ι] [CharZero R] (b : P.Base) [IsDomain R] [Invertible 2] [P.IsCrystallographic] [P.IsReduced] (f : AddMonoidAlgebra ℤ M) : IsDotAlternating P b f ↔ ∀ (w : ↥P.weylGroup) (x : M), f.coeff (dotAction P b w x) = ↑((weylSign P b) w) * f.coeff x

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

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

theorem TauCeti.isDotAlternating_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) [IsDomain R] [Invertible 2] [P.IsCrystallographic] [P.IsReduced] : IsDotAlternating P b 0

The zero element is alternating.

theorem TauCeti.isDotAlternating_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) [IsDomain R] [Invertible 2] [P.IsCrystallographic] [P.IsReduced] : IsDotAlternating P b (weylDenominator P b)

The Weyl denominator is alternating. This is TauCeti.coeff_weylDenominator_dotAction, packaged as the predicate.

theorem TauCeti.isDotAlternating_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) [IsDomain R] [Invertible 2] [P.IsCrystallographic] [P.IsReduced] [Fintype ↥P.weylGroup] (lam : M) : IsDotAlternating P b (weylNumerator P b lam)

The Weyl numerator of any weight is alternating. Reindexing the defining sum by v ↦ w⁻¹v matches the term at w ⬝ x with the term at x, at the cost of the sign of w.

theorem TauCeti.IsDotAlternating.coeff_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] [Invertible 2] [P.IsCrystallographic] [P.IsReduced] {f : AddMonoidAlgebra ℤ M} (hf : IsDotAlternating P b f) (w : ↥P.weylGroup) (x : M) : f.coeff (dotAction P b w x) = ↑((weylSign P b) w) * f.coeff x

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

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

A sum of alternating elements is alternating.

theorem TauCeti.IsDotAlternating.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} [Finite ι] [CharZero R] {b : P.Base} [IsDomain R] [Invertible 2] [P.IsCrystallographic] [P.IsReduced] {f : AddMonoidAlgebra ℤ M} (hf : IsDotAlternating P b f) : IsDotAlternating P b (-f)

The negative of an alternating element is alternating.

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

A difference of alternating elements is alternating.

theorem TauCeti.IsDotAlternating.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} [IsDomain R] [Invertible 2] [P.IsCrystallographic] [P.IsReduced] {f : AddMonoidAlgebra ℤ M} (hf : IsDotAlternating P b f) (c : ℤ) : IsDotAlternating P b (c • f)

An integer multiple of an alternating element is alternating.

theorem TauCeti.IsDotAlternating.coeff_eq_zero_of_dotAction_eq_self {ι : 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] [Invertible 2] [P.IsCrystallographic] [P.IsReduced] {f : AddMonoidAlgebra ℤ M} (hf : IsDotAlternating P b f) {w : ↥P.weylGroup} {x : M} (hw : (weylSign P b) w = -1) (hx : dotAction P b w x = x) : f.coeff x = 0

A coefficient of an alternating element at a weight fixed by an odd Weyl-group element vanishes: the alternating identity turns such a fixed point into c = -c.

theorem TauCeti.IsDotAlternating.coeff_eq_zero_of_coroot'_eq_neg_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} [Finite ι] [CharZero R] {b : P.Base} [IsDomain R] [Invertible 2] [P.IsCrystallographic] [P.IsReduced] {f : AddMonoidAlgebra ℤ M} (hf : IsDotAlternating P b f) {i : ι} (hi : i ∈ b.support) {x : M} (hx : (P.coroot' i) x = -1) : f.coeff x = 0

A coefficient of an alternating element on a wall of the dot action vanishes. The wall of the simple reflection sᵢ is the affine hyperplane ⟨x, αᵢ^∨⟩ = -1, and a simple reflection is odd.

theorem TauCeti.isDotAlternating_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} [Finite ι] [CharZero R] {b : P.Base} [IsDomain R] [Invertible 2] [P.IsCrystallographic] [P.IsReduced] {α : Type u_1} {s : Finset α} {g : α → AddMonoidAlgebra ℤ M} (hg : ∀ a ∈ s, IsDotAlternating P b (g a)) : IsDotAlternating P b (∑ a ∈ s, g a)

A finite sum of alternating elements is alternating.

def TauCeti.dotAlternatingSubmodule {ι : 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] [Invertible 2] [P.IsCrystallographic] [P.IsReduced] : Submodule ℤ (AddMonoidAlgebra ℤ M)

The alternating elements of the integral group algebra ℤ[M], as a ℤ-submodule. The closure properties are TauCeti.isDotAlternating_zero, TauCeti.IsDotAlternating.add and TauCeti.IsDotAlternating.zsmul; TauCeti.weylNumeratorBasis is its basis of Weyl numerators.

Equations

• TauCeti.dotAlternatingSubmodule P b = { carrier := {f : AddMonoidAlgebra ℤ M | TauCeti.IsDotAlternating P b f}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

@[simp]

theorem TauCeti.mem_dotAlternatingSubmodule {ι : 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] [Invertible 2] [P.IsCrystallographic] [P.IsReduced] {f : AddMonoidAlgebra ℤ M} : f ∈ dotAlternatingSubmodule P b ↔ IsDotAlternating P b f

Membership in TauCeti.dotAlternatingSubmodule is being alternating.

The open chamber of the dot action as a fundamental domain

Everything below reads an alternating element off its coefficients on TauCeti.openDotDominantChamber. The linearly ordered hypotheses already supply IsDomain R through IsStrictOrderedRing.isDomain, so it is not repeated.

@[simp]

theorem TauCeti.coeff_weylNumerator_eq_zero_of_mem_openDotDominantChamber {ι : 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) [Invertible 2] [P.IsCrystallographic] [P.IsReduced] [LinearOrder R] [IsStrictOrderedRing R] [P.flip.IsReduced] [Fintype ↥P.weylGroup] {lam nu : M} (hlam : lam ∈ openDotDominantChamber P b) (hnu : nu ∈ openDotDominantChamber P b) (hne : lam ≠ nu) : (weylNumerator P b lam).coeff nu = 0

The numerator of a weight of the open dot chamber vanishes at every other weight of that chamber: the chamber meets each dot orbit at most once.

theorem TauCeti.IsDotAlternating.coeff_eq_zero_of_forall_mem_openDotDominantChamber {ι : 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} [Invertible 2] [P.IsCrystallographic] [P.IsReduced] [LinearOrder R] [IsStrictOrderedRing R] {f : AddMonoidAlgebra ℤ M} [P.IsRootSystem] (hf : IsDotAlternating P b f) (h : ∀ y ∈ openDotDominantChamber P b, f.coeff y = 0) (x : M) : f.coeff x = 0

An alternating element vanishing on the open chamber of the dot action vanishes identically.

Every weight is carried by some Weyl-group element to one whose ρ-shift is dominant. If that shift is strictly dominant the hypothesis applies; otherwise the weight lies on a wall, where an alternating element vanishes. Either way the coefficient there vanishes, and it differs from the original coefficient by a sign.

theorem TauCeti.IsDotAlternating.eq_of_coeff_openDotDominantChamber_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} [Invertible 2] [P.IsCrystallographic] [P.IsReduced] [LinearOrder R] [IsStrictOrderedRing R] {f g : AddMonoidAlgebra ℤ M} [P.IsRootSystem] (hf : IsDotAlternating P b f) (hg : IsDotAlternating P b g) (h : ∀ x ∈ openDotDominantChamber P b, f.coeff x = g.coeff x) : f = g

An alternating element is determined by its coefficients on the open chamber of the dot action.

theorem TauCeti.IsDotAlternating.eq_sum_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} [Invertible 2] [P.IsCrystallographic] [P.IsReduced] [LinearOrder R] [IsStrictOrderedRing R] {f : AddMonoidAlgebra ℤ M} [P.flip.IsReduced] [P.IsRootSystem] [Fintype ↥P.weylGroup] (hf : IsDotAlternating P b f) : f = ∑ mu ∈ f.coeff.support with mu ∈ openDotDominantChamber P b, f.coeff mu • weylNumerator P b mu

An alternating element is the combination of the Weyl numerators of the weights of the open dot chamber in its support, taken with its own coefficients there as multipliers.

This is the spanning half of TauCeti.weylNumeratorBasis; with TauCeti.eq_zero_of_sum_smul_weylNumerator_eq_zero, which says those coefficients are uniquely determined, it exhibits the numerators N(μ) for μ in the open dot chamber as a basis of the alternating elements of ℤ[M].

theorem TauCeti.eq_zero_of_sum_smul_weylNumerator_eq_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} [Invertible 2] [P.IsCrystallographic] [P.IsReduced] [LinearOrder R] [IsStrictOrderedRing R] [P.flip.IsReduced] [Fintype ↥P.weylGroup] {s : Finset M} {c : M → ℤ} (hs : ∀ mu ∈ s, mu ∈ openDotDominantChamber P b) (h : ∑ mu ∈ s, c mu • weylNumerator P b mu = 0) {nu : M} (hnu : nu ∈ s) : c nu = 0

The Weyl numerators of the weights of the open dot chamber are linearly independent over ℤ: a vanishing combination has vanishing multipliers, since the coefficient of the combination at ν is exactly the multiplier of N(ν).

noncomputable def TauCeti.weylNumeratorBasis {ι : 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) [Invertible 2] [P.IsCrystallographic] [P.IsReduced] [LinearOrder R] [IsStrictOrderedRing R] [P.flip.IsReduced] [P.IsRootSystem] [Fintype ↥P.weylGroup] : Module.Basis ↑(openDotDominantChamber P b) ℤ ↥(dotAlternatingSubmodule P b)

The Weyl numerators of the weights of the open dot chamber, as a basis of the alternating elements of ℤ[M].

The two halves are TauCeti.IsDotAlternating.eq_sum_weylNumerator, which spans, and TauCeti.eq_zero_of_sum_smul_weylNumerator_eq_zero, which is the independence; those are what Module.Basis.mk consumes here, and TauCeti.weylNumeratorBasis_repr_apply reads the resulting coordinates back as the coefficients of the element on the chamber.

Equations

• TauCeti.weylNumeratorBasis P b = Module.Basis.mk ⋯ ⋯

@[simp]

theorem TauCeti.coe_weylNumeratorBasis {ι : 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) [Invertible 2] [P.IsCrystallographic] [P.IsReduced] [LinearOrder R] [IsStrictOrderedRing R] [P.flip.IsReduced] [P.IsRootSystem] [Fintype ↥P.weylGroup] (mu : ↑(openDotDominantChamber P b)) : ↑((weylNumeratorBasis P b) mu) = weylNumerator P b ↑mu

The basis vector of TauCeti.weylNumeratorBasis at a weight of the open dot chamber is the Weyl numerator of that weight.

@[simp]

theorem TauCeti.weylNumeratorBasis_repr_apply {ι : 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) [Invertible 2] [P.IsCrystallographic] [P.IsReduced] [LinearOrder R] [IsStrictOrderedRing R] [P.flip.IsReduced] [P.IsRootSystem] [Fintype ↥P.weylGroup] (f : ↥(dotAlternatingSubmodule P b)) (mu : ↑(openDotDominantChamber P b)) : ((weylNumeratorBasis P b).repr f) mu = (↑f).coeff ↑mu

The coordinates of an alternating element in the basis of Weyl numerators are its coefficients on the open dot chamber.

theorem TauCeti.IsDotAlternating.eq_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} [Invertible 2] [P.IsCrystallographic] [P.IsReduced] [LinearOrder R] [IsStrictOrderedRing R] {f : AddMonoidAlgebra ℤ M} [P.flip.IsReduced] [P.IsRootSystem] [Fintype ↥P.weylGroup] (hf : IsDotAlternating P b f) {lam : M} (hlam : lam ∈ openDotDominantChamber P b) (hcoeff : f.coeff lam = 1) (hsupp : ∀ x ∈ openDotDominantChamber P b, f.coeff x ≠ 0 → x = lam) : f = weylNumerator P b lam

An alternating element whose only nonvanishing coefficient on the open dot chamber is a 1 at λ is the Weyl numerator of λ.

This is the form in which the Weyl denominator identity (TauCeti.weylDenominator_eq_weylNumerator_zero) is proved, and the form the Weyl character formula is meant to be concluded in: for an alternating element the hypotheses are two coefficient computations on the open dot chamber, and nothing else about it is needed.