corootSubmodule — Mathlib

English

The root-associated sl2-submodule is generated by the root-space components and the coroot.

Русский

Подмодуль sl2, связанный с корнем, порождается компонентами корневого пространства и коротом.

LaTeX

$$sl2SubmoduleOfRoot α = genWeightSpace L α ⊔ genWeightSpace L (−α) ⊔ corootSubmodule α$$

Lean4

/-- The coroot space of `α` viewed as a submodule of the ambient Lie algebra `L`.
This represents the image of the coroot space under the inclusion `H ↪ L`. -/
noncomputable abbrev corootSubmodule (α : Weight K H L) : LieSubmodule K H L :=
  LieSubmodule.map H.toLieSubmodule.incl (corootSpace α)

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