coe_genWeightSpaceOf_zero — Mathlib

English

For zero weight χ=0, the generalized weight space genWeightSpaceOf M χ x equals the maximal generalized zero-eigenspace of the endomorphism toEnd R L M x, i.e., its coequal subspace is the supremum of kernels of (toEnd x)^k over k≥0.

Русский

Для нулевого веса χ=0 genWeightSpaceOf M χ x совпадает с наибольшим общим нулевым собственнымspace эндоморфизма toEnd x; т.е. это верхняя граница ядер (toEnd x)^k по k≥0.

LaTeX

$$$\\text{genWeightSpaceOf } M (0) x = \\bigcup_{k \\ge 0} \\ker\\big((\\mathrm{toEnd}\\;R\\;L\\;M\\;x)^k\\big)$$$

Lean4

theorem coe_genWeightSpaceOf_zero (x : L) : ↑(genWeightSpaceOf M (0 : R) x) = ⨆ k, LinearMap.ker (toEnd R L M x ^ k) :=
  by simp [genWeightSpaceOf, ← Module.End.iSup_genEigenspace_eq]

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