English
A commutator identity holds: [e_i, f_j] ω = - ω [e_j, f_i] with explicit relations given by the root data; this is a compatibility between the e-f blocks and ω.
Русский
Сохраняется тождество `[e_i, f_j] ω = - ω [e_j, e_i]` с учётом корневых данных; это совместимость блоков e-f и ω.
LaTeX
$$$[[e_i,f_j],\omega] = -\omega[[e_j,f_i]]$$$
Lean4
theorem lie_e_f_mul_ω [Fintype ι] (i j : b.support) : ⁅e i, f j⁆ * ω b = -ω b * ⁅e j, f i⁆ := by
classical
calc
⁅e i, f j⁆ * ω b = e i * f j * ω b - f j * e i * ω b := by rw [Ring.lie_def, sub_mul]
_ = e i * (f j * ω b) - f j * (e i * ω b) := by rw [mul_assoc, mul_assoc]
_ = e i * (ω b * e j) - f j * (ω b * f i) := by rw [← ω_mul_e, ← ω_mul_f]
_ = (e i * ω b) * e j - (f j * ω b) * f i := by rw [← mul_assoc, ← mul_assoc]
_ = (ω b * f i) * e j - (ω b * e j) * f i := by rw [← ω_mul_e, ← ω_mul_f]
_ = ω b * (f i * e j) - ω b * (e j * f i) := by rw [mul_assoc, mul_assoc]
_ = -ω b * ⁅e j, f i⁆ := ?_
rw [Ring.lie_def, mul_sub, neg_mul, neg_mul, sub_neg_eq_add]
abel
