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 α)