English
Let α, β be weights for a triangularizable Cartan subalgebra acting on a finite-dimensional module; for any x in the α-chain top root space, the n-th chain length action of α on x equals the Lie bracket with the coroot of α: chainLength α β · x = [coroot α, x]. In particular, when α = 0 this is trivial, and otherwise this describes a precise weight-space action.
Русский
Пусть α, β — веса для треугольной подлежатCartan-подалгебры, действующей на конечно-размерный модуль; для любого x из пространства корневых состояний цепи α-цепи вверху, действие цепной длины chainLength α β на x равно скобке [coroot α, x]. В частности, при α = 0 это тривиально; иначе это задаёт точное описание действия на весовом подпространстве.
LaTeX
$$$\operatorname{chainLength}(\alpha, \beta) \cdot x = [\operatorname{coroot}(\alpha), x]$$$
Lean4
theorem chainLength_nsmul {x} (hx : x ∈ rootSpace H (chainTop α β)) : chainLength α β • x = ⁅coroot α, x⁆ :=
by
by_cases hα : α.IsZero
· rw [coroot_eq_zero_iff.mpr hα, chainLength_of_isZero _ _ hα, zero_smul, zero_lie]
let x' := (chainTop α β).exists_ne_zero.choose
have h : x' ∈ rootSpace H (chainTop α β) ∧ x' ≠ 0 := (chainTop α β).exists_ne_zero.choose_spec
obtain ⟨k, rfl⟩ : ∃ k : K, k • x' = x := by
simpa using
(finrank_eq_one_iff_of_nonzero' ⟨x', h.1⟩ (by simpa using h.2)).mp
(finrank_rootSpace_eq_one _ (chainTop_isNonZero α β hα)) ⟨_, hx⟩
rw [lie_smul, smul_comm, chainLength, dif_neg hα, (chainLength_aux α β hα h.1).choose_spec]
