exists_genWeightSpace_le_ker_of_isNoetherian

English

Equivalence of iSup_ucs with genWeightSpace at zero in a Noetherian setting (alternative formulation).

Русский

Другая формулировка эквивалентности iSup_ucs и genWeightSpace 0 при условиях Ноetherian.

LaTeX

$$iSup (fun k => (⊥ : LieSubmodule R L M).ucs k) = genWeightSpace M (0 : L → R)$$

Lean4

theorem exists_genWeightSpace_le_ker_of_isNoetherian [IsNoetherian R M] (χ : L → R) (x : L) :
    ∃ k : ℕ, genWeightSpace M χ ≤ LinearMap.ker ((toEnd R L M x - algebraMap R _ (χ x)) ^ k) :=
  by
  use (toEnd R L M x).maxGenEigenspaceIndex (χ x)
  intro m hm
  replace hm : m ∈ (toEnd R L M x).maxGenEigenspace (χ x) := genWeightSpace_le_genWeightSpaceOf M x χ hm
  rwa [Module.End.maxGenEigenspace_eq, Module.End.genEigenspace_nat] at hm

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