Documentation

Mathlib.Algebra.Lie.CartanExists

Existence of Cartan subalgebras #

In this file we prove existence of Cartan subalgebras in finite-dimensional Lie algebras, following [Bar67].

Main results #

References #

Implementation details for the proof of LieAlgebra.engel_isBot_of_isMin #

In this section we provide some auxiliary definitions and lemmas that are used in the proof of LieAlgebra.engel_isBot_of_isMin, which is the following statement:

Let L be a Lie algebra of dimension n over a field K with at least n elements. Given a Lie subalgebra U of L, and an element x ∈ U such that U ≤ engel K x. Suppose that engel K x is minimal amongst the Engel subalgebras engel K y for y ∈ U. Then engel K x ≤ engel K y for all y ∈ U.

We follow the proof strategy of Lemma 2 in [Bar67].

theorem LieAlgebra.engel_isBot_of_isMin.lieCharpoly_coeff_natDegree (R : Type u_2) {L : Type u_3} (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [Module.Finite R L] [Module.Free R L] [Module.Finite R M] [Module.Free R M] (x : L) (y : L) [Nontrivial R] (i : ) (j : ) (hij : i + j = Module.finrank R M) :
((LieAlgebra.engel_isBot_of_isMin.lieCharpoly R M x y).coeff i).natDegree j
theorem LieAlgebra.engel_isBot_of_isMin {K : Type u_1} {L : Type u_2} [Field K] [LieRing L] [LieAlgebra K L] [Module.Finite K L] (hLK : (Module.finrank K L) Cardinal.mk K) (U : LieSubalgebra K L) (E : {x : LieSubalgebra K L | x_1U, LieSubalgebra.engel K x_1 = x}) (hUle : U E) (hmin : IsMin E) :

Let L be a Lie algebra of dimension n over a field K with at least n elements. Given a Lie subalgebra U of L, and an element x ∈ U such that U ≤ engel K x. Suppose that engel K x is minimal amongst the Engel subalgebras engel K y for y ∈ U. Then engel K x ≤ engel K y for all y ∈ U.

Lemma 2 in [Bar67].

theorem LieAlgebra.exists_isCartanSubalgebra_engel_of_finrank_le_card (K : Type u_1) (L : Type u_2) [Field K] [LieRing L] [LieAlgebra K L] [Module.Finite K L] (h : (Module.finrank K L) Cardinal.mk K) :
∃ (x : L), (LieSubalgebra.engel K x).IsCartanSubalgebra
theorem LieAlgebra.exists_isCartanSubalgebra_engel (K : Type u_1) (L : Type u_2) [Field K] [LieRing L] [LieAlgebra K L] [Module.Finite K L] [Infinite K] :
∃ (x : L), (LieSubalgebra.engel K x).IsCartanSubalgebra