English
If α is nonzero and n is strictly less than the chain length, then the root space at -(nα) + chainTop α β is nontrivial: rootSpace H (-(n • α) + chainTop α β) ≠ ⊥.
Русский
Если α не нулевой и n строго меньше chainLength, то корневое пространство по -(nα) + chainTop α β не нулево: ≠ ⊥.
LaTeX
$$$\text{If } α \neq 0,\; n < \operatorname{chainLength}(α,β) \Rightarrow \operatorname{rootSpace}(H, -(n \cdot α) + \operatorname{chainTop}(α,β)) \neq ⊥$$$
Lean4
theorem rootSpace_neg_nsmul_add_chainTop_of_lt (hα : α.IsNonZero) {n : ℕ} (hn : chainLength α β < n) :
rootSpace H (-(n • α) + chainTop α β) = ⊥ := by
by_contra e
let W : Weight K H L := ⟨_, e⟩
have hW : (W : H → K) = -(n • α) + chainTop α β := rfl
have H₁ : 1 + n + chainTopCoeff (-α) W ≤ chainLength (-α) W :=
by
have := apply_coroot_eq_cast' (-α) W
simp only [coroot_neg, map_neg, hW, nsmul_eq_mul, Pi.natCast_def, coe_chainTop, zsmul_eq_mul, Int.cast_natCast,
Pi.add_apply, Pi.neg_apply, Pi.mul_apply, root_apply_coroot hα, mul_two, apply_coroot_eq_cast' α β, Int.cast_sub,
Int.cast_mul, Int.cast_ofNat, mul_comm (2 : K), add_sub_cancel, add_sub, Nat.cast_inj, eq_sub_iff_add_eq,
← Nat.cast_add, ← sub_eq_neg_add, sub_eq_iff_eq_add] at this
omega
have H₂ : ((1 + n + chainTopCoeff (-α) W) • α + chainTop (-α) W : H → K) = (chainTopCoeff α β + 1) • α + β :=
by
simp only [Weight.coe_neg, ← Nat.cast_smul_eq_nsmul ℤ, Nat.cast_add, Nat.cast_one, coe_chainTop, smul_neg,
← neg_smul, hW, ← add_assoc, ← add_smul, ← sub_eq_add_neg]
congr 2
ring
have := rootSpace_neg_nsmul_add_chainTop_of_le (-α) W H₁
rw [Weight.coe_neg, ← smul_neg, neg_neg, ← Weight.coe_neg, H₂] at this
exact this (genWeightSpace_chainTopCoeff_add_one_nsmul_add α β hα)
