English
If α is nonzero, and n is a natural number not exceeding the chain length, the root space at the element -(nα) + chainTop α β is nontrivial: rootSpace H (-(n • α) + chainTop α β) ≠ ⊥.
Русский
Пусть α не нулевой, и n натуральное число, не превосходящее длину цепи; тогда корневое пространство по элементу −(nα) + chainTop α β не тривиально.
LaTeX
$$$\text{If } α \neq 0,\; n \le \operatorname{chainLength}(α,β)\; \Rightarrow\; \operatorname{rootSpace}(H, -(n \cdot α) + \operatorname{chainTop}(α,β)) \neq \{0\}$$$
Lean4
theorem rootSpace_neg_nsmul_add_chainTop_of_le {n : ℕ} (hn : n ≤ chainLength α β) :
rootSpace H (-(n • α) + chainTop α β) ≠ ⊥ :=
by
by_cases hα : α.IsZero
· simpa only [hα.eq, smul_zero, neg_zero, chainTop_zero, zero_add, ne_eq] using β.2
obtain ⟨x, hx, x_ne0⟩ := (chainTop α β).exists_ne_zero
obtain ⟨h, e, f, isSl2, he, hf⟩ := exists_isSl2Triple_of_weight_isNonZero hα
obtain rfl := isSl2.h_eq_coroot hα he hf
have prim : isSl2.HasPrimitiveVectorWith x (chainLength α β : K) :=
have := lie_mem_genWeightSpace_of_mem_genWeightSpace he hx
⟨x_ne0, (chainLength_smul _ _ hx).symm, by rwa [genWeightSpace_add_chainTop _ _ hα] at this⟩
simp only [← smul_neg, ne_eq, LieSubmodule.eq_bot_iff, not_forall]
exact ⟨_, toEnd_pow_apply_mem hf hx n, prim.pow_toEnd_f_ne_zero_of_eq_nat rfl hn⟩
