English
A collection of technical lemmas showing stability of triangularizability under various constructions (e.g., endomorphism ranges, subalgebras, submodules, and weight-space products)
Русский
Набор технических лемм, демонстрирующих сохранение треуганильности при различных конструкциях (диапазоны эндоморфизмов, подалгебры, подмодули и произведения весовых пространств).
LaTeX
$$$\text{IsTriangularizable}$ preserved under endomorphism ranges, subalgebras, submodules, weight-space products$$
Lean4
/-- Given a nilpotent Lie subalgebra `H ⊆ L` together with `χ₁ χ₂ : H → R`, there is a natural
`R`-bilinear product of root vectors and weight vectors, compatible with the actions of `H`. -/
def rootSpaceWeightSpaceProduct (χ₁ χ₂ χ₃ : H → R) (hχ : χ₁ + χ₂ = χ₃) :
rootSpace H χ₁ ⊗[R] genWeightSpace M χ₂ →ₗ⁅R,H⁆ genWeightSpace M χ₃ :=
liftLie R H (rootSpace H χ₁) (genWeightSpace M χ₂) (genWeightSpace M χ₃)
{ toLinearMap := rootSpaceWeightSpaceProductAux R L H M hχ
map_lie' := fun {x y} => by
ext m
simp only [rootSpaceWeightSpaceProductAux]
dsimp
simp only [lie_lie] }
