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₂_genWeightSpace_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.genWeightSpaceChain: given weights χ₁, χ₂ together with integers p and q, this is the sum of the weight spaces k • χ₁ + χ₂ for p < k < q.
• LieModule.trace_toEnd_genWeightSpaceChain_eq_zero: given a root α relative to a Cartan subalgebra H, there is a natural ideal corootSpace α 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_corootSpace_smul_add_eq_zero: given a (potential) root α relative to a Cartan subalgebra H, if we restrict to the ideal corootSpace α of H, we may find an integral linear combination between α and any weight χ of a representation.

TODO

It should be possible to unify some of the definitions here such as LieModule.chainBotCoeff, LieModule.chainTopCoeff with corresponding definitions such as RootPairing.chainBotCoeff, RootPairing.chainTopCoeff. This is not quite trivial since:

• The definitions here allow for chains in representations of Lie algebras.
• The proof that the roots of a Lie algebra are a root system currently depends on these results. (This can be resolved by proving the root reflection formula using the approach outlined in Bourbaki Ch. VIII §2.2 Lemma 1 (page 80 of English translation, 88 of English PDF).)

theorem LieModule.eventually_genWeightSpace_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] [LieRing.IsNilpotent L] (χ₁ χ₂ : L → R) [NoZeroSMulDivisors ℤ R] [NoZeroSMulDivisors R M] [IsNoetherian R M] (hχ₁ : χ₁ ≠ 0) : ∀ᶠ (k : ℕ) in Filter.atTop, genWeightSpace M (k • χ₁ + χ₂) = ⊥

theorem LieModule.exists_genWeightSpace_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] [LieRing.IsNilpotent L] (χ₁ χ₂ : L → R) [NoZeroSMulDivisors ℤ R] [NoZeroSMulDivisors R M] [IsNoetherian R M] (hχ₁ : χ₁ ≠ 0) : ∃ k > 0, genWeightSpace M (k • χ₁ + χ₂) = ⊥

theorem LieModule.exists₂_genWeightSpace_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] [LieRing.IsNilpotent L] (χ₁ χ₂ : L → R) [NoZeroSMulDivisors ℤ R] [NoZeroSMulDivisors R M] [IsNoetherian R M] (hχ₁ : χ₁ ≠ 0) : ∃ p < 0, ∃ q > 0, genWeightSpace M (p • χ₁ + χ₂) = ⊥ ∧ genWeightSpace M (q • χ₁ + χ₂) = ⊥

def LieModule.genWeightSpaceChain {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] [LieRing.IsNilpotent L] (χ₁ χ₂ : 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.genWeightSpaceChain M χ₁ χ₂ p q = ⨆ k ∈ Set.Ioo p q, LieModule.genWeightSpace M (k • χ₁ + χ₂)

theorem LieModule.genWeightSpaceChain_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] [LieRing.IsNilpotent L] (χ₁ χ₂ : L → R) (p q : ℤ) : genWeightSpaceChain M χ₁ χ₂ p q = ⨆ k ∈ Set.Ioo p q, genWeightSpace M (k • χ₁ + χ₂)

theorem LieModule.genWeightSpaceChain_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] [LieRing.IsNilpotent L] (χ₁ χ₂ : L → R) (p q : ℤ) : genWeightSpaceChain M χ₁ χ₂ p q = ⨆ k ∈ Finset.Ioo p q, genWeightSpace M (k • χ₁ + χ₂)

@[simp]

theorem LieModule.genWeightSpaceChain_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] [LieRing.IsNilpotent L] (χ₁ χ₂ : L → R) (p q : ℤ) : genWeightSpaceChain M (-χ₁) χ₂ (-q) (-p) = genWeightSpaceChain M χ₁ χ₂ p q

theorem LieModule.genWeightSpace_le_genWeightSpaceChain {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] [LieRing.IsNilpotent L] (χ₁ χ₂ : L → R) (p q : ℤ) {k : ℤ} (hk : k ∈ Set.Ioo p q) : genWeightSpace M (k • χ₁ + χ₂) ≤ genWeightSpaceChain M χ₁ χ₂ p q

