Regular elements by minimal centralizer dimension

An element x of a Lie algebra L over a field K is regular when its centralizer ker (ad x) has the smallest dimension among the centralizers of all elements of L (LieAlgebra.IsCentralizerRegular). For a semisimple Lie algebra over an algebraically closed field of characteristic zero this minimal dimension is the rank, and the regular elements include both the regular semisimple elements and the regular nilpotent ones. If L is the Lie algebra of an affine algebraic group G over a field of characteristic zero, the centralizer C_G(x) is smooth with Lie algebra ker (ad x), so these are also the elements whose group centralizer has minimal dimension.

This notion differs from Mathlib's LieAlgebra.IsRegular, which is stated for L finite free over a commutative ring R. There the coefficients of the characteristic polynomial of ad x are polynomial functions of x, LieAlgebra.rank R L is the least index of a coefficient that is not the zero polynomial, and x is regular when the coefficient of index LieAlgebra.rank R L of the characteristic polynomial of ad x is nonzero. Over a field such an element has an Engel subalgebra, the generalized 0-eigenspace of ad x, of minimal dimension (LieAlgebra.isRegular_iff_finrank_engel_eq_rank and LieAlgebra.rank_le_finrank_engel), and over an infinite field the converse holds as well (LieAlgebra.exists_isRegular). Over a finite field the converse can fail, since there may be no element regular in Mathlib's sense at all. So minimal centralizer dimension, Mathlib's characteristic-polynomial condition and minimal Engel dimension are three notions of regularity that differ in general. No nilpotent element of a nonzero semisimple Lie algebra is regular in Mathlib's sense, while the regular nilpotent elements are regular in the sense of this file.

Dimensions are measured by the cardinal Module.rank, so the notion is meaningful also when L is infinite-dimensional; in finite dimension it is the minimality of finrank K (ker (ad x)) (LieAlgebra.isCentralizerRegular_iff_forall_finrank_ker_le).

Regular elements exist, and two regular elements have centralizers of the same dimension, so in finite dimension regularity is the lower bound rank (ad x₀) ≤ rank (ad x) for any one regular element x₀. In the coordinates of a basis of a finite-dimensional L this bound is a Zariski-open condition, since it asks for a nonzero minor of the matrix of ad x, whose entries are linear in the coordinates of x. Over an infinite field the regular elements therefore form a nonempty Zariski-open and Zariski-dense subset of L. Regularity is preserved by Lie algebra isomorphisms, hence by the adjoint action, and by nonzero scalars. In finite dimension the element 0 is regular only when L is abelian.

Main definitions

• LieAlgebra.IsCentralizerRegular K x: the centralizer ker (ad x) has minimal dimension.

Main results

• LieAlgebra.exists_isCentralizerRegular: regular elements exist.
• LieAlgebra.IsCentralizerRegular.isCentralizerRegular_iff_rank_ker_le: an element is regular exactly when its centralizer is no larger than that of a given regular element.
• LieAlgebra.isCentralizerRegular_iff_forall_finrank_ker_le: in finite dimension, regularity is minimality of finrank K (ker (ad x)).
• LieAlgebra.isCentralizerRegular_iff_forall_finrank_range_le: in finite dimension, an element is regular exactly when ad x has maximal rank.
• LieEquiv.isCentralizerRegular_apply_iff and LieAlgebra.isCentralizerRegular_smul_iff: invariance under Lie algebra isomorphisms and nonzero scalars.
• LieAlgebra.isCentralizerRegular_zero_iff: in finite dimension, 0 is regular exactly when L is abelian.
• Module.Basis.not_isCentralizerRegular_of_mem_zeroLocus_vanishingIdeal: the nonregular elements form a Zariski-closed set.
• Module.Basis.vanishingIdeal_setOfPred_isCentralizerRegular_eq_bot: over an infinite field the regular elements are Zariski dense.

References

• B. Kostant, Lie group representations on polynomial rings, Amer. J. Math. 85 (1963), 327–404.
• D. H. Collingwood and W. M. McGovern, Nilpotent Orbits in Semisimple Lie Algebras, Van Nostrand Reinhold, 1993, Chapter 4.

