English
If the finite-dimensional Lie algebra L over a field K satisfies finrank_K L ≤ #K, then there exists x ∈ L such that engel_K x is a Cartan subalgebra of L.
Русский
Если конечномерная надпольная Ли-алгебра L над полем K удовлетворяет условию finrank_K L ≤ #K, то существует элемент x ∈ L такой, что engel_K x является картановой подалгеброй L.
LaTeX
$$$\\exists x\\in L:\\; \\operatorname{engel} K x\\; \\text{IsCartanSubalgebra} \\; (L) $$$
Lean4
theorem exists_isCartanSubalgebra_engel_of_finrank_le_card (h : finrank K L ≤ #K) :
∃ x : L, IsCartanSubalgebra (engel K x) :=
by
obtain ⟨x, hx⟩ := exists_isRegular_of_finrank_le_card K L h
use x
refine ⟨?_, normalizer_engel _ _⟩
apply isNilpotent_of_forall_le_engel
intro y hy
set Ex : {engel K z | z ∈ engel K x} := ⟨engel K x, x, self_mem_engel _ _, rfl⟩
suffices IsBot Ex from @this ⟨engel K y, y, hy, rfl⟩
apply engel_isBot_of_isMin h (engel K x) Ex le_rfl
rintro ⟨_, y, hy, rfl⟩ hyx
suffices finrank K (engel K x) ≤ finrank K (engel K y)
by
suffices engel K y = engel K x from this.ge
apply LieSubalgebra.toSubmodule_injective
exact Submodule.eq_of_le_of_finrank_le hyx this
rw [(isRegular_iff_finrank_engel_eq_rank K x).mp hx]
apply rank_le_finrank_engel
