e — Mathlib · SciLib

English

The matrix e(i) is a block matrix encoding the interaction of root data within an sl2 triple.

Русский

Матрица e(i) кодирует взаимодействие корневых данных внутри тройки sl2.

LaTeX

$$e (i) := Block matrix described in Geck construction with blocks determined by root data$$

Lean4

/-- Part of an `sl₂` triple used in Geck's construction of a Lie algebra from a root system. -/
def e (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 i + P.root j then P.chainBotCoeff i j + 1 else 0)

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