weightSpace_le_genWeightSpace — Mathlib

English

For any χ, weightSpace ≤ genWeightSpace; i.e., every weight vector is contained in the generalized weight space, and the generalized space is the intersection over all original weight components.

Русский

Для любого χ выполнено, что weightSpace ≤ genWeightSpace; то есть любой весовой вектор содержит в обобщенном весовом пространстве, которое является пересечением весовых компонентов.

LaTeX

$$$\\mathrm{weightSpace}(M, χ) \\leq \\mathrm{genWeightSpace}(M, χ)$$$

Lean4

theorem weightSpace_le_genWeightSpace (χ : L → R) : weightSpace M χ ≤ genWeightSpace M χ :=
  by
  apply le_iInf
  intro x
  rw [← (LieSubmodule.toSubmodule_orderEmbedding R L M).le_iff_le]
  apply (iInf_le _ x).trans
  exact ((toEnd R L M x).genEigenspace (χ x)).monotone le_top

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