English
Compute commutators with h_j: [h_j, e_i] and [h_j, f_i] yield Cartan actions on e_i and f_i respectively.
Русский
Выражение [h_j, e_i] и [h_j, f_i] дают действие Картановой матрицы на e_i и f_i.
LaTeX
$$$[h_j, e_i] = c_{ij} e_i$, $[h_j, f_i] = -c_{ij} f_i$ (where $c_{ij}$ is cartanMatrix entry)$$
Lean4
/-- Lemma 3.3 (b) from [Geck](Geck2017). -/
theorem lie_h_f : ⁅h j, f i⁆ = -b.cartanMatrix i j • f i := by
classical
suffices ω b * ⁅h j, f i⁆ = ω b * (-b.cartanMatrix i j • f i)
by
replace this := congr_arg (ω b * ·) this
simpa [← mul_assoc, ω_mul_ω] using this
calc
ω b * ⁅h j, f i⁆ = ω b * (h j * f i - f i * h j) := by rw [Ring.lie_def]
_ = -(h j * e i - e i * h j) * ω b := ?_
_ = -⁅h j, e i⁆ * ω b := by rw [Ring.lie_def]
_ = -(b.cartanMatrix i j • e i) * ω b := by rw [lie_h_e]
_ = ω b * (-b.cartanMatrix i j • f i) := ?_
· rw [mul_sub, ← mul_assoc, ← mul_assoc, ω_mul_h, ω_mul_f, mul_assoc, mul_assoc, ω_mul_f, ω_mul_h, neg_sub, neg_mul,
neg_mul, mul_neg, sub_mul, mul_assoc, mul_assoc]
abel
· rw [Matrix.mul_smul, ω_mul_f]
simp [mul_assoc]
