iSup_genWeightSpaceOf_eq_top — Mathlib

English

For a triangularizable finite-dimensional module, the weight-spaces generate the entire module; i.e., the join of genWeightSpace M χ across all χ equals M.

Русский

Для треугольного конечномерного модуля весовые пространства порождают весь модуль; наслоение весовых пространств даёт весь модуль.

LaTeX

$$$\bigvee_{\chi} \mathrm{genWeightSpace}(M,\chi) = M$$$

Lean4

@[simp]
theorem iSup_genWeightSpaceOf_eq_top [IsTriangularizable R L M] (x : L) : ⨆ (φ : R), genWeightSpaceOf M φ x = ⊤ :=
  by
  rw [← LieSubmodule.toSubmodule_inj, LieSubmodule.iSup_toSubmodule, LieSubmodule.top_toSubmodule]
  dsimp [genWeightSpaceOf]
  exact IsTriangularizable.maxGenEigenspace_eq_top x

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