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.

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] [LieAlgebra.IsNilpotent R L] (χ₁ : L → R) (χ₂ : L → R) [NoZeroSMulDivisors ℤ R] [NoZeroSMulDivisors R M] [IsNoetherian R M] (hχ₁ : χ₁ ≠ 0) : ∀ᶠ (k : ℕ) in Filter.atTop, LieModule.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] [LieAlgebra.IsNilpotent R L] (χ₁ : L → R) (χ₂ : L → R) [NoZeroSMulDivisors ℤ R] [NoZeroSMulDivisors R M] [IsNoetherian R M] (hχ₁ : χ₁ ≠ 0) : ∃ k > 0, LieModule.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] [LieAlgebra.IsNilpotent R L] (χ₁ : L → R) (χ₂ : L → R) [NoZeroSMulDivisors ℤ R] [NoZeroSMulDivisors R M] [IsNoetherian R M] (hχ₁ : χ₁ ≠ 0) : ∃ p < 0, ∃ q > 0, LieModule.genWeightSpace M (p • χ₁ + χ₂) = ⊥ ∧ LieModule.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] [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.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] [LieAlgebra.IsNilpotent R L] (χ₁ : L → R) (χ₂ : L → R) (p : ℤ) (q : ℤ) : 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] [LieAlgebra.IsNilpotent R L] (χ₁ : L → R) (χ₂ : L → R) (p : ℤ) (q : ℤ) : LieModule.genWeightSpaceChain M χ₁ χ₂ p q = ⨆ k ∈ Finset.Ioo p q, LieModule.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] [LieAlgebra.IsNilpotent R L] (χ₁ : L → R) (χ₂ : L → R) (p : ℤ) (q : ℤ) : LieModule.genWeightSpaceChain M (-χ₁) χ₂ (-q) (-p) = LieModule.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] [LieAlgebra.IsNilpotent R L] (χ₁ : L → R) (χ₂ : L → R) (p : ℤ) (q : ℤ) {k : ℤ} (hk : k ∈ Set.Ioo p q) : LieModule.genWeightSpace M (k • χ₁ + χ₂) ≤ LieModule.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) (χ : ↥H → R) (p : ℤ) (q : ℤ) [LieAlgebra.IsNilpotent R ↥H] (hq : LieModule.genWeightSpace M (q • α + χ) = ⊥) {x : L} (hx : x ∈ LieAlgebra.rootSpace H α) {y : M} (hy : y ∈ LieModule.genWeightSpaceChain M α χ p q) : ⁅x, y⁆ ∈ LieModule.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) (χ : ↥H → R) (p : ℤ) (q : ℤ) [LieAlgebra.IsNilpotent R ↥H] (hp : LieModule.genWeightSpace M (p • α + χ) = ⊥) {x : L} (hx : x ∈ LieAlgebra.rootSpace H (-α)) {y : M} (hy : y ∈ LieModule.genWeightSpaceChain M α χ p q) : ⁅x, y⁆ ∈ LieModule.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) (χ : ↥H → R) (p : ℤ) (q : ℤ) [H.IsCartanSubalgebra] [IsNoetherian R L] (hp : LieModule.genWeightSpace M (p • α + χ) = ⊥) (hq : LieModule.genWeightSpace M (q • α + χ) = ⊥) {x : ↥H} (hx : x ∈ LieAlgebra.corootSpace α) : (LinearMap.trace R ↥(LieModule.genWeightSpaceChain M α χ p q)) ((LieModule.toEnd R ↥H ↥(LieModule.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 → R) [H.IsCartanSubalgebra] [IsNoetherian R L] [IsDomain R] [IsPrincipalIdealRing R] [CharZero R] [NoZeroSMulDivisors R M] [IsNoetherian R M] (hα : α ≠ 0) (hχ : LieModule.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] [LieAlgebra.IsNilpotent R L] [NoZeroSMulDivisors ℤ R] [NoZeroSMulDivisors R M] [IsNoetherian R M] (α : L → R) (β : LieModule.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] [LieAlgebra.IsNilpotent R L] [NoZeroSMulDivisors ℤ R] [NoZeroSMulDivisors R M] [IsNoetherian R M] (α : L → R) (β : LieModule.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] [LieAlgebra.IsNilpotent R L] [NoZeroSMulDivisors ℤ R] [NoZeroSMulDivisors R M] [IsNoetherian R M] (α : L → R) (β : LieModule.Weight R L M) : LieModule.chainTopCoeff (-α) β = LieModule.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] [LieAlgebra.IsNilpotent R L] [NoZeroSMulDivisors ℤ R] [NoZeroSMulDivisors R M] [IsNoetherian R M] (α : L → R) (β : LieModule.Weight R L M) : LieModule.chainBotCoeff (-α) β = LieModule.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] [LieAlgebra.IsNilpotent R L] [NoZeroSMulDivisors ℤ R] [NoZeroSMulDivisors R M] [IsNoetherian R M] (β : LieModule.Weight R L M) : LieModule.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] [LieAlgebra.IsNilpotent R L] [NoZeroSMulDivisors ℤ R] [NoZeroSMulDivisors R M] [IsNoetherian R M] (β : LieModule.Weight R L M) : LieModule.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] [LieAlgebra.IsNilpotent R L] [NoZeroSMulDivisors ℤ R] [NoZeroSMulDivisors R M] [IsNoetherian R M] (α : L → R) (β : LieModule.Weight R L M) (hα : α ≠ 0) : LieModule.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] [LieAlgebra.IsNilpotent R L] [NoZeroSMulDivisors ℤ R] [NoZeroSMulDivisors R M] [IsNoetherian R M] (α : L → R) (β : LieModule.Weight R L M) (hα : α ≠ 0) : LieModule.genWeightSpace M ((LieModule.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] [LieAlgebra.IsNilpotent R L] [NoZeroSMulDivisors ℤ R] [NoZeroSMulDivisors R M] [IsNoetherian R M] (α : L → R) (β : LieModule.Weight R L M) (hα : α ≠ 0) : LieModule.genWeightSpace M ((↑(LieModule.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] [LieAlgebra.IsNilpotent R L] [NoZeroSMulDivisors ℤ R] [NoZeroSMulDivisors R M] [IsNoetherian R M] (α : L → R) (β : LieModule.Weight R L M) (hα : α ≠ 0) : LieModule.genWeightSpace M ((-↑(LieModule.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] [LieAlgebra.IsNilpotent R L] [NoZeroSMulDivisors ℤ R] [NoZeroSMulDivisors R M] [IsNoetherian R M] (α : L → R) (β : LieModule.Weight R L M) {n : ℕ} (hn : n ≤ LieModule.chainTopCoeff α β) : LieModule.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] [LieAlgebra.IsNilpotent R L] [NoZeroSMulDivisors ℤ R] [NoZeroSMulDivisors R M] [IsNoetherian R M] (α : L → R) (β : LieModule.Weight R L M) {n : ℤ} (hn : -↑(LieModule.chainBotCoeff α β) ≤ n) (hn' : n ≤ ↑(LieModule.chainTopCoeff α β)) : LieModule.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] [LieAlgebra.IsNilpotent R L] [NoZeroSMulDivisors ℤ R] [NoZeroSMulDivisors R M] [IsNoetherian R M] (α : L → R) (β : LieModule.Weight R L M) {n : ℕ} (hn : n ≤ LieModule.chainBotCoeff α β) : LieModule.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] [LieAlgebra.IsNilpotent R L] [NoZeroSMulDivisors ℤ R] [NoZeroSMulDivisors R M] [IsNoetherian R M] (α : L → R) (β : LieModule.Weight R L M) : LieModule.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] [LieAlgebra.IsNilpotent R L] [NoZeroSMulDivisors ℤ R] [NoZeroSMulDivisors R M] [IsNoetherian R M] (α : L → R) (β : LieModule.Weight R L M) : LieModule.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] [LieAlgebra.IsNilpotent R L] [NoZeroSMulDivisors ℤ R] [NoZeroSMulDivisors R M] [IsNoetherian R M] (α : L → R) (β : LieModule.Weight R L M) : ⇑(LieModule.chainTop α β) = LieModule.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] [LieAlgebra.IsNilpotent R L] [NoZeroSMulDivisors ℤ R] [NoZeroSMulDivisors R M] [IsNoetherian R M] (α : L → R) (β : LieModule.Weight R L M) : ⇑(LieModule.chainTop α β) = ↑(LieModule.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] [LieAlgebra.IsNilpotent R L] [NoZeroSMulDivisors ℤ R] [NoZeroSMulDivisors R M] [IsNoetherian R M] (α : L → R) (β : LieModule.Weight R L M) : ⇑(LieModule.chainBot α β) = -↑(LieModule.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] [LieAlgebra.IsNilpotent R L] [NoZeroSMulDivisors ℤ R] [NoZeroSMulDivisors R M] [IsNoetherian R M] (α : L → R) (β : LieModule.Weight R L M) : LieModule.chainTop (-α) β = LieModule.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] [LieAlgebra.IsNilpotent R L] [NoZeroSMulDivisors ℤ R] [NoZeroSMulDivisors R M] [IsNoetherian R M] (α : L → R) (β : LieModule.Weight R L M) : LieModule.chainBot (-α) β = LieModule.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] [LieAlgebra.IsNilpotent R L] [NoZeroSMulDivisors ℤ R] [NoZeroSMulDivisors R M] [IsNoetherian R M] (β : LieModule.Weight R L M) : LieModule.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] [LieAlgebra.IsNilpotent R L] [NoZeroSMulDivisors ℤ R] [NoZeroSMulDivisors R M] [IsNoetherian R M] (β : LieModule.Weight R L M) : LieModule.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] [LieAlgebra.IsNilpotent R L] [NoZeroSMulDivisors ℤ R] [NoZeroSMulDivisors R M] [IsNoetherian R M] (α : L → R) (β : LieModule.Weight R L M) (hα : α ≠ 0) : LieModule.genWeightSpace M (α + ⇑(LieModule.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] [LieAlgebra.IsNilpotent R L] [NoZeroSMulDivisors ℤ R] [NoZeroSMulDivisors R M] [IsNoetherian R M] (α : L → R) (β : LieModule.Weight R L M) (hα : α ≠ 0) : LieModule.genWeightSpace M (-α + ⇑(LieModule.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] [LieAlgebra.IsNilpotent R L] [NoZeroSMulDivisors ℤ R] [NoZeroSMulDivisors R M] [IsNoetherian R M] (α : L → R) (β : LieModule.Weight R L M) (hα : α ≠ 0) (hα' : LieModule.genWeightSpace M α ≠ ⊥) : (LieModule.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] [LieAlgebra.IsNilpotent R L] [NoZeroSMulDivisors ℤ R] [NoZeroSMulDivisors R M] [IsNoetherian R M] (α : LieModule.Weight R L M) (β : LieModule.Weight R L M) (hα : α.IsNonZero) : (LieModule.chainTop (⇑α) β).IsNonZero