Admissible lattices decompose into weight components

Let U_ℤ = kostantForm e h be a Kostant integral form in U(L), acting through ρ on a rational vector space V, and let M ≤ V be a U_ℤ-stable additive subgroup — an admissible lattice once it is also a lattice. A designated Cartan vector h j acts on V by an operator whose eigenvalues on a representation with integral weights are integers, and the question this file answers is whether an element of M has all of its weight components in M. It does, and this is what makes the weight components of an admissible lattice into lattices themselves.

Nothing about M forces this: M is only assumed stable, and the projection onto a weight space is a Lagrange interpolation polynomial in the Cartan operator with rational coefficients, so it does not obviously preserve an integral structure. The point is that the Kostant form contains not just the Cartan vector h j but all of its binomial coefficients (h j choose k), and even all the coefficients (h j - a choose k) of its integer translates (TauCeti.UniversalEnvelopingAlgebra.ringChoose_ι_sub_intCast_mem_kostantForm). Those act on a vector of weight a + i by the ordinary binomial coefficient (i choose k), and Newton's forward-difference formula (TauCeti.exists_forall_sum_mul_choose_eq) writes any prescribed integer values on i = 0, …, N as an integral combination of them. Choosing the values to be the indicator of a single weight produces a genuine projector inside U_ℤ, which is TauCeti.UniversalEnvelopingAlgebra.exists_mem_kostantForm_forall_apply_eq.

A weight of the whole Cartan family is an integer-valued function on the Cartan indices, and two distinct weights differ at some single index, so grouping summands by their value there reduces the simultaneous statement TauCeti.UniversalEnvelopingAlgebra.jointWeightComponent_mem_of_kostantStable to the one-index one. That is Humphreys' Lemma 27.1: an admissible lattice contains every joint weight component of each of its elements, so it is the direct sum of the lattices it cuts out of the weight spaces. For a single Cartan direction the decomposition is packaged as a submodule identity, TauCeti.UniversalEnvelopingAlgebra.iSup_weightComponent_eq together with TauCeti.UniversalEnvelopingAlgebra.iSupIndep_weightComponent.

This is the input the pinned Chevalley--Demazure group scheme of Layer 9 needs before its split maximal torus can be written down, since the torus is exactly what acts by a character on each weight component.

Main declarations

• TauCeti.UniversalEnvelopingAlgebra.exists_mem_kostantForm_forall_apply_eq: prescribed integer scalars on a window of consecutive weights are realized by a single element of the Kostant form.
• TauCeti.UniversalEnvelopingAlgebra.weightComponent_mem_of_kostantStable: every weight component for one Cartan vector of an element of a Kostant-stable subgroup lies in that subgroup.
• TauCeti.UniversalEnvelopingAlgebra.jointWeightComponent_mem_of_kostantStable: the same for the joint weight components of the whole Cartan family.
• TauCeti.UniversalEnvelopingAlgebra.weightComponent: the weight components of a ℤ-submodule.
• TauCeti.UniversalEnvelopingAlgebra.iSup_weightComponent_eq and TauCeti.UniversalEnvelopingAlgebra.iSupIndep_weightComponent: a Kostant-stable ℤ-submodule of a module with integral weights is the direct sum of its weight components.

References

• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, §27.1.
• J. C. Jantzen, Representations of Algebraic Groups, II.1.

Separating weights inside the Kostant form

theorem TauCeti.UniversalEnvelopingAlgebra.exists_mem_kostantForm_forall_apply_eq {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} {V : Type v} [AddCommGroup V] [Module ℚ V] (e : ι → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (j : κ) (a : ℤ) (N : ℕ) (g : ℕ → ℤ) : ∃ u ∈ kostantForm e h, ∀ i ≤ N, ∀ (x : V), (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (h j))) x = ↑(a + ↑i) • x → (ρ u) x = ↑(g i) • x

The Kostant form separates the weights in a window. Given a base weight a, a window length N and prescribed integer values g 0, …, g N, some element of the Kostant integral form acts by the scalar g i on every vector of weight a + i, simultaneously for all i ≤ N.

The element is the integral combination ∑ k ≤ N, c k • (h j - a choose k) supplied by Newton's forward-difference formula; each summand lies in the form because the Cartan binomial coefficients of a designated Cartan vector survive integer translation of their argument.

Weight components of a stable subgroup

theorem TauCeti.UniversalEnvelopingAlgebra.weightComponent_mem_of_kostantStable {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} {V : Type v} [AddCommGroup V] [Module ℚ V] (e : ι → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) {S : Type u_2} [SetLike S V] {M : S} (hM : ∀ u ∈ kostantForm e h, ∀ x ∈ M, (ρ u) x ∈ M) (j : κ) {s : Finset ℤ} {w : ℤ → V} (hw : ∀ m ∈ s, (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (h j))) (w m) = ↑m • w m) (hv : ∑ m ∈ s, w m ∈ M) {m₀ : ℤ} (hm₀ : m₀ ∈ s) : w m₀ ∈ M

