genWeightSpace_zero_normalizer_eq_self

English

There is a lemma expressing that the weight-space at weight χ x is nonzero when considering generalized eigenvectors.

Русский

Существует лемма, выражающая не равно нулю весовое пространство χ(x) для обобщённых собственных векторов.

LaTeX

$$genWeightSpaceOf M (χ x) x ≠ ⊥$$

Lean4

@[simp]
theorem genWeightSpace_zero_normalizer_eq_self : (genWeightSpace M (0 : L → R)).normalizer = genWeightSpace M 0 :=
  by
  refine le_antisymm ?_ (LieSubmodule.le_normalizer _)
  intro m hm
  rw [LieSubmodule.mem_normalizer] at hm
  simp only [mem_genWeightSpace, Pi.zero_apply, zero_smul, sub_zero] at hm ⊢
  intro y
  obtain ⟨k, hk⟩ := hm y y
  use k + 1
  simpa [pow_succ, Module.End.mul_eq_comp]

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