rootSpaceProduct — Mathlib

English

Auxiliary construction giving a linear map from root space to weight space using the weight-addition rule χ1+χ2=χ3.

Русский

Вспомогательная конструкция задающая линейное отображение из корневого пространства в весовое пространство по правилу сложения весов χ1+χ2=χ3.

LaTeX

$$$\mathrm{rootSpaceWeightSpaceProductAux}\; (χ_1,χ_2,χ_3) : \text{...}$$$

Lean4

/-- Given a nilpotent Lie subalgebra `H ⊆ L` together with `χ₁ χ₂ : H → R`, there is a natural
`R`-bilinear product of root vectors, compatible with the actions of `H`. -/
def rootSpaceProduct (χ₁ χ₂ χ₃ : H → R) (hχ : χ₁ + χ₂ = χ₃) :
    rootSpace H χ₁ ⊗[R] rootSpace H χ₂ →ₗ⁅R,H⁆ rootSpace H χ₃ :=
  rootSpaceWeightSpaceProduct R L H L χ₁ χ₂ χ₃ hχ

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