English
Let e, f, h form an sl2-triple acting on a Lie module M with a primitive vector ψ indexed by n. Then for every natural number n, the Lie bracket of e with ψ(n+1) is proportional to ψ(n) with scalar ((n+1)(μ − n)).
Русский
Пусть e, f, h образуют тройку sl2, действующую на линейном модуле M, и имеется примитивный вектор ψ, индексируемый по n. Тогда для каждого натурального n элемент [e, ψ(n+1)] пропорционален ψ(n) с коэффициентом (n+1)(μ − n).
LaTeX
$$$[e, \psi(n+1)] = ((n+1) \cdot (\mu - n)) \cdot \psi(n)$$$
Lean4
theorem lie_e_pow_succ_toEnd_f (n : ℕ) : ⁅e, ψ(n + 1)⁆ = ((n + 1) * (μ - n)) • ψ n := by
induction n with
| zero =>
simp only [zero_add, pow_one, toEnd_apply_apply, Nat.cast_zero, sub_zero, one_mul, pow_zero, Module.End.one_apply,
leibniz_lie e, t.lie_e_f, P.lie_e, P.lie_h, lie_zero, add_zero]
| succ n
ih =>
rw [pow_succ', Module.End.mul_apply, toEnd_apply_apply, leibniz_lie e, t.lie_e_f, lie_h_pow_toEnd_f P, ih, lie_smul,
lie_f_pow_toEnd_f P, ← add_smul, Nat.cast_add, Nat.cast_one]
congr
ring