def LieAlgebra.IsCentralizerRegular (K : Type u_1) {L : Type u} [Field K] [LieRing L] [LieAlgebra K L] (x : L) : Prop

An element x of a Lie algebra is regular when its centralizer ker (ad x) has minimal dimension among the centralizers of all elements. The dimension is the cardinal Module.rank, so that an infinite-dimensional centralizer is never smaller than a finite-dimensional one. Over a field of characteristic zero this is the dimension of the group centralizer C_G(x) when the Lie algebra is that of an affine algebraic group G. This differs from Mathlib's LieAlgebra.IsRegular, which asks that the coefficient of index LieAlgebra.rank of the characteristic polynomial of ad x be nonzero, and from minimality of the dimension of the Engel subalgebra, the generalized 0-eigenspace of ad x.

theorem LieAlgebra.isCentralizerRegular_iff {K : Type u_1} {L : Type u} [Field K] [LieRing L] [LieAlgebra K L] {x : L} : IsCentralizerRegular K x ↔ ∀ (y : L), Module.rank K ↥(LinearMap.ker ((ad K L) x)) ≤ Module.rank K ↥(LinearMap.ker ((ad K L) y))

Unfold LieAlgebra.IsCentralizerRegular.

theorem LieAlgebra.isCentralizerRegular_iff_forall_finrank_ker_le {K : Type u_1} {L : Type u} [Field K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] {x : L} : IsCentralizerRegular K x ↔ ∀ (y : L), Module.finrank K ↥(LinearMap.ker ((ad K L) x)) ≤ Module.finrank K ↥(LinearMap.ker ((ad K L) y))

In finite dimension, an element is regular exactly when finrank K (ker (ad x)) is minimal.

theorem LieAlgebra.exists_isCentralizerRegular (K : Type u_1) (L : Type u) [Field K] [LieRing L] [LieAlgebra K L] : ∃ (x : L), IsCentralizerRegular K x

Every Lie algebra has a regular element.

theorem LieAlgebra.IsCentralizerRegular.rank_ker_eq {K : Type u_1} {L : Type u} [Field K] [LieRing L] [LieAlgebra K L] {x y : L} (hx : IsCentralizerRegular K x) (hy : IsCentralizerRegular K y) : Module.rank K ↥(LinearMap.ker ((ad K L) x)) = Module.rank K ↥(LinearMap.ker ((ad K L) y))

Two regular elements have centralizers of the same dimension.

theorem LieAlgebra.IsCentralizerRegular.finrank_ker_eq {K : Type u_1} {L : Type u} [Field K] [LieRing L] [LieAlgebra K L] {x y : L} (hx : IsCentralizerRegular K x) (hy : IsCentralizerRegular K y) : Module.finrank K ↥(LinearMap.ker ((ad K L) x)) = Module.finrank K ↥(LinearMap.ker ((ad K L) y))

Two regular elements have centralizers with the same Module.finrank.

theorem LieAlgebra.IsCentralizerRegular.isCentralizerRegular_iff_rank_ker_le {K : Type u_1} {L : Type u} [Field K] [LieRing L] [LieAlgebra K L] {x₀ : L} (hx₀ : IsCentralizerRegular K x₀) {x : L} : IsCentralizerRegular K x ↔ Module.rank K ↥(LinearMap.ker ((ad K L) x)) ≤ Module.rank K ↥(LinearMap.ker ((ad K L) x₀))

Given one regular element x₀, an element is regular exactly when its centralizer is no larger than that of x₀.

theorem LieAlgebra.isCentralizerRegular_iff_forall_finrank_range_le {K : Type u_1} {L : Type u} [Field K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] {x : L} : IsCentralizerRegular K x ↔ ∀ (y : L), Module.finrank K ↥(LinearMap.range ((ad K L) y)) ≤ Module.finrank K ↥(LinearMap.range ((ad K L) x))

In finite dimension, an element x is regular exactly when ad x has maximal rank.