A Kostant-stable subgroup contains the weight components of its elements. If a vector of M is written as a finite sum of vectors of pairwise distinct integer weights for the Cartan vector h j, then each of those vectors already lies in M.

This is the integrality statement behind Humphreys' Lemma 27.1: the projector onto a single weight has rational coefficients as a polynomial in the Cartan operator, yet it is realized inside the Kostant integral form.

theorem TauCeti.UniversalEnvelopingAlgebra.jointWeightComponent_mem_of_kostantStable {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} {V : Type v} [AddCommGroup V] [Module ℚ V] (e : ι → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) {S : Type u_2} [SetLike S V] {M : S} (hM : ∀ u ∈ kostantForm e h, ∀ x ∈ M, (ρ u) x ∈ M) {s : Finset (κ → ℤ)} {w : (κ → ℤ) → V} (hw : ∀ l ∈ s, ∀ (j : κ), (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (h j))) (w l) = ↑(l j) • w l) (hv : ∑ l ∈ s, w l ∈ M) {l₀ : κ → ℤ} (hl₀ : l₀ ∈ s) : w l₀ ∈ M

A Kostant-stable subgroup contains the joint weight components of its elements. A weight is an integer-valued function on the designated Cartan vectors, and a vector of M written as a finite sum of simultaneous eigenvectors of pairwise distinct weights has each summand in M.

Two distinct weights differ at some Cartan index, so grouping the summands by their value at that index and applying the one-index statement strips off at least one weight while keeping l₀. The induction is on the set of weights involved, which shrinks strictly at every step.

The direct-sum decomposition

def TauCeti.UniversalEnvelopingAlgebra.weightComponent {L : Type u} [LieRing L] [LieAlgebra ℚ L] {κ : Type u_1} {V : Type v} [AddCommGroup V] [Module ℚ V] (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : Submodule ℤ V) (j : κ) (m : ℤ) : Submodule ℤ V

The m-th weight component of a ℤ-submodule M of V: the part of M lying in the m-eigenspace of the operator by which the Cartan vector h j acts.

Equations

• TauCeti.UniversalEnvelopingAlgebra.weightComponent h ρ M j m = M ⊓ Submodule.restrictScalars ℤ ((ρ ((UniversalEnvelopingAlgebra.ι ℚ) (h j))).eigenspace ↑m)

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.mem_weightComponent_iff {L : Type u} [LieRing L] [LieAlgebra ℚ L] {κ : Type u_1} {V : Type v} [AddCommGroup V] [Module ℚ V] (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) {M : Submodule ℤ V} {j : κ} {m : ℤ} {x : V} : x ∈ weightComponent h ρ M j m ↔ x ∈ M ∧ (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (h j))) x = ↑m • x

Membership in a weight component: an element of M whose weight for the Cartan vector h j is m.

theorem TauCeti.UniversalEnvelopingAlgebra.weightComponent_le {L : Type u} [LieRing L] [LieAlgebra ℚ L] {κ : Type u_1} {V : Type v} [AddCommGroup V] [Module ℚ V] (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : Submodule ℤ V) (j : κ) (m : ℤ) : weightComponent h ρ M j m ≤ M

A weight component of M is contained in M.

theorem TauCeti.UniversalEnvelopingAlgebra.iSup_weightComponent_eq {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} {V : Type v} [AddCommGroup V] [Module ℚ V] (e : ι → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) {M : Submodule ℤ V} (hM : ∀ u ∈ kostantForm e h, ∀ x ∈ M, (ρ u) x ∈ M) (j : κ) (hV : ⨆ (m : ℤ), (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (h j))).eigenspace ↑m = ⊤) : ⨆ (m : ℤ), weightComponent h ρ M j m = M

A Kostant-stable lattice is spanned by its weight components. If the Cartan vector h j acts on V with integral weights, then a ℤ-submodule stable under the Kostant integral form is the sum of the pieces it cuts out of the weight spaces.

theorem TauCeti.UniversalEnvelopingAlgebra.iSupIndep_weightComponent {L : Type u} [LieRing L] [LieAlgebra ℚ L] {κ : Type u_1} {V : Type v} [AddCommGroup V] [Module ℚ V] (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : Submodule ℤ V) (j : κ) : iSupIndep (weightComponent h ρ M j)

The weight components of a ℤ-submodule are independent. They inherit independence from the eigenspaces of the Cartan operator, so the sum in TauCeti.UniversalEnvelopingAlgebra.iSup_weightComponent_eq is direct.