lie_eq_killingForm_smul_of_mem_rootSpace_of_mem_rootSpace_neg

English

If e ∈ rootSpace α and f ∈ rootSpace −α, then [e,f] equals the Killing form evaluated at (e,f) times the Cartan dual of α.

Русский

Если e из пространства корня α и f из пространства −α, то [e,f] = Killing(e,f) · (cartanEquivDual H)⁻¹(α).

LaTeX

$$$[e,f] = \operatorname{Killing}(e,f) \cdot (\mathrm{cartanEquivDual} H)^{-1}(\alpha)\quad (e\in\mathfrak{g}_\alpha, f\in\mathfrak{g}_{-\alpha})$$$

Lean4

theorem lie_eq_killingForm_smul_of_mem_rootSpace_of_mem_rootSpace_neg {α : Weight K H L} {e f : L}
    (heα : e ∈ rootSpace H α) (hfα : f ∈ rootSpace H (-α)) :
    ⁅e, f⁆ = killingForm K L e f • (cartanEquivDual H).symm α :=
  by
  apply lie_eq_killingForm_smul_of_mem_rootSpace_of_mem_rootSpace_neg_aux heα hfα
  exact lie_eq_smul_of_mem_rootSpace heα

Похожие утверждения