English
For each i in the distinguished base support, the matrix f(i) is a matrix over R indexed by b.support ⊕ ι, and lies in the crystallographic Lie subalgebra generated by the distinguished root data. In particular, each f(i) is a concrete element of the Lie algebra associated to the root system's Geck construction.
Русский
Для каждого i из выделенной основы базовых индексов матрица f(i) является матрицей над R с индексами b.support ⊕ ι и принадлежит к кристоналной подалгебре Ли, связанной с размещением корней в конструировании Geck.
LaTeX
$$$f(i) \in \operatorname{lieAlgebra}(b)$$$
Lean4
/-- Part of an `sl₂` triple used in Geck's construction of a Lie algebra from a root system. -/
def f (i : b.support) : Matrix (b.support ⊕ ι) (b.support ⊕ ι) R :=
open scoped Classical in
letI := P.indexNeg
.fromBlocks 0 (.of fun i' j ↦ if i' = i ∧ j = i then 1 else 0)
(.of fun i' j ↦ if i' = -i then ↑|b.cartanMatrix i j| else 0)
(.of fun i' j ↦ if P.root i' = P.root j - P.root i then P.chainTopCoeff i j + 1 else 0)
