Rank of a Lie algebra and regular elements

Let L be a Lie algebra over a nontrivial commutative ring R, and assume that L is finite free as R-module. Then the coefficients of the characteristic polynomial of ad R L x are polynomial in x. The rank of L is the smallest n for which the n-th coefficient is not the zero polynomial.

Continuing to write n for the rank of L, an element x of L is regular if the n-th coefficient of the characteristic polynomial of ad R L x is non-zero.

Main declarations

• LieAlgebra.rank R L is the rank of a Lie algebra L over a commutative ring R.
• LieAlgebra.IsRegular R x is the predicate that an element x of a Lie algebra L is regular.

References

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

noncomputable def LieModule.rank (R : Type u_1) (L : Type u_3) (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [Module.Finite R L] [Module.Free R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [Module.Finite R M] [Module.Free R M] : ℕ

Let M be a representation of a Lie algebra L over a nontrivial commutative ring R, and assume that L and M are finite free as R-module. Then the coefficients of the characteristic polynomial of ⁅x, ·⁆ are polynomial in x. The rank of M is the smallest n for which the n-th coefficient is not the zero polynomial.

theorem LieModule.polyCharpoly_coeff_rank_ne_zero (R : Type u_1) (L : Type u_3) (M : Type u_4) {ι : Type u_5} [CommRing R] [LieRing L] [LieAlgebra R L] [Module.Finite R L] [Module.Free R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [Module.Finite R M] [Module.Free R M] [Fintype ι] (b : Module.Basis ι R L) [Nontrivial R] [DecidableEq ι] : ((↑(toEnd R L M)).polyCharpoly b).coeff (rank R L M) ≠ 0

theorem LieModule.rank_eq_natTrailingDegree (R : Type u_1) (L : Type u_3) (M : Type u_4) {ι : Type u_5} [CommRing R] [LieRing L] [LieAlgebra R L] [Module.Finite R L] [Module.Free R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [Module.Finite R M] [Module.Free R M] [Fintype ι] (b : Module.Basis ι R L) [Nontrivial R] [DecidableEq ι] : rank R L M = ((↑(toEnd R L M)).polyCharpoly b).natTrailingDegree

theorem LieModule.rank_le_card (R : Type u_1) (L : Type u_3) (M : Type u_4) {ιₘ : Type u_6} [CommRing R] [LieRing L] [LieAlgebra R L] [Module.Finite R L] [Module.Free R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [Module.Finite R M] [Module.Free R M] [Fintype ιₘ] (bₘ : Module.Basis ιₘ R M) [Nontrivial R] : rank R L M ≤ Fintype.card ιₘ

theorem LieModule.rank_le_finrank (R : Type u_1) (L : Type u_3) (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [Module.Finite R L] [Module.Free R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [Module.Finite R M] [Module.Free R M] [Nontrivial R] : rank R L M ≤ Module.finrank R M

theorem LieModule.rank_le_natTrailingDegree_charpoly_ad (R : Type u_1) {L : Type u_3} (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [Module.Finite R L] [Module.Free R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [Module.Finite R M] [Module.Free R M] (x : L) [Nontrivial R] : rank R L M ≤ (LinearMap.charpoly ((toEnd R L M) x)).natTrailingDegree

def LieModule.IsRegular (R : Type u_1) {L : Type u_3} (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [Module.Finite R L] [Module.Free R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [Module.Finite R M] [Module.Free R M] (x : L) : Prop

Let x be an element of a Lie algebra L over R, and write n for rank R L. Then x is regular if the n-th coefficient of the characteristic polynomial of ad R L x is non-zero.

theorem LieModule.isRegular_def (R : Type u_1) {L : Type u_3} (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [Module.Finite R L] [Module.Free R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [Module.Finite R M] [Module.Free R M] (x : L) : IsRegular R M x ↔ (LinearMap.charpoly ((toEnd R L M) x)).coeff (rank R L M) ≠ 0

theorem LieModule.isRegular_iff_coeff_polyCharpoly_rank_ne_zero (R : Type u_1) {L : Type u_3} (M : Type u_4) {ι : Type u_5} [CommRing R] [LieRing L] [LieAlgebra R L] [Module.Finite R L] [Module.Free R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [Module.Finite R M] [Module.Free R M] [Fintype ι] (b : Module.Basis ι R L) (x : L) [DecidableEq ι] : IsRegular R M x ↔ (MvPolynomial.eval ⇑(b.repr x)) (((↑(toEnd R L M)).polyCharpoly b).coeff (rank R L M)) ≠ 0

theorem LieModule.isRegular_iff_natTrailingDegree_charpoly_eq_rank (R : Type u_1) {L : Type u_3} (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [Module.Finite R L] [Module.Free R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [Module.Finite R M] [Module.Free R M] (x : L) [Nontrivial R] : IsRegular R M x ↔ (LinearMap.charpoly ((toEnd R L M) x)).natTrailingDegree = rank R L M

theorem LieModule.exists_isRegular_of_finrank_le_card (R : Type u_1) (L : Type u_3) (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [Module.Finite R L] [Module.Free R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [Module.Finite R M] [Module.Free R M] [IsDomain R] (h : ↑(Module.finrank R M) ≤ Cardinal.mk R) : ∃ (x : L), IsRegular R M x

theorem LieModule.exists_isRegular (R : Type u_1) (L : Type u_3) (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [Module.Finite R L] [Module.Free R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [Module.Finite R M] [Module.Free R M] [IsDomain R] [Infinite R] : ∃ (x : L), IsRegular R M x

@[reducible, inline]

noncomputable abbrev LieAlgebra.rank (R : Type u_1) (L : Type u_3) [CommRing R] [LieRing L] [LieAlgebra R L] [Module.Finite R L] [Module.Free R L] : ℕ

Let L be a Lie algebra over a nontrivial commutative ring R, and assume that L is finite free as R-module. Then the coefficients of the characteristic polynomial of ad R L x are polynomial in x. The rank of L is the smallest n for which the n-th coefficient is not the zero polynomial.

theorem LieAlgebra.polyCharpoly_coeff_rank_ne_zero (R : Type u_1) (L : Type u_3) {ι : Type u_5} [CommRing R] [LieRing L] [LieAlgebra R L] [Module.Finite R L] [Module.Free R L] [Fintype ι] (b : Module.Basis ι R L) [Nontrivial R] [DecidableEq ι] : ((↑(ad R L)).polyCharpoly b).coeff (rank R L) ≠ 0

theorem LieAlgebra.rank_eq_natTrailingDegree (R : Type u_1) (L : Type u_3) {ι : Type u_5} [CommRing R] [LieRing L] [LieAlgebra R L] [Module.Finite R L] [Module.Free R L] [Fintype ι] (b : Module.Basis ι R L) [Nontrivial R] [DecidableEq ι] : rank R L = ((↑(ad R L)).polyCharpoly b).natTrailingDegree

theorem LieAlgebra.rank_le_card (R : Type u_1) (L : Type u_3) {ι : Type u_5} [CommRing R] [LieRing L] [LieAlgebra R L] [Module.Finite R L] [Module.Free R L] [Fintype ι] (b : Module.Basis ι R L) [Nontrivial R] : rank R L ≤ Fintype.card ι

theorem LieAlgebra.rank_le_finrank (R : Type u_1) (L : Type u_3) [CommRing R] [LieRing L] [LieAlgebra R L] [Module.Finite R L] [Module.Free R L] [Nontrivial R] : rank R L ≤ Module.finrank R L

theorem LieAlgebra.rank_le_natTrailingDegree_charpoly_ad (R : Type u_1) {L : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [Module.Finite R L] [Module.Free R L] (x : L) [Nontrivial R] : rank R L ≤ (LinearMap.charpoly ((ad R L) x)).natTrailingDegree

@[reducible, inline]

abbrev LieAlgebra.IsRegular (R : Type u_1) {L : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [Module.Finite R L] [Module.Free R L] (x : L) : Prop

Let x be an element of a Lie algebra L over R, and write n for rank R L. Then x is regular if the n-th coefficient of the characteristic polynomial of ad R L x is non-zero.

theorem LieAlgebra.isRegular_def (R : Type u_1) {L : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [Module.Finite R L] [Module.Free R L] (x : L) : IsRegular R x ↔ (LinearMap.charpoly ((ad R L) x)).coeff (rank R L) ≠ 0

theorem LieAlgebra.isRegular_iff_coeff_polyCharpoly_rank_ne_zero (R : Type u_1) {L : Type u_3} {ι : Type u_5} [CommRing R] [LieRing L] [LieAlgebra R L] [Module.Finite R L] [Module.Free R L] [Fintype ι] (b : Module.Basis ι R L) (x : L) [DecidableEq ι] : IsRegular R x ↔ (MvPolynomial.eval ⇑(b.repr x)) (((↑(ad R L)).polyCharpoly b).coeff (rank R L)) ≠ 0

theorem LieAlgebra.isRegular_iff_natTrailingDegree_charpoly_eq_rank (R : Type u_1) {L : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [Module.Finite R L] [Module.Free R L] (x : L) [Nontrivial R] : IsRegular R x ↔ (LinearMap.charpoly ((ad R L) x)).natTrailingDegree = rank R L

theorem LieAlgebra.exists_isRegular_of_finrank_le_card (R : Type u_1) (L : Type u_3) [CommRing R] [LieRing L] [LieAlgebra R L] [Module.Finite R L] [Module.Free R L] [IsDomain R] (h : ↑(Module.finrank R L) ≤ Cardinal.mk R) : ∃ (x : L), IsRegular R x

theorem LieAlgebra.exists_isRegular (R : Type u_1) (L : Type u_3) [CommRing R] [LieRing L] [LieAlgebra R L] [Module.Finite R L] [Module.Free R L] [IsDomain R] [Infinite R] : ∃ (x : L), IsRegular R x

theorem LieAlgebra.finrank_engel (K : Type u_7) {L : Type u_8} [Field K] [LieRing L] [LieAlgebra K L] [Module.Finite K L] (x : L) : Module.finrank K ↥(LieSubalgebra.engel K x) = (LinearMap.charpoly ((ad K L) x)).natTrailingDegree

theorem LieAlgebra.rank_le_finrank_engel (K : Type u_7) {L : Type u_8} [Field K] [LieRing L] [LieAlgebra K L] [Module.Finite K L] (x : L) : rank K L ≤ Module.finrank K ↥(LieSubalgebra.engel K x)

theorem LieAlgebra.isRegular_iff_finrank_engel_eq_rank (K : Type u_7) {L : Type u_8} [Field K] [LieRing L] [LieAlgebra K L] [Module.Finite K L] (x : L) : IsRegular K x ↔ Module.finrank K ↥(LieSubalgebra.engel K x) = rank K L