English
If H is a nilpotent Lie subalgebra of L, then H.toLieSubmodule is contained in the root space of weight zero, i.e., H.toLieSubmodule ≤ rootSpace H 0.
Русский
Если H — нильпотентная подалгебра Ли внутри L, то H.toLieSubmodule вложено в пространство корней нулевого веса: H.toLieSubmodule ≤ rootSpace H 0.
LaTeX
$$toLieSubmodule_le_rootSpace_zero : H.toLieSubmodule ≤ rootSpace H 0$$
Lean4
theorem toLieSubmodule_le_rootSpace_zero : H.toLieSubmodule ≤ rootSpace H 0 :=
by
intro x hx
simp only [LieSubalgebra.mem_toLieSubmodule] at hx
simp only [mem_genWeightSpace, Pi.zero_apply, sub_zero, zero_smul]
intro y
obtain ⟨k, hk⟩ := IsNilpotent.nilpotent R H H
use k
let f : Module.End R H := toEnd R H H y
let g : Module.End R L := toEnd R H L y
have hfg : g.comp (H : Submodule R L).subtype = (H : Submodule R L).subtype.comp f := rfl
change (g ^ k).comp (H : Submodule R L).subtype ⟨x, hx⟩ = 0
rw [Module.End.commute_pow_left_of_commute hfg k]
have h := iterate_toEnd_mem_lowerCentralSeries R H H y ⟨x, hx⟩ k
rw [hk, LieSubmodule.mem_bot] at h
simp only [Submodule.subtype_apply, Function.comp_apply, Module.End.pow_apply, LinearMap.coe_comp,
Submodule.coe_eq_zero]
exact h
