mapsTo_toEnd_genWeightSpace_add_of_mem_rootSpace

English

If x acts nilpotently on a weight space via the endomorphism, then all its iterated actions remain inside the appropriate weight spaces.

Русский

Если x действует нильпотентно на весовом пространстве через эндоморфизм, то все итерационные действия остаются внутри соответствующих весовых пространств.

LaTeX

$$$\forall n:\mathbb{N}, (toEnd\; R L M x)^n(m) \in \mathrm{genWeightSpace} M (n\cdot χ_1 + χ_2)$, когда $m\in \mathrm{genWeightSpace} M χ_2$$$

Lean4

theorem mapsTo_toEnd_genWeightSpace_add_of_mem_rootSpace (α χ : H → R) {x : L} (hx : x ∈ rootSpace H α) :
    MapsTo (toEnd R L M x) (genWeightSpace M χ) (genWeightSpace M (α + χ)) :=
  by
  intro m hm
  let x' : rootSpace H α := ⟨x, hx⟩
  let m' : genWeightSpace M χ := ⟨m, hm⟩
  exact (rootSpaceWeightSpaceProduct R L H M α χ (α + χ) rfl (x' ⊗ₜ m')).property

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