theorem LieModule.lie_mem_genWeightSpaceChain_of_genWeightSpace_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) (p q : ℤ) [LieRing.IsNilpotent ↥H] (hq : genWeightSpace M (q • α + χ) = ⊥) {x : L} (hx : x ∈ LieAlgebra.rootSpace H α) {y : M} (hy : y ∈ genWeightSpaceChain M α χ p q) : ⁅x, y⁆ ∈ genWeightSpaceChain M α χ p q

theorem LieModule.lie_mem_genWeightSpaceChain_of_genWeightSpace_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) (p q : ℤ) [LieRing.IsNilpotent ↥H] (hp : genWeightSpace M (p • α + χ) = ⊥) {x : L} (hx : x ∈ LieAlgebra.rootSpace H (-α)) {y : M} (hy : y ∈ genWeightSpaceChain M α χ p q) : ⁅x, y⁆ ∈ genWeightSpaceChain M α χ p q

theorem LieModule.trace_toEnd_genWeightSpaceChain_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) (p q : ℤ) [H.IsCartanSubalgebra] [IsNoetherian R L] (hp : genWeightSpace M (p • α + χ) = ⊥) (hq : genWeightSpace M (q • α + χ) = ⊥) {x : ↥H} (hx : x ∈ LieAlgebra.corootSpace α) : (LinearMap.trace R ↥(genWeightSpaceChain M α χ p q)) ((toEnd R ↥H ↥(genWeightSpaceChain M α χ p q)) x) = 0

theorem LieModule.exists_forall_mem_corootSpace_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.IsCartanSubalgebra] [IsNoetherian R L] [IsDomain R] [IsPrincipalIdealRing R] [CharZero R] [NoZeroSMulDivisors R M] [IsNoetherian R M] (hα : α ≠ 0) (hχ : genWeightSpace M χ ≠ ⊥) : ∃ (a : ℤ) (b : ℤ), 0 < b ∧ ∀ x ∈ LieAlgebra.corootSpace α, (a • α + b • χ) x = 0

Given a (potential) root α relative to a Cartan subalgebra H, if we restrict to the ideal I = corootSpace α 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).

noncomputable def LieModule.chainTopCoeff {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] [LieRing.IsNilpotent L] [NoZeroSMulDivisors ℤ R] [NoZeroSMulDivisors R M] [IsNoetherian R M] (α : L → R) (β : Weight R L M) : ℕ

This is the largest n : ℕ such that i • α + β is a weight for all 0 ≤ i ≤ n.

Equations

• LieModule.chainTopCoeff α β = if hα : α = 0 then 0 else (Nat.find ⋯).pred

noncomputable def LieModule.chainBotCoeff {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] [LieRing.IsNilpotent L] [NoZeroSMulDivisors ℤ R] [NoZeroSMulDivisors R M] [IsNoetherian R M] (α : L → R) (β : Weight R L M) : ℕ

This is the largest n : ℕ such that -i • α + β is a weight for all 0 ≤ i ≤ n.

Equations

• LieModule.chainBotCoeff α β = LieModule.chainTopCoeff (-α) β

@[simp]

theorem LieModule.chainTopCoeff_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] [LieRing.IsNilpotent L] [NoZeroSMulDivisors ℤ R] [NoZeroSMulDivisors R M] [IsNoetherian R M] (α : L → R) (β : Weight R L M) : chainTopCoeff (-α) β = chainBotCoeff α β

@[simp]

theorem LieModule.chainBotCoeff_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] [LieRing.IsNilpotent L] [NoZeroSMulDivisors ℤ R] [NoZeroSMulDivisors R M] [IsNoetherian R M] (α : L → R) (β : Weight R L M) : chainBotCoeff (-α) β = chainTopCoeff α β

@[simp]

theorem LieModule.chainTopCoeff_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] [LieRing.IsNilpotent L] [NoZeroSMulDivisors ℤ R] [NoZeroSMulDivisors R M] [IsNoetherian R M] (β : Weight R L M) : chainTopCoeff 0 β = 0

@[simp]

theorem LieModule.chainBotCoeff_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] [LieRing.IsNilpotent L] [NoZeroSMulDivisors ℤ R] [NoZeroSMulDivisors R M] [IsNoetherian R M] (β : Weight R L M) : chainBotCoeff 0 β = 0

