English
The Lie algebra associated to the crystallographic root datum with base b is the Lie subalgebra generated by the elements h, e, f coming from the root data; explicitly it is the Lie span of h, e, f inside the matrix algebra on b.support ⊕ ι.
Русский
Ли-алгебра кристаллографических данных корней с основанием b является подалгеброй Ли, порождённой элементами h, e, f, взятыми из данных корня; явно это — линейная оболочка по r-коэффициентам h, e, f внутри матричной алгебры на b.support ⊕ ι.
LaTeX
$$$\operatorname{lieAlgebra}(b) = \operatorname{LieSubalgebra}(R)\;\text{generated by } h,e,f$$$
Lean4
/-- Geck's construction of the Lie algebra associated to a root system with distinguished base.
Note that it is convenient to include `range h` in the Lie span, to make it elementary that it
contains `RootPairing.GeckConstruction.cartanSubalgebra`, and not depend on
`RootPairing.GeckConstruction.lie_e_f_same`. -/
def lieAlgebra [Fintype ι] [DecidableEq ι] : LieSubalgebra R (Matrix (b.support ⊕ ι) (b.support ⊕ ι) R) :=
LieSubalgebra.lieSpan R _ (range h ∪ range e ∪ range f)
