cartanSubalgebra_eq_lieSpan — Mathlib

English

The Lie subalgebra lieAlgebra(b) is the Lie span of the union of the sets {h_i}, {e_i}, {f_i} for i ranging over the root data, i.e., the smallest Lie subalgebra containing all h_i, e_i, f_i.

Русский

Подалгебра LieAlgebra(b) является наименьшей подалгеброй Ли, которая содержит все элементы h_i, e_i, f_i на всех i из данных корней.

LaTeX

$$$\text{lieAlgebra}(b) = \operatorname{LieSpan}(R,\,\{h_i, e_i, f_i : i\in b.support\})$$$

Lean4

theorem cartanSubalgebra_eq_lieSpan [Fintype ι] [DecidableEq ι] :
    cartanSubalgebra b = LieSubalgebra.lieSpan R _ (range h) :=
  by
  refine le_antisymm LieSubalgebra.submodule_span_le_lieSpan ?_
  rw [LieSubalgebra.lieSpan_le, cartanSubalgebra]
  exact Submodule.subset_span

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