The weight cone below a weight is finite once it is stable under the simple reflections

Fix a base b of a finite crystallographic root system P and a weight lam. The set of weights lying below lam, that is those mu with lam - mu in the positive root cone Q⁺, is infinite: it is a whole translated cone. This file proves that two further conditions cut it down to a finite set.

• Dominance. Only finitely many mu below lam take a natural value on every simple coroot (Ado.finite_setOf_dominant_sub_mem_posRootCone). This is the classical statement that a dominant weight below lam is bounded, and it comes straight from positive definiteness of the symmetrized Cartan matrix, in the form given in TauCeti/LinearAlgebra/RootSystem/FiniteType/Bounded.lean.
• Stability under the simple reflections. A set of weights below lam on which every simple coroot takes integer values and which is carried into itself by every simple reflection is finite (Ado.finite_of_forall_reflection_mem_of_sub_mem_posRootCone). Stability replaces dominance: a non-dominant member is raised by a simple reflection to another member strictly closer to lam, so it is a Weyl translate of a dominant member, and the Weyl group is finite.

The second statement is the shape the representation theory needs. The weights of an irreducible highest weight module of dominant integral highest weight lam lie in lam - Q⁺, take integer values on the simple coroots and are stable under the simple reflections, none of which presupposes that the module is finite-dimensional; the theorem below turns those three facts into finiteness of the weight support.

The raising step is itself worth naming, because a Weyl translate carries more information than a cardinality: under the same three hypotheses every member has a Weyl-group element taking it to a dominant member of the set (Ado.exists_weylGroup_smul_dominant_of_forall_reflection_mem_of_sub_mem_posRootCone). Finiteness is the corollary obtained by forgetting which translate was used.

Main results

• Ado.finite_setOf_dominant_sub_mem_posRootCone: only finitely many dominant weights lie below a given weight.
• Ado.exists_weylGroup_smul_dominant_of_forall_reflection_mem_of_sub_mem_posRootCone: a member of a set of weights below lam, integral on the simple coroots and stable under the simple reflections, has a dominant Weyl translate in the set.
• Ado.finite_of_forall_reflection_mem_of_sub_mem_posRootCone: a set of weights below lam, integral on the simple coroots and stable under the simple reflections, is finite.
• Ado.eq_zero_of_mem_posRootCone_of_forall_coroot'_nonpos: the only antidominant member of the positive root cone is zero, the case lam = 0 of the first statement applied to all the natural multiples of a member at once.

The argument

Writing lam - mu = ∑ j, c j • αⱼ with natural coefficients c j, the value of mu on the simple coroot αᵢ^∨ is lam (αᵢ^∨) - ∑ j, c j * ⟨αⱼ, αᵢ^∨⟩. Dominance therefore says that the natural vector c solves the Cartan inequality of the transposed Cartan matrix, whose solution set is finite; the right-hand side of the inequality is manufactured from one member of the set, which is why the argument begins by disposing of the empty case.

For the other two, if mu is a member on which αᵢ^∨ takes a negative value, then sᵢ mu = mu - ⟨mu, αᵢ^∨⟩ αᵢ is again a member and lam - sᵢ mu has strictly smaller height: the simple roots are linearly independent, so the coefficient vectors of the two differences agree except at i, where the coefficient drops by -⟨mu, αᵢ^∨⟩ ≥ 1. Induction on that height therefore writes every member as a Weyl translate of a dominant member, which is the second statement; finiteness follows because both the dominant members and the Weyl group are finite.

References

This is the root-system content of the "weight-cone bound" milestone of Layer 4, "the classification of finite-dimensional irreducibles", of TauCetiRoadmap/RepresentationTheory/LieHighestWeight/README.md.

• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, GTM 9, §13.2 and §21.2.