theorem LieModule.chainTopCoeff_add_one {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] [LieRing.IsNilpotent L] [NoZeroSMulDivisors ℤ R] [NoZeroSMulDivisors R M] [IsNoetherian R M] (α : L → R) (β : Weight R L M) (hα : α ≠ 0) : chainTopCoeff α β + 1 = Nat.find ⋯

theorem LieModule.genWeightSpace_chainTopCoeff_add_one_nsmul_add {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] [LieRing.IsNilpotent L] [NoZeroSMulDivisors ℤ R] [NoZeroSMulDivisors R M] [IsNoetherian R M] (α : L → R) (β : Weight R L M) (hα : α ≠ 0) : genWeightSpace M ((chainTopCoeff α β + 1) • α + ⇑β) = ⊥

theorem LieModule.genWeightSpace_chainTopCoeff_add_one_zsmul_add {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] [LieRing.IsNilpotent L] [NoZeroSMulDivisors ℤ R] [NoZeroSMulDivisors R M] [IsNoetherian R M] (α : L → R) (β : Weight R L M) (hα : α ≠ 0) : genWeightSpace M ((↑(chainTopCoeff α β) + 1) • α + ⇑β) = ⊥

theorem LieModule.genWeightSpace_chainBotCoeff_sub_one_zsmul_sub {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] [LieRing.IsNilpotent L] [NoZeroSMulDivisors ℤ R] [NoZeroSMulDivisors R M] [IsNoetherian R M] (α : L → R) (β : Weight R L M) (hα : α ≠ 0) : genWeightSpace M ((-↑(chainBotCoeff α β) - 1) • α + ⇑β) = ⊥

theorem LieModule.genWeightSpace_nsmul_add_ne_bot_of_le {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] [LieRing.IsNilpotent L] [NoZeroSMulDivisors ℤ R] [NoZeroSMulDivisors R M] [IsNoetherian R M] (α : L → R) (β : Weight R L M) {n : ℕ} (hn : n ≤ chainTopCoeff α β) : genWeightSpace M (n • α + ⇑β) ≠ ⊥

theorem LieModule.genWeightSpace_zsmul_add_ne_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] [LieRing.IsNilpotent L] [NoZeroSMulDivisors ℤ R] [NoZeroSMulDivisors R M] [IsNoetherian R M] (α : L → R) (β : Weight R L M) {n : ℤ} (hn : -↑(chainBotCoeff α β) ≤ n) (hn' : n ≤ ↑(chainTopCoeff α β)) : genWeightSpace M (n • α + ⇑β) ≠ ⊥

theorem LieModule.genWeightSpace_neg_zsmul_add_ne_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] [LieRing.IsNilpotent L] [NoZeroSMulDivisors ℤ R] [NoZeroSMulDivisors R M] [IsNoetherian R M] (α : L → R) (β : Weight R L M) {n : ℕ} (hn : n ≤ chainBotCoeff α β) : genWeightSpace M (-↑n • α + ⇑β) ≠ ⊥

noncomputable def LieModule.chainTop {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] [LieRing.IsNilpotent L] [NoZeroSMulDivisors ℤ R] [NoZeroSMulDivisors R M] [IsNoetherian R M] (α : L → R) (β : Weight R L M) : Weight R L M

The last weight in an α-chain through β.

Equations

• LieModule.chainTop α β = { toFun := LieModule.chainTopCoeff α β • α + ⇑β, genWeightSpace_ne_bot' := ⋯ }

noncomputable def LieModule.chainBot {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] [LieRing.IsNilpotent L] [NoZeroSMulDivisors ℤ R] [NoZeroSMulDivisors R M] [IsNoetherian R M] (α : L → R) (β : Weight R L M) : Weight R L M

The first weight in an α-chain through β.

Equations

• LieModule.chainBot α β = { toFun := -↑(LieModule.chainBotCoeff α β) • α + ⇑β, genWeightSpace_ne_bot' := ⋯ }

theorem LieModule.coe_chainTop' {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] [LieRing.IsNilpotent L] [NoZeroSMulDivisors ℤ R] [NoZeroSMulDivisors R M] [IsNoetherian R M] (α : L → R) (β : Weight R L M) : ⇑(chainTop α β) = chainTopCoeff α β • α + ⇑β

@[simp]

theorem LieModule.coe_chainTop {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] [LieRing.IsNilpotent L] [NoZeroSMulDivisors ℤ R] [NoZeroSMulDivisors R M] [IsNoetherian R M] (α : L → R) (β : Weight R L M) : ⇑(chainTop α β) = ↑(chainTopCoeff α β) • α + ⇑β

@[simp]

theorem LieModule.coe_chainBot {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] [LieRing.IsNilpotent L] [NoZeroSMulDivisors ℤ R] [NoZeroSMulDivisors R M] [IsNoetherian R M] (α : L → R) (β : Weight R L M) : ⇑(chainBot α β) = -↑(chainBotCoeff α β) • α + ⇑β

@[simp]

theorem LieModule.chainTop_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] [LieRing.IsNilpotent L] [NoZeroSMulDivisors ℤ R] [NoZeroSMulDivisors R M] [IsNoetherian R M] (α : L → R) (β : Weight R L M) : chainTop (-α) β = chainBot α β

@[simp]

theorem LieModule.chainBot_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] [LieRing.IsNilpotent L] [NoZeroSMulDivisors ℤ R] [NoZeroSMulDivisors R M] [IsNoetherian R M] (α : L → R) (β : Weight R L M) : chainBot (-α) β = chainTop α β

