A Cartan subalgebra contains a generic element

Let L be a finite-dimensional Lie algebra over an infinite field, and let H be a Cartan subalgebra whose action on L is triangularizable with linear weights. This file chooses an element h : H on which no root vanishes and proves that its Engel subalgebra is exactly H. Mathlib's lower bound on the dimension of each Engel subalgebra then gives

LieAlgebra.rank K L ≤ Module.finrank K H.

The construction has two ingredients. First, finitely many nonzero linear functionals cannot cover a vector space over an infinite field, so there is an h outside every root hyperplane. Second, the generalized Cartan weight spaces span L. The generalized zero eigenspace of ad h therefore receives only the zero weight space: every nonzero weight is a root, and its value at h is nonzero by construction. The zero root space is the Cartan subalgebra.

Main results

• TauCeti.exists_forall_root_apply_ne_zero: some element of H is nonzero under every root.
• TauCeti.engel_eq_cartan_of_forall_root_apply_ne_zero: any such element has Engel subalgebra H.
• TauCeti.exists_engel_eq_cartan: a Cartan subalgebra is the Engel subalgebra of one of its elements.
• TauCeti.rank_le_finrank_cartan: the rank of L is at most the dimension of H.

This is a direct prerequisite for the Layer 9 target rank_eq_finrank_cartan in TauCetiRoadmap/RepresentationTheory/SpinRepresentations/Suggested.lean. It supplies only the rank ≤ dim H direction. The reverse inequality needs a separate minimal-centralizer or Cartan-dimension argument and is deliberately not asserted here.

References

• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, Springer GTM 9 (1972), §15.1--15.3.

theorem TauCeti.exists_forall_root_apply_ne_zero {K : Type u_1} {L : Type u_2} [Field K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] (H : LieSubalgebra K L) [H.IsCartanSubalgebra] [Infinite K] [LieModule.LinearWeights K (↥H) L] : ∃ (h : ↥H), ∀ α ∈ LieSubalgebra.root, α h ≠ 0

A generic element of a Cartan subalgebra avoids every root hyperplane. Since the root set is finite and each root is a nonzero linear functional, finite hyperplane avoidance over the infinite field K supplies one h : H on which every root is nonzero.

theorem TauCeti.engel_eq_cartan_of_forall_root_apply_ne_zero {K : Type u_1} {L : Type u_2} [Field K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] (H : LieSubalgebra K L) [H.IsCartanSubalgebra] {h : ↥H} [LieModule.IsTriangularizable K (↥H) L] (hh : ∀ α ∈ LieSubalgebra.root, α h ≠ 0) : LieSubalgebra.engel K ↑h = H

A root-regular Cartan element has Engel subalgebra equal to the Cartan subalgebra. The Engel subalgebra is the generalized zero eigenspace of ad h. Decomposing that eigenspace into Cartan weight spaces leaves only the zero weight: a nonzero weight is a root, and hence does not vanish at h by hypothesis.

theorem TauCeti.exists_engel_eq_cartan {K : Type u_1} {L : Type u_2} [Field K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] (H : LieSubalgebra K L) [H.IsCartanSubalgebra] [Infinite K] [LieModule.LinearWeights K (↥H) L] [LieModule.IsTriangularizable K (↥H) L] : ∃ (h : ↥H), LieSubalgebra.engel K ↑h = H

Every Cartan subalgebra is the Engel subalgebra of one of its elements when its action has linear weights and is triangularizable over an infinite field.

theorem TauCeti.rank_le_finrank_cartan {K : Type u_1} {L : Type u_2} [Field K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] (H : LieSubalgebra K L) [H.IsCartanSubalgebra] [Infinite K] [LieModule.LinearWeights K (↥H) L] [LieModule.IsTriangularizable K (↥H) L] : LieAlgebra.rank K L ≤ Module.finrank K ↥H

The rank is at most the dimension of a Cartan subalgebra. Choose a root-regular Cartan element whose Engel subalgebra is H, then apply Mathlib's Engel-subalgebra dimension bound LieAlgebra.rank_le_finrank_engel.