Chains of roots and weights

Given roots α and β of a Lie algebra, together with elements x in the α-root space and y in the β-root space, it follows from the Leibniz identity that ⁅x, y⁆ is either zero or belongs to the α + β-root space. Iterating this operation leads to the study of families of roots of the form k • α + β. Such a family is known as the α-chain through β (or sometimes, the α-string through β) and the study of the sum of the corresponding root spaces is an important technique.

More generally if α is a root and χ is a weight of a representation, it is useful to study the α-chain through χ.

We provide basic definitions and results to support α-chain techniques in this file.

Main definitions / results

• LieModule.exists₂_weightSpace_smul_add_eq_bot: given weights χ₁, χ₂ if χ₁ ≠ 0, we can find p < 0 and q > 0 such that the weight spaces p • χ₁ + χ₂ and q • χ₁ + χ₂ are both trivial.
• LieModule.weightSpaceChain: given weights χ₁, χ₂ together with integers p and q, this is the sum of the weight spaces k • χ₁ + χ₂ for p < k < q.
• LieModule.trace_toEndomorphism_weightSpaceChain_eq_zero: given a root α relative to a Cartan subalgebra H, there is a natural ideal (rootSpaceProductNegSelf α).range in H. This lemma states that this ideal acts by trace-zero endomorphisms on the sum of root spaces of any α-chain, provided the weight spaces at the endpoints are both trivial.
• LieModule.exists_forall_mem_rootSpaceProductNegSelf_smul_add_eq_zero: given a (potential) root α relative to a Cartan subalgebra H, if we restrict to the ideal (rootSpaceProductNegSelf α).range of H, we may find an integral linear combination between α and any weight χ of a representation.

