English
In a nilpotent setting, there exists a weight χ with a nontrivial weight space inside M.
Русский
В условиях нильпотентности существует вес χ с ненуловым весовым пространством внутри M.
LaTeX
$$$\\exists χ: Weight\\,K\\,L\\,M,\\; weightSpace(M,χ) \\neq \\{0\\}.$$$
Lean4
/-- In characteristic zero, the weights of any finite-dimensional Lie module are linear and vanish
on the derived ideal. -/
instance instLinearWeightsOfCharZero [CharZero R] : LinearWeights R L M
where
map_add χ hχ x
y := by
rw [← smul_right_inj (zero_lt_finrank_genWeightSpace hχ).ne', smul_add, ← Pi.smul_apply, ← Pi.smul_apply, ←
Pi.smul_apply, ← trace_comp_toEnd_genWeightSpace_eq, map_add]
map_smul χ hχ t
x := by
rw [← smul_right_inj (zero_lt_finrank_genWeightSpace hχ).ne', smul_comm, ← Pi.smul_apply, ←
Pi.smul_apply (finrank R _), ← trace_comp_toEnd_genWeightSpace_eq, map_smul]
map_lie χ hχ x
y := by
rw [← smul_right_inj (zero_lt_finrank_genWeightSpace hχ).ne', nsmul_zero, ← Pi.smul_apply, ←
trace_comp_toEnd_genWeightSpace_eq, LinearMap.comp_apply, LieHom.coe_toLinearMap, LieHom.map_lie, Ring.lie_def,
map_sub, LinearMap.trace_mul_comm, sub_self]