theorem LieAlgebra.IsCentralizerRegular.isCentralizerRegular_iff_finrank_range_le {K : Type u_1} {L : Type u} [Field K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] {x₀ : L} (hx₀ : IsCentralizerRegular K x₀) {x : L} : IsCentralizerRegular K x ↔ Module.finrank K ↥(LinearMap.range ((ad K L) x₀)) ≤ Module.finrank K ↥(LinearMap.range ((ad K L) x))

Given one regular element x₀ of a finite-dimensional Lie algebra, an element x is regular exactly when ad x has rank at least that of ad x₀.

@[simp]

theorem LieAlgebra.isCentralizerRegular_smul_iff {K : Type u_1} {L : Type u} [Field K] [LieRing L] [LieAlgebra K L] {c : K} (hc : c ≠ 0) {x : L} : IsCentralizerRegular K (c • x) ↔ IsCentralizerRegular K x

Regularity is invariant under multiplication by a nonzero scalar.

@[simp]

theorem LieAlgebra.isCentralizerRegular_zero_iff {K : Type u_1} {L : Type u} [Field K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] : IsCentralizerRegular K 0 ↔ IsLieAbelian L

In finite dimension, 0 is regular exactly in an abelian Lie algebra. In a finite-dimensional Lie algebra the centralizer of 0 is everything, so 0 is regular exactly when every centralizer is everything.

theorem LieAlgebra.isCentralizerRegular_of_isLieAbelian {K : Type u_1} {L : Type u} [Field K] [LieRing L] [LieAlgebra K L] [IsLieAbelian L] (x : L) : IsCentralizerRegular K x

In an abelian Lie algebra every element is regular.

Zariski openness and density

theorem Module.Basis.not_isCentralizerRegular_of_mem_zeroLocus_vanishingIdeal {K : Type u_1} {L : Type u_2} [Field K] [LieRing L] [LieAlgebra K L] {ι : Type u_3} [Finite ι] (b : Basis ι K L) {S : Set L} (hS : ∀ y ∈ S, ¬LieAlgebra.IsCentralizerRegular K y) {x : L} (hx : b.equivFun x ∈ MvPolynomial.zeroLocus K (MvPolynomial.vanishingIdeal K (⇑b.equivFun '' S))) : ¬LieAlgebra.IsCentralizerRegular K x

The nonregular elements form a Zariski-closed set. If no element of a set S is regular, then no x whose coordinates lie in the common zero locus of the polynomials vanishing on the coordinates of S is regular.

theorem Module.Basis.vanishingIdeal_setOfPred_isCentralizerRegular_eq_bot {K : Type u_1} {L : Type u_2} [Field K] [LieRing L] [LieAlgebra K L] {ι : Type u_3} [Finite ι] (b : Basis ι K L) [Infinite K] : MvPolynomial.vanishingIdeal K (⇑b.equivFun '' {x : L | LieAlgebra.IsCentralizerRegular K x}) = ⊥

The regular elements are Zariski dense. Over an infinite field, the only polynomial vanishing on the coordinates of every regular element is zero.

Invariance under Lie algebra isomorphisms

@[simp]

theorem LieEquiv.finrank_range_ad_apply {K : Type u_1} {L : Type u} {L' : Type v} [Field K] [LieRing L] [LieAlgebra K L] [LieRing L'] [LieAlgebra K L'] (e : L ≃ₗ⁅K⁆ L') (x : L) : Module.finrank K ↥(LinearMap.range ((LieAlgebra.ad K L') (e x))) = Module.finrank K ↥(LinearMap.range ((LieAlgebra.ad K L) x))

The adjoint endomorphisms of corresponding elements under a Lie algebra isomorphism have ranges of the same dimension, even for infinite-dimensional Lie algebras.

@[simp]

theorem LieEquiv.isCentralizerRegular_apply_iff {K : Type u_1} {L : Type u} {L' : Type v} [Field K] [LieRing L] [LieAlgebra K L] [LieRing L'] [LieAlgebra K L'] (e : L ≃ₗ⁅K⁆ L') {x : L} : LieAlgebra.IsCentralizerRegular K (e x) ↔ LieAlgebra.IsCentralizerRegular K x

Regularity is invariant under Lie algebra isomorphisms, in particular under the adjoint action of a group acting by Lie algebra automorphisms.