theorem LieModule.eventually_weightSpace_smul_add_eq_bot {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (M : Type u_3) [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [LieAlgebra.IsNilpotent R L] (χ₁ : L → R) (χ₂ : L → R) [NoZeroSMulDivisors ℤ R] [NoZeroSMulDivisors R M] [IsNoetherian R M] (hχ₁ : χ₁ ≠ 0) : ∀ᶠ (k : ℕ) in Filter.atTop, LieModule.weightSpace M (k • χ₁ + χ₂) = ⊥

theorem LieModule.exists_weightSpace_smul_add_eq_bot {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (M : Type u_3) [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [LieAlgebra.IsNilpotent R L] (χ₁ : L → R) (χ₂ : L → R) [NoZeroSMulDivisors ℤ R] [NoZeroSMulDivisors R M] [IsNoetherian R M] (hχ₁ : χ₁ ≠ 0) : ∃ k > 0, LieModule.weightSpace M (k • χ₁ + χ₂) = ⊥

theorem LieModule.exists₂_weightSpace_smul_add_eq_bot {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (M : Type u_3) [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [LieAlgebra.IsNilpotent R L] (χ₁ : L → R) (χ₂ : L → R) [NoZeroSMulDivisors ℤ R] [NoZeroSMulDivisors R M] [IsNoetherian R M] (hχ₁ : χ₁ ≠ 0) : ∃ p < 0, ∃ q > 0, LieModule.weightSpace M (p • χ₁ + χ₂) = ⊥ ∧ LieModule.weightSpace M (q • χ₁ + χ₂) = ⊥

def LieModule.weightSpaceChain {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (M : Type u_3) [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [LieAlgebra.IsNilpotent R L] (χ₁ : L → R) (χ₂ : L → R) (p : ℤ) (q : ℤ) : LieSubmodule R L M

Given two (potential) weights χ₁ and χ₂ together with integers p and q, it is often useful to study the sum of weight spaces associated to the family of weights k • χ₁ + χ₂ for p < k < q.

Equations

• LieModule.weightSpaceChain M χ₁ χ₂ p q = ⨆ k ∈ Set.Ioo p q, LieModule.weightSpace M (k • χ₁ + χ₂)

theorem LieModule.weightSpaceChain_def {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (M : Type u_3) [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [LieAlgebra.IsNilpotent R L] (χ₁ : L → R) (χ₂ : L → R) (p : ℤ) (q : ℤ) : LieModule.weightSpaceChain M χ₁ χ₂ p q = ⨆ k ∈ Set.Ioo p q, LieModule.weightSpace M (k • χ₁ + χ₂)

theorem LieModule.weightSpaceChain_def' {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (M : Type u_3) [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [LieAlgebra.IsNilpotent R L] (χ₁ : L → R) (χ₂ : L → R) (p : ℤ) (q : ℤ) : LieModule.weightSpaceChain M χ₁ χ₂ p q = ⨆ k ∈ Finset.Ioo p q, LieModule.weightSpace M (k • χ₁ + χ₂)

@[simp]

theorem LieModule.weightSpaceChain_neg {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (M : Type u_3) [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [LieAlgebra.IsNilpotent R L] (χ₁ : L → R) (χ₂ : L → R) (p : ℤ) (q : ℤ) : LieModule.weightSpaceChain M (-χ₁) χ₂ (-q) (-p) = LieModule.weightSpaceChain M χ₁ χ₂ p q

theorem LieModule.weightSpace_le_weightSpaceChain {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (M : Type u_3) [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [LieAlgebra.IsNilpotent R L] (χ₁ : L → R) (χ₂ : L → R) (p : ℤ) (q : ℤ) {k : ℤ} (hk : k ∈ Set.Ioo p q) : LieModule.weightSpace M (k • χ₁ + χ₂) ≤ LieModule.weightSpaceChain M χ₁ χ₂ p q

theorem LieModule.lie_mem_weightSpaceChain_of_weightSpace_eq_bot_right {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (M : Type u_3) [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {H : LieSubalgebra R L} (α : ↥H → R) (χ : ↥H → R) (p : ℤ) (q : ℤ) [LieAlgebra.IsNilpotent R ↥H] (hq : LieModule.weightSpace M (q • α + χ) = ⊥) {x : L} (hx : x ∈ LieAlgebra.rootSpace H α) {y : M} (hy : y ∈ LieModule.weightSpaceChain M α χ p q) : ⁅x, y⁆ ∈ LieModule.weightSpaceChain M α χ p q

theorem LieModule.lie_mem_weightSpaceChain_of_weightSpace_eq_bot_left {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (M : Type u_3) [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {H : LieSubalgebra R L} (α : ↥H → R) (χ : ↥H → R) (p : ℤ) (q : ℤ) [LieAlgebra.IsNilpotent R ↥H] (hp : LieModule.weightSpace M (p • α + χ) = ⊥) {x : L} (hx : x ∈ LieAlgebra.rootSpace H (-α)) {y : M} (hy : y ∈ LieModule.weightSpaceChain M α χ p q) : ⁅x, y⁆ ∈ LieModule.weightSpaceChain M α χ p q

theorem LieModule.trace_toEndomorphism_weightSpaceChain_eq_zero {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (M : Type u_3) [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {H : LieSubalgebra R L} (α : ↥H → R) (χ : ↥H → R) (p : ℤ) (q : ℤ) [LieSubalgebra.IsCartanSubalgebra H] [IsNoetherian R L] (hp : LieModule.weightSpace M (p • α + χ) = ⊥) (hq : LieModule.weightSpace M (q • α + χ) = ⊥) {x : ↥H} (hx : x ∈ LieModuleHom.range (LieAlgebra.rootSpaceProductNegSelf α)) : (LinearMap.trace R ↥↑(LieModule.weightSpaceChain M α χ p q)) ((LieModule.toEndomorphism R ↥H ↥↑(LieModule.weightSpaceChain M α χ p q)) x) = 0

theorem LieModule.exists_forall_mem_rootSpaceProductNegSelf_smul_add_eq_zero {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (M : Type u_3) [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {H : LieSubalgebra R L} (α : ↥H → R) (χ : ↥H → R) [LieSubalgebra.IsCartanSubalgebra H] [IsNoetherian R L] [IsDomain R] [IsPrincipalIdealRing R] [CharZero R] [NoZeroSMulDivisors R M] [IsNoetherian R M] (hα : α ≠ 0) (hχ : LieModule.weightSpace M χ ≠ ⊥) : ∃ (a : ℤ) (b : ℤ), 0 < b ∧ ∀ x ∈ LieModuleHom.range (LieAlgebra.rootSpaceProductNegSelf α), (a • α + b • χ) x = 0

Given a (potential) root α relative to a Cartan subalgebra H, if we restrict to the ideal I = (rootSpaceProductNegSelf α).range of H (informally, I = ⁅H(α), H(-α)⁆), we may find an integral linear combination between α and any weight χ of a representation.

This is Proposition 4.4 from [carter2005] and is a key step in the proof that the roots of a semisimple Lie algebra form a root system. It shows that the restriction of α to I vanishes iff the restriction of every root to I vanishes (which cannot happen in a semisimple Lie algebra).