English
If L is nontrivial, then the chain length with α = 0 and any β vanishes: chainLength 0 β = 0.
Русский
Если модуль L не тривиален, цепная длина для α = 0 равна нулю.
LaTeX
$$$\operatorname{chainLength}(0, \beta) = 0$$$
Lean4
theorem chainBotCoeff_add_chainTopCoeff : chainBotCoeff α β + chainTopCoeff α β = chainLength α β :=
by
by_cases hα : α.IsZero
· rw [hα.eq, chainTopCoeff_zero, chainBotCoeff_zero, zero_add, chainLength_of_isZero α β hα]
apply le_antisymm
· rw [← Nat.le_sub_iff_add_le (chainTopCoeff_le_chainLength α β), ← not_lt, ← Nat.succ_le, chainBotCoeff, ←
Weight.coe_neg]
intro e
apply genWeightSpace_nsmul_add_ne_bot_of_le _ _ e
rw [← Nat.cast_smul_eq_nsmul ℤ, Nat.cast_succ, Nat.cast_sub (chainTopCoeff_le_chainLength α β),
LieModule.Weight.coe_neg, smul_neg, ← neg_smul, neg_add_rev, neg_sub, sub_eq_neg_add, ← add_assoc, ← neg_add_rev,
add_smul, add_assoc, ← coe_chainTop, neg_smul, ← @Nat.cast_one ℤ, ← Nat.cast_add, Nat.cast_smul_eq_nsmul]
exact rootSpace_neg_nsmul_add_chainTop_of_lt α β hα (Nat.lt_succ_self _)
· rw [← not_lt]
intro e
apply rootSpace_neg_nsmul_add_chainTop_of_le α β e
rw [← Nat.succ_add, ← Nat.cast_smul_eq_nsmul ℤ, ← neg_smul, coe_chainTop, ← add_assoc, ← add_smul, Nat.cast_add,
neg_add, add_assoc, neg_add_cancel, add_zero, neg_smul, ← smul_neg, Nat.cast_smul_eq_nsmul]
exact genWeightSpace_chainTopCoeff_add_one_nsmul_add (-α) β (Weight.IsNonZero.neg hα)