theorem Ado.finite_setOf_dominant_sub_mem_posRootCone {ι : 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) (lam : M) : {mu : M | lam - mu ∈ posRootCone P b ∧ ∀ i ∈ b.support, ∃ (n : ℕ), (P.coroot' i) mu = ↑n}.Finite

Only finitely many dominant weights lie below a given weight. For a base b of a finite crystallographic root system and a weight lam, only finitely many mu satisfy both that lam - mu is a nonnegative integer combination of the simple roots and that every simple coroot takes a natural value on mu.

The two hypotheses pull in opposite directions: the first writes lam - mu as ∑ j, c j • αⱼ with c j natural, and the second bounds the resulting Cartan expression ∑ j, c j ⟨αⱼ, αᵢ^∨⟩ above. Positive definiteness of the symmetrized Cartan matrix (Ado.finite_setOf_forall_sum_mul_le) leaves only finitely many such c.

theorem Ado.exists_weylGroup_smul_dominant_of_forall_reflection_mem_of_sub_mem_posRootCone {ι : 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} [CharZero R] (b : P.Base) {lam : M} {S : Set M} (hcone : ∀ mu ∈ S, lam - mu ∈ posRootCone P b) (hint : ∀ mu ∈ S, ∀ i ∈ b.support, ∃ (z : ℤ), (P.coroot' i) mu = ↑z) (hrefl : ∀ mu ∈ S, ∀ i ∈ b.support, (P.reflection i) mu ∈ S) {mu : M} (hmu : mu ∈ S) : ∃ (w : ↥P.weylGroup), w • mu ∈ S ∧ ∀ i ∈ b.support, ∃ (n : ℕ), (P.coroot' i) (w • mu) = ↑n

A member of a reflection-stable set of weights below a weight has a dominant Weyl translate in the set. Let S be a set of weights with lam - mu in the positive root cone for every mu ∈ S, on which every simple coroot takes integer values, and which every simple reflection carries into itself. Then every mu ∈ S has a Weyl-group element w for which w • mu again lies in S and every simple coroot takes a natural value on it.

A member on which some simple coroot is negative is moved by the corresponding reflection strictly closer to lam, so the induction on the height of lam - mu stops exactly at a dominant member; the set of weights admitting such a w is reflection stable, which is what lets the induction run inside it.

Ado.exists_mem_dominantChamber is the same statement for an arbitrary weight, with dominance read as 0 ≤ ⟨mu, αᵢ^∨⟩ and no reference to lam; it needs a [LinearOrder R] on the coefficient ring, which is exactly what the weight space of a Lie algebra over an algebraically closed field does not carry. Here dominance is instead the order-free condition that each ⟨mu, αᵢ^∨⟩ is a natural number, which the hypotheses on S make available, and the cone below lam replaces the maximization argument.

theorem Ado.finite_of_forall_reflection_mem_of_sub_mem_posRootCone {ι : 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) {lam : M} {S : Set M} (hcone : ∀ mu ∈ S, lam - mu ∈ posRootCone P b) (hint : ∀ mu ∈ S, ∀ i ∈ b.support, ∃ (z : ℤ), (P.coroot' i) mu = ↑z) (hrefl : ∀ mu ∈ S, ∀ i ∈ b.support, (P.reflection i) mu ∈ S) : S.Finite

A reflection-stable set of weights below a weight is finite. Let S be a set of weights with lam - mu in the positive root cone for every mu ∈ S, on which every simple coroot takes integer values, and which every simple reflection carries into itself. Then S is finite.

Stability is what replaces dominance in Ado.finite_setOf_dominant_sub_mem_posRootCone: every member is a Weyl translate of a dominant member by Ado.exists_weylGroup_smul_dominant_of_forall_reflection_mem_of_sub_mem_posRootCone, and both the dominant members and the Weyl group are finite.

theorem Ado.eq_zero_of_mem_posRootCone_of_forall_coroot'_nonpos {ι : 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] [P.IsRootSystem] [P.IsCrystallographic] (b : P.Base) [LinearOrder R] [IsStrictOrderedRing R] {nu : M} (hnu : nu ∈ posRootCone P b) (h : ∀ i ∈ b.support, (P.coroot' i) nu ≤ 0) : nu = 0

The only antidominant member of the positive root cone is zero. A nonnegative integer combination nu of the simple roots on which every simple coroot takes a nonpositive value is zero.

The pairings of a member of Q⁺ with the simple coroots are Cartan integers (Ado.exists_intCast_eq_coroot'_of_mem_posRootCone), so nonpositivity makes every natural multiple of -nu a dominant weight below 0. There are only finitely many of those by Ado.finite_setOf_dominant_sub_mem_posRootCone, while the multiples of a nonzero member of Q⁺ are pairwise distinct because their heights are.

This is the statement that separates the dot orbit of 0 from the rest of the negative cone: it is what forces the Weyl denominator to be supported on that orbit alone.