instIsTriangularizableSubtypeMemLieSubmodule_1

English

If M is triangularizable for the action of L, then the endomorphism range formed by this action is triangularizable.

Русский

Если M треугольна по действию L, то диапазон эндоморфизмов этого действия треугольизируем.

LaTeX

$$$\text{IsTriangularizable}(R,L,M) \Rightarrow \text{IsTriangularizable}(R,(\mathrm{LieModule}.toEnd R L M).range M)$$$

Lean4

instance (N : LieSubmodule K L M) [IsTriangularizable K L M] : IsTriangularizable K L N :=
  by
  refine ⟨fun y ↦ ?_⟩
  rw [← N.toEnd_restrict_eq_toEnd y]
  exact Module.End.genEigenspace_restrict_eq_top _ (IsTriangularizable.maxGenEigenspace_eq_top y)

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