HH — Mathlib · SciLib

English

For a Lie algebra with generators indexed by B and a Cartan matrix A, the ad action raised to the power (−A_{ij}) clipped to Nat yields the relation involving ad(E_i) and the bracket [E_i, E_j].

Русский

Для Ли-алгебры с генераторами, индексы которых задаются B, и матрицей Кардана A, действие ad(E_i)^{(−A_{ij}).toNat} на [E_i,E_j] задаёт отношение между этими элементами.

LaTeX

$$$\\text{adE } :=\\; \\text{uncurry }(\\lambda i j,\\; \\operatorname{ad}(E_i)^{(-A_{ij}).toNat}( [E_i,E_j]))$$$

Lean4

/-- The terms corresponding to the `⁅H, H⁆`-relations. -/
def HH : B × B → FreeLieAlgebra R (Generators B) :=
  uncurry fun i j => ⁅H i, H j⁆

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