English
The image of a weight α under the Cartan dual's inverse lies in the coroot space of α.
Русский
Образ веса α через обратное отображение картан-дайлa лежит в корневом пространстве α.
LaTeX
$$$ (\\operatorname{cartanEquivDual} H)^{-1}(\\alpha) \\in \\mathrm{corootSpace}(\\alpha) $$$
Lean4
/-- If a Lie algebra `L` has non-degenerate Killing form, the only element of a Cartan subalgebra
whose adjoint action on `L` is nilpotent, is the zero element.
Over a perfect field a much stronger result is true, see
`LieAlgebra.IsKilling.isSemisimple_ad_of_mem_isCartanSubalgebra`. -/
theorem eq_zero_of_isNilpotent_ad_of_mem_isCartanSubalgebra {x : L} (hx : x ∈ H) (hx' : _root_.IsNilpotent (ad K L x)) :
x = 0 :=
by
suffices ⟨x, hx⟩ ∈ LinearMap.ker (traceForm K H L)
by
simp only [ker_traceForm_eq_bot_of_isCartanSubalgebra, Submodule.mem_bot] at this
exact (AddSubmonoid.mk_eq_zero H.toAddSubmonoid).mp this
simp only [LinearMap.mem_ker]
ext y
have comm : Commute (toEnd K H L ⟨x, hx⟩) (toEnd K H L y) := by
rw [commute_iff_lie_eq, ← LieHom.map_lie, trivial_lie_zero, LieHom.map_zero]
rw [traceForm_apply_apply, ← Module.End.mul_eq_comp, LinearMap.zero_apply]
exact (LinearMap.isNilpotent_trace_of_isNilpotent (comm.isNilpotent_mul_right hx')).eq_zero
