Existence of Cartan subalgebras

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

Main results

• exists_isCartanSubalgebra_of_finrank_le_card: A Lie algebra L over a field K has a Cartan subalgebra, provided that the dimension of L over K is less than or equal to the cardinality of K.
• exists_isCartanSubalgebra: A finite-dimensional Lie algebra L over an infinite field K has a Cartan subalgebra.

References

• [barnes1967]: "On Cartan subalgebras of Lie algebras" by D.W. Barnes.

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 [barnes1967].

theorem LieAlgebra.engel_isBot_of_isMin.lieCharpoly_monic (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) : (LieAlgebra.engel_isBot_of_isMin.lieCharpoly R M x y).Monic

theorem LieAlgebra.engel_isBot_of_isMin.lieCharpoly_natDegree (R : Type u_2) {L : Type u_3} (M : Type u_4) [CommRing R] [Nontrivial 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) : (LieAlgebra.engel_isBot_of_isMin.lieCharpoly R M x y).natDegree = FiniteDimensional.finrank R M

theorem LieAlgebra.engel_isBot_of_isMin.lieCharpoly_map_eval {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) (r : R) : Polynomial.map (Polynomial.evalRingHom r) (LieAlgebra.engel_isBot_of_isMin.lieCharpoly R M x y) = LinearMap.charpoly ((LieModule.toEnd R L M) (r • y + x))

theorem LieAlgebra.engel_isBot_of_isMin.lieCharpoly_coeff_natDegree (R : Type u_2) {L : Type u_3} (M : Type u_4) [CommRing R] [Nontrivial 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) (i : ℕ) (j : ℕ) (hij : i + j = FiniteDimensional.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 : ↑(FiniteDimensional.finrank K L) ≤ Cardinal.mk K) (U : LieSubalgebra K L) (E : ↑{x : LieSubalgebra K L | ∃ x_1 ∈ U, LieSubalgebra.engel K x_1 = x}) (hUle : U ≤ ↑E) (hmin : IsMin E) : IsBot 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 [barnes1967].

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 : ↑(FiniteDimensional.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