@[simp]

theorem LieModule.chainTop_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] [LieRing.IsNilpotent L] [NoZeroSMulDivisors ℤ R] [NoZeroSMulDivisors R M] [IsNoetherian R M] (β : Weight R L M) : chainTop 0 β = β

@[simp]

theorem LieModule.chainBot_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] [LieRing.IsNilpotent L] [NoZeroSMulDivisors ℤ R] [NoZeroSMulDivisors R M] [IsNoetherian R M] (β : Weight R L M) : chainBot 0 β = β

theorem LieModule.genWeightSpace_add_chainTop {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] [LieRing.IsNilpotent L] [NoZeroSMulDivisors ℤ R] [NoZeroSMulDivisors R M] [IsNoetherian R M] (α : L → R) (β : Weight R L M) (hα : α ≠ 0) : genWeightSpace M (α + ⇑(chainTop α β)) = ⊥

theorem LieModule.genWeightSpace_neg_add_chainBot {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] [LieRing.IsNilpotent L] [NoZeroSMulDivisors ℤ R] [NoZeroSMulDivisors R M] [IsNoetherian R M] (α : L → R) (β : Weight R L M) (hα : α ≠ 0) : genWeightSpace M (-α + ⇑(chainBot α β)) = ⊥

theorem LieModule.chainTop_isNonZero' {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] [LieRing.IsNilpotent L] [NoZeroSMulDivisors ℤ R] [NoZeroSMulDivisors R M] [IsNoetherian R M] (α : L → R) (β : Weight R L M) (hα : α ≠ 0) (hα' : genWeightSpace M α ≠ ⊥) : (chainTop α β).IsNonZero

theorem LieModule.chainTop_isNonZero {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] [LieRing.IsNilpotent L] [NoZeroSMulDivisors ℤ R] [NoZeroSMulDivisors R M] [IsNoetherian R M] (α β : Weight R L M) (hα : α.IsNonZero) : (chainTop (⇑α) β).IsNonZero

theorem LieModule.isNilpotent_toEnd_of_mem_rootSpace {L : Type u_2} [LieRing L] (M : Type u_3) [AddCommGroup M] [LieRingModule L M] {K : Type u_4} [Field K] [CharZero K] [LieAlgebra K L] (H : LieSubalgebra K L) [LieRing.IsNilpotent ↥H] [Module K M] [LieModule K L M] [IsTriangularizable K (↥H) M] [FiniteDimensional K M] {x : L} {χ : ↥H → K} (hχ : χ ≠ 0) (hx : x ∈ LieAlgebra.rootSpace H χ) : _root_.IsNilpotent ((toEnd K L M) x)

theorem LieAlgebra.isNilpotent_ad_of_mem_rootSpace {L : Type u_2} [LieRing L] {K : Type u_4} [Field K] [CharZero K] [LieAlgebra K L] (H : LieSubalgebra K L) [LieRing.IsNilpotent ↥H] [LieModule.IsTriangularizable K (↥H) L] [FiniteDimensional K L] {x : L} {χ : ↥H → K} (hχ : χ ≠ 0) (hx : x ∈ rootSpace H χ) : IsNilpotent ((ad K L) x)