The weights of an integrable module are stable under the root reflections

Let L be a finite-dimensional Lie algebra with non-degenerate Killing form over an algebraically closed field of characteristic zero, let H be a Cartan subalgebra and let α be a root. A module M is integrable along α when every vector of M lies in a finitely generated subspace stable under the sl₂ triple of α, that is when Ado.locallyFiniteSubmodule K M (t.toLieSubalgebra K) = ⊤ for such a triple t. This file proves that the weights of an integrable module are stable under the reflection s_α.

M is not assumed finite-dimensional, and that is the point. For a finite-dimensional module TauCeti/Algebra/Lie/Weights/WeylInvariance.lean already proves the stronger statement that the reflections preserve the weight multiplicities. But the modules Layer 4 of the highest weight roadmap has to bound are the irreducible highest weight modules L(λ), whose finite-dimensionality is the thing to be proved; what is available for them beforehand is integrability (TauCeti/Algebra/Lie/HighestWeight/Integrable.lean). Reflection stability of the weight support, together with the weight cone λ - Q⁺, is what confines those weights to a finite set.

The argument

Fix a weight χ of M, a nonzero vector v of M_χ, and a finitely generated subspace N containing v and stable under the sl₂ triple of α. The subspace

W = ⨆ k : ℤ, (M_{k α + χ} ⊓ N)

is a finite-dimensional module over that triple: the raising and lowering vectors move M_{k α + χ} to M_{(k ± 1) α + χ} and preserve N, while W ≤ N is finite-dimensional because N is. So the rank-one theory applies to W, in two ways.

• The Cartan element α^∨ acts diagonalizably on a finite-dimensional module over an sl₂ triple (Ado.iSup_eigenspace_toEnd_eq_top), with integer eigenvalues (Ado.exists_int_of_hasEigenvalue). Diagonalizable endomorphisms are semisimple (Ado.isSemisimple_of_iSup_eigenspace_eq_top), so the generalized eigenvectors lying in W are honest eigenvectors, and χ (α^∨) = m is an integer.
• Its eigenspaces at opposite eigenvalues have equal dimension (Ado.finrank_eigenspace_toEnd_neg). The eigenvalue m is attained, by v, so -m is attained too.

An eigenvector for -m inside W has to lie in the summand M_{-m α + χ} ⊓ N, because α^∨ acts on the summand M_{k α + χ} ⊓ N by 2 k + m and these scalars are distinct (Ado.biSup_inf_eigenspace_eq_self). That summand is therefore nonzero, and -m α + χ = χ - χ(α^∨) α is the reflection of χ.

Main results

• Ado.exists_int_apply_coroot_of_genWeightSpace_ne_bot: a weight of a module integrable along α takes an integer value on the coroot α^∨, so the reflection statement below needs no integrality hypothesis.
• Ado.genWeightSpace_sub_apply_coroot_smul_ne_bot: the weights of a module integrable along α are stable under the reflection s_α, and Ado.genWeightSpace_sub_apply_coroot_smul_eq_bot_iff records the resulting equivalence, the reflection being an involution.

References

This is the weight-stability half 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, §21.2.
• V. G. Kac, Infinite Dimensional Lie Algebras, 3rd ed., §3.6.

Reflection stability of the weights of an integrable module

theorem Ado.exists_int_apply_coroot_of_genWeightSpace_ne_bot {K : Type u} {L : Type v} [Field K] [CharZero K] [IsAlgClosed K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] {M : Type w} [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] {α : LieModule.Weight K (↥H) L} {χ : ↥H → K} {h e f : L} (hα : α.IsNonZero) (t : IsSl2Triple h e f) (he : e ∈ LieAlgebra.rootSpace H ⇑α) (hf : f ∈ LieAlgebra.rootSpace H (-⇑α)) (hlf : locallyFiniteSubmodule K M ↑(IsSl2Triple.toLieSubalgebra K t) = ⊤) (hχ : LieModule.genWeightSpace M χ ≠ ⊥) : ∃ (m : ℤ), χ (LieAlgebra.IsKilling.coroot α) = ↑m

A weight of an integrable module is integral on the coroot. If a module M is integrable along a nonzero root α, in the sense that every vector lies in a finitely generated subspace stable under an sl₂ triple (h, e, f) of α, then every weight χ of M takes an integer value on the coroot α^∨.

This is the rank-one integrality statement for a module that is not assumed finite-dimensional: the string of χ truncated to a stable finitely generated subspace is a finite-dimensional module over the triple, and Ado.exists_int_of_hasEigenvalue applies to it. For a finite-dimensional module Ado.exists_int_apply_coroot says the same with no integrability hypothesis.

theorem Ado.genWeightSpace_sub_apply_coroot_smul_ne_bot {K : Type u} {L : Type v} [Field K] [CharZero K] [IsAlgClosed K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] {M : Type w} [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] {α : LieModule.Weight K (↥H) L} {χ : ↥H → K} {h e f : L} (hα : α.IsNonZero) (t : IsSl2Triple h e f) (he : e ∈ LieAlgebra.rootSpace H ⇑α) (hf : f ∈ LieAlgebra.rootSpace H (-⇑α)) (hlf : locallyFiniteSubmodule K M ↑(IsSl2Triple.toLieSubalgebra K t) = ⊤) (hχ : LieModule.genWeightSpace M χ ≠ ⊥) : LieModule.genWeightSpace M (χ - χ (LieAlgebra.IsKilling.coroot α) • ⇑α) ≠ ⊥

The weights of an integrable module are stable under the root reflections. Let α be a nonzero root with sl₂ triple (h, e, f), and let M be a module integrable along α: every vector of M lies in a finitely generated subspace stable under the triple. Then the reflection s_α χ = χ - χ(α^∨) α of a weight of M is again a weight of M.

M is not assumed finite-dimensional. For a finite-dimensional module Ado.finrank_weightSpace_sub_apply_coroot_smul gives the stronger conclusion that the reflection preserves the multiplicity.

theorem Ado.genWeightSpace_sub_apply_coroot_smul_eq_bot_iff {K : Type u} {L : Type v} [Field K] [CharZero K] [IsAlgClosed K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] {M : Type w} [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] {α : LieModule.Weight K (↥H) L} {χ : ↥H → K} {h e f : L} (hα : α.IsNonZero) (t : IsSl2Triple h e f) (he : e ∈ LieAlgebra.rootSpace H ⇑α) (hf : f ∈ LieAlgebra.rootSpace H (-⇑α)) (hlf : locallyFiniteSubmodule K M ↑(IsSl2Triple.toLieSubalgebra K t) = ⊤) : LieModule.genWeightSpace M (χ - χ (LieAlgebra.IsKilling.coroot α) • ⇑α) = ⊥ ↔ LieModule.genWeightSpace M χ = ⊥

The weights of an integrable module are exactly the reflections of its weights. With the hypotheses of Ado.genWeightSpace_sub_apply_coroot_smul_ne_bot, a form χ on the Cartan subalgebra is a weight of M exactly when its reflection s_α χ is: the reflection is an involution, so the forward implication applies in both directions.