iSup_genWeightSpace_eq_top' — Mathlib

English

In the alg-closed setting, or under triangularizability, the iSup over weights in Weight(K,L,M) of genWeightSpace M χ equals top.

Русский

В условии треугольности или при алгебраически замкнутом поле берём супремум по всем весам — получаем верхний подмодуль.

LaTeX

$$$\bigvee_{\chi \in \mathrm{Weight}(K,L,M)} \mathrm{genWeightSpace}(M,\chi) = \top$$$

Lean4

theorem iSup_genWeightSpace_eq_top' [IsTriangularizable K L M] : ⨆ χ : Weight K L M, genWeightSpace M χ = ⊤ :=
  by
  have := iSup_genWeightSpace_eq_top K L M
  erw [← iSup_ne_bot_subtype, ← (Weight.equivSetOf K L M).iSup_comp] at this
  exact this

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