# Nilpotent Lie algebras #

Like groups, Lie algebras admit a natural concept of nilpotency. More generally, any Lie module carries a natural concept of nilpotency. We define these here via the lower central series.

## Main definitions #

• LieModule.lowerCentralSeries
• LieModule.IsNilpotent

## Tags #

lie algebra, lower central series, nilpotent

def LieSubmodule.lcs {R : Type u} {L : Type v} {M : Type w} [] [] [] [] [Module R M] [] (k : ) :
LieSubmodule R L MLieSubmodule R L M

A generalisation of the lower central series. The zeroth term is a specified Lie submodule of a Lie module. In the case when we specify the top ideal ⊤ of the Lie algebra, regarded as a Lie module over itself, we get the usual lower central series of a Lie algebra.

It can be more convenient to work with this generalisation when considering the lower central series of a Lie submodule, regarded as a Lie module in its own right, since it provides a type-theoretic expression of the fact that the terms of the Lie submodule's lower central series are also Lie submodules of the enclosing Lie module.

See also LieSubmodule.lowerCentralSeries_eq_lcs_comap and LieSubmodule.lowerCentralSeries_map_eq_lcs below, as well as LieSubmodule.ucs.

Equations
Instances For
@[simp]
theorem LieSubmodule.lcs_zero {R : Type u} {L : Type v} {M : Type w} [] [] [] [] [Module R M] [] (N : LieSubmodule R L M) :
= N
@[simp]
theorem LieSubmodule.lcs_succ {R : Type u} {L : Type v} {M : Type w} [] [] [] [] [Module R M] [] (k : ) (N : LieSubmodule R L M) :
@[simp]
theorem LieSubmodule.lcs_sup {R : Type u} {L : Type v} {M : Type w} [] [] [] [] [Module R M] [] {N₁ : LieSubmodule R L M} {N₂ : LieSubmodule R L M} {k : } :
LieSubmodule.lcs k (N₁ N₂) =
def LieModule.lowerCentralSeries (R : Type u) (L : Type v) (M : Type w) [] [] [] [] [Module R M] [] (k : ) :

The lower central series of Lie submodules of a Lie module.

Equations
Instances For
@[simp]
theorem LieModule.lowerCentralSeries_zero (R : Type u) (L : Type v) (M : Type w) [] [] [] [] [Module R M] [] :
@[simp]
theorem LieModule.lowerCentralSeries_succ (R : Type u) (L : Type v) (M : Type w) [] [] [] [] [Module R M] [] (k : ) :
theorem LieSubmodule.lcs_le_self {R : Type u} {L : Type v} {M : Type w} [] [] [] [] [Module R M] [] (k : ) (N : LieSubmodule R L M) :
N
theorem LieSubmodule.lowerCentralSeries_eq_lcs_comap {R : Type u} {L : Type v} {M : Type w} [] [] [] [] [Module R M] [] [LieModule R L M] (k : ) (N : LieSubmodule R L M) :
theorem LieSubmodule.lowerCentralSeries_map_eq_lcs {R : Type u} {L : Type v} {M : Type w} [] [] [] [] [Module R M] [] [LieModule R L M] (k : ) (N : LieSubmodule R L M) :
theorem LieModule.antitone_lowerCentralSeries (R : Type u) (L : Type v) (M : Type w) [] [] [] [] [Module R M] [] :
theorem LieModule.eventually_iInf_lowerCentralSeries_eq (R : Type u) (L : Type v) (M : Type w) [] [] [] [] [Module R M] [] [] :
∀ᶠ (l : ) in Filter.atTop, ⨅ (k : ), =
theorem LieModule.trivial_iff_lower_central_eq_bot (R : Type u) (L : Type v) (M : Type w) [] [] [] [] [Module R M] [] :
theorem LieModule.iterate_toEndomorphism_mem_lowerCentralSeries (R : Type u) (L : Type v) (M : Type w) [] [] [] [] [Module R M] [] [LieModule R L M] (x : L) (m : M) (k : ) :
((() x))^[k] m
theorem LieModule.iterate_toEndomorphism_mem_lowerCentralSeries₂ (R : Type u) (L : Type v) (M : Type w) [] [] [] [] [Module R M] [] [LieModule R L M] (x : L) (y : L) (m : M) (k : ) :
((() x ∘ₗ () y))^[k] m LieModule.lowerCentralSeries R L M (2 * k)
theorem LieModule.map_lowerCentralSeries_le {R : Type u} {L : Type v} {M : Type w} [] [] [] [] [Module R M] [] [LieModule R L M] (k : ) {M₂ : Type w₁} [] [Module R M₂] [] [LieModule R L M₂] (f : M →ₗ⁅R,L M₂) :
theorem LieModule.map_lowerCentralSeries_eq {R : Type u} {L : Type v} {M : Type w} [] [] [] [] [Module R M] [] [LieModule R L M] (k : ) {M₂ : Type w₁} [] [Module R M₂] [] [LieModule R L M₂] {f : M →ₗ⁅R,L M₂} (hf : ) :
theorem LieModule.derivedSeries_le_lowerCentralSeries (R : Type u) (L : Type v) [] [] [] (k : ) :
class LieModule.IsNilpotent (R : Type u) (L : Type v) (M : Type w) [] [] [] [] [Module R M] [] :

A Lie module is nilpotent if its lower central series reaches 0 (in a finite number of steps).

Instances
theorem LieModule.IsNilpotent.nilpotent {R : Type u} {L : Type v} {M : Type w} [] [] [] [] [Module R M] [] [self : ] :
∃ (k : ), =
theorem LieModule.exists_lowerCentralSeries_eq_bot_of_isNilpotent (R : Type u) (L : Type v) (M : Type w) [] [] [] [] [Module R M] [] [] :
∃ (k : ), =
@[simp]
theorem LieModule.iInf_lowerCentralSeries_eq_bot_of_isNilpotent (R : Type u) (L : Type v) (M : Type w) [] [] [] [] [Module R M] [] [] :
⨅ (k : ), =
theorem LieModule.isNilpotent_iff (R : Type u) (L : Type v) (M : Type w) [] [] [] [] [Module R M] [] :
∃ (k : ), =

See also LieModule.isNilpotent_iff_exists_ucs_eq_top.

theorem LieSubmodule.isNilpotent_iff_exists_lcs_eq_bot {R : Type u} {L : Type v} {M : Type w} [] [] [] [] [Module R M] [] [LieModule R L M] (N : LieSubmodule R L M) :
∃ (k : ),
@[instance 100]
instance LieModule.trivialIsNilpotent (R : Type u) (L : Type v) (M : Type w) [] [] [] [] [Module R M] [] [] :
Equations
• =
theorem LieModule.exists_forall_pow_toEndomorphism_eq_zero (R : Type u) (L : Type v) (M : Type w) [] [] [] [] [Module R M] [] [LieModule R L M] [hM : ] :
∃ (k : ), ∀ (x : L), () x ^ k = 0
theorem LieModule.isNilpotent_toEndomorphism_of_isNilpotent (R : Type u) (L : Type v) (M : Type w) [] [] [] [] [Module R M] [] [LieModule R L M] [] (x : L) :
theorem LieModule.isNilpotent_toEndomorphism_of_isNilpotent₂ (R : Type u) (L : Type v) (M : Type w) [] [] [] [] [Module R M] [] [LieModule R L M] [] (x : L) (y : L) :
IsNilpotent (() x ∘ₗ () y)
@[simp]
theorem LieModule.maxGenEigenSpace_toEndomorphism_eq_top (R : Type u) (L : Type v) (M : Type w) [] [] [] [] [Module R M] [] [LieModule R L M] [] (x : L) :
(() x).maximalGeneralizedEigenspace 0 =
theorem LieModule.nilpotentOfNilpotentQuotient (R : Type u) (L : Type v) (M : Type w) [] [] [] [] [Module R M] [] [LieModule R L M] {N : LieSubmodule R L M} (h₁ : N ) (h₂ : LieModule.IsNilpotent R L (M N)) :

If the quotient of a Lie module M by a Lie submodule on which the Lie algebra acts trivially is nilpotent then M is nilpotent.

This is essentially the Lie module equivalent of the fact that a central extension of nilpotent Lie algebras is nilpotent. See LieAlgebra.nilpotent_of_nilpotent_quotient below for the corresponding result for Lie algebras.

theorem LieModule.isNilpotent_quotient_iff (R : Type u) (L : Type v) (M : Type w) [] [] [] [] [Module R M] [] [LieModule R L M] (N : LieSubmodule R L M) :
LieModule.IsNilpotent R L (M N) ∃ (k : ), N
theorem LieModule.iInf_lcs_le_of_isNilpotent_quot (R : Type u) (L : Type v) (M : Type w) [] [] [] [] [Module R M] [] [LieModule R L M] (N : LieSubmodule R L M) (h : LieModule.IsNilpotent R L (M N)) :
⨅ (k : ), N
noncomputable def LieModule.nilpotencyLength (R : Type u) (L : Type v) (M : Type w) [] [] [] [] [Module R M] [] :

Given a nilpotent Lie module M with lower central series M = C₀ ≥ C₁ ≥ ⋯ ≥ Cₖ = ⊥, this is the natural number k (the number of inclusions).

For a non-nilpotent module, we use the junk value 0.

Equations
Instances For
@[simp]
theorem LieModule.nilpotencyLength_eq_zero_iff (R : Type u) (L : Type v) (M : Type w) [] [] [] [] [Module R M] [] [] :
= 0
theorem LieModule.nilpotencyLength_eq_succ_iff (R : Type u) (L : Type v) (M : Type w) [] [] [] [] [Module R M] [] (k : ) :
@[simp]
theorem LieModule.nilpotencyLength_eq_one_iff (R : Type u) (L : Type v) (M : Type w) [] [] [] [] [Module R M] [] [] :
= 1
theorem LieModule.isTrivial_of_nilpotencyLength_le_one (R : Type u) (L : Type v) (M : Type w) [] [] [] [] [Module R M] [] [] (h : 1) :
noncomputable def LieModule.lowerCentralSeriesLast (R : Type u) (L : Type v) (M : Type w) [] [] [] [] [Module R M] [] :

Given a non-trivial nilpotent Lie module M with lower central series M = C₀ ≥ C₁ ≥ ⋯ ≥ Cₖ = ⊥, this is the k-1th term in the lower central series (the last non-trivial term).

For a trivial or non-nilpotent module, this is the bottom submodule, ⊥.

Equations
• = match with | 0 => | k.succ =>
Instances For
theorem LieModule.lowerCentralSeriesLast_le_max_triv (R : Type u) (L : Type v) (M : Type w) [] [] [] [] [Module R M] [] [LieModule R L M] :
theorem LieModule.nontrivial_lowerCentralSeriesLast (R : Type u) (L : Type v) (M : Type w) [] [] [] [] [Module R M] [] [] [] :
theorem LieModule.lowerCentralSeriesLast_le_of_not_isTrivial (R : Type u) (L : Type v) (M : Type w) [] [] [] [] [Module R M] [] [] (h : ) :
theorem LieModule.disjoint_lowerCentralSeries_maxTrivSubmodule_iff (R : Type u) (L : Type v) (M : Type w) [] [] [] [] [Module R M] [] [LieModule R L M] [] :
Disjoint () ()

For a nilpotent Lie module M of a Lie algebra L, the first term in the lower central series of M contains a non-zero element on which L acts trivially unless the entire action is trivial.

Taking M = L, this provides a useful characterisation of Abelian-ness for nilpotent Lie algebras.

theorem LieModule.nontrivial_max_triv_of_isNilpotent (R : Type u) (L : Type v) (M : Type w) [] [] [] [] [Module R M] [] [LieModule R L M] [] [] :
Nontrivial ()
@[simp]
theorem LieModule.coe_lcs_range_toEndomorphism_eq (R : Type u) (L : Type v) (M : Type w) [] [] [] [] [Module R M] [] [LieModule R L M] (k : ) :
(LieModule.lowerCentralSeries R (().range) M k) = ()
@[simp]
theorem LieModule.isNilpotent_range_toEndomorphism_iff (R : Type u) (L : Type v) (M : Type w) [] [] [] [] [Module R M] [] [LieModule R L M] :
LieModule.IsNilpotent R (().range) M
def LieSubmodule.ucs {R : Type u} {L : Type v} {M : Type w} [] [] [] [] [Module R M] [] [LieModule R L M] (k : ) :
LieSubmodule R L MLieSubmodule R L M

The upper (aka ascending) central series.

See also LieSubmodule.lcs.

Equations
• = LieSubmodule.normalizer^[k]
Instances For
@[simp]
theorem LieSubmodule.ucs_zero {R : Type u} {L : Type v} {M : Type w} [] [] [] [] [Module R M] [] [LieModule R L M] (N : LieSubmodule R L M) :
= N
@[simp]
theorem LieSubmodule.ucs_succ {R : Type u} {L : Type v} {M : Type w} [] [] [] [] [Module R M] [] [LieModule R L M] (N : LieSubmodule R L M) (k : ) :
LieSubmodule.ucs (k + 1) N = ().normalizer
theorem LieSubmodule.ucs_add {R : Type u} {L : Type v} {M : Type w} [] [] [] [] [Module R M] [] [LieModule R L M] (N : LieSubmodule R L M) (k : ) (l : ) :
theorem LieSubmodule.ucs_mono {R : Type u} {L : Type v} {M : Type w} [] [] [] [] [Module R M] [] [LieModule R L M] {N₁ : LieSubmodule R L M} {N₂ : LieSubmodule R L M} (k : ) (h : N₁ N₂) :
theorem LieSubmodule.ucs_eq_self_of_normalizer_eq_self {R : Type u} {L : Type v} {M : Type w} [] [] [] [] [Module R M] [] [LieModule R L M] {N₁ : LieSubmodule R L M} (h : N₁.normalizer = N₁) (k : ) :
= N₁
theorem LieSubmodule.ucs_le_of_normalizer_eq_self {R : Type u} {L : Type v} {M : Type w} [] [] [] [] [Module R M] [] [LieModule R L M] {N₁ : LieSubmodule R L M} (h : N₁.normalizer = N₁) (k : ) :
N₁

If a Lie module M contains a self-normalizing Lie submodule N, then all terms of the upper central series of M are contained in N.

An important instance of this situation arises from a Cartan subalgebra H ⊆ L with the roles of L, M, N played by H, L, H, respectively.

theorem LieSubmodule.lcs_add_le_iff {R : Type u} {L : Type v} {M : Type w} [] [] [] [] [Module R M] [] [LieModule R L M] {N₁ : LieSubmodule R L M} {N₂ : LieSubmodule R L M} (l : ) (k : ) :
LieSubmodule.lcs (l + k) N₁ N₂
theorem LieSubmodule.lcs_le_iff {R : Type u} {L : Type v} {M : Type w} [] [] [] [] [Module R M] [] [LieModule R L M] {N₁ : LieSubmodule R L M} {N₂ : LieSubmodule R L M} (k : ) :
N₂ N₁
theorem LieSubmodule.gc_lcs_ucs {R : Type u} {L : Type v} {M : Type w} [] [] [] [] [Module R M] [] [LieModule R L M] (k : ) :
GaloisConnection (fun (N : LieSubmodule R L M) => ) fun (N : LieSubmodule R L M) =>
theorem LieSubmodule.ucs_eq_top_iff {R : Type u} {L : Type v} {M : Type w} [] [] [] [] [Module R M] [] [LieModule R L M] (N : LieSubmodule R L M) (k : ) :
N
theorem LieModule.isNilpotent_iff_exists_ucs_eq_top {R : Type u} {L : Type v} {M : Type w} [] [] [] [] [Module R M] [] [LieModule R L M] :
∃ (k : ),
theorem LieSubmodule.ucs_comap_incl {R : Type u} {L : Type v} {M : Type w} [] [] [] [] [Module R M] [] [LieModule R L M] (N : LieSubmodule R L M) (k : ) :
theorem LieSubmodule.isNilpotent_iff_exists_self_le_ucs {R : Type u} {L : Type v} {M : Type w} [] [] [] [] [Module R M] [] [LieModule R L M] (N : LieSubmodule R L M) :
∃ (k : ),
theorem LieSubmodule.ucs_bot_one {R : Type u} {L : Type v} {M : Type w} [] [] [] [] [Module R M] [] [LieModule R L M] :
theorem Function.Surjective.lieModule_lcs_map_eq {R : Type u} {L : Type v} {M : Type w} [] [] [] [] [Module R M] [] [LieModule R L M] {L₂ : Type u_1} {M₂ : Type u_2} [LieRing L₂] [LieAlgebra R L₂] [] [Module R M₂] [LieRingModule L₂ M₂] [LieModule R L₂ M₂] {f : L →ₗ⁅R L₂} {g : M →ₗ[R] M₂} (hf : ) (hg : ) (hfg : ∀ (x : L) (m : M), f x, g m = g x, m) (k : ) :
Submodule.map g () = ()
theorem Function.Surjective.lieModuleIsNilpotent {R : Type u} {L : Type v} {M : Type w} [] [] [] [] [Module R M] [] [LieModule R L M] {L₂ : Type u_1} {M₂ : Type u_2} [LieRing L₂] [LieAlgebra R L₂] [] [Module R M₂] [LieRingModule L₂ M₂] [LieModule R L₂ M₂] {f : L →ₗ⁅R L₂} {g : M →ₗ[R] M₂} (hf : ) (hg : ) (hfg : ∀ (x : L) (m : M), f x, g m = g x, m) [] :
theorem Equiv.lieModule_isNilpotent_iff {R : Type u} {L : Type v} {M : Type w} [] [] [] [] [Module R M] [] [LieModule R L M] {L₂ : Type u_1} {M₂ : Type u_2} [LieRing L₂] [LieAlgebra R L₂] [] [Module R M₂] [LieRingModule L₂ M₂] [LieModule R L₂ M₂] (f : L ≃ₗ⁅R L₂) (g : M ≃ₗ[R] M₂) (hfg : ∀ (x : L) (m : M), f x, g m = g x, m) :
@[simp]
theorem LieModule.isNilpotent_of_top_iff {R : Type u} {L : Type v} {M : Type w} [] [] [] [] [Module R M] [] [LieModule R L M] :
@[simp]
theorem LieModule.isNilpotent_of_top_iff' {R : Type u} {L : Type v} {M : Type w} [] [] [] [] [Module R M] [] [LieModule R L M] :
@[instance 100]
instance LieAlgebra.isSolvable_of_isNilpotent (R : Type u) (L : Type v) [] [] [] [hL : ] :
Equations
• =
@[reducible, inline]
abbrev LieAlgebra.IsNilpotent (R : Type u) (L : Type v) [] [] [] :

We say a Lie algebra is nilpotent when it is nilpotent as a Lie module over itself via the adjoint representation.

Equations
Instances For
theorem LieAlgebra.nilpotent_ad_of_nilpotent_algebra (R : Type u) (L : Type v) [] [] [] [] :
∃ (k : ), ∀ (x : L), () x ^ k = 0
theorem coe_lowerCentralSeries_ideal_quot_eq {R : Type u} {L : Type v} [] [] [] {I : LieIdeal R L} (k : ) :

Given an ideal I of a Lie algebra L, the lower central series of L ⧸ I is the same whether we regard L ⧸ I as an L module or an L ⧸ I module.

TODO: This result obviously generalises but the generalisation requires the missing definition of morphisms between Lie modules over different Lie algebras.

theorem LieModule.coe_lowerCentralSeries_ideal_le {R : Type u} {L : Type v} [] [] [] {I : LieIdeal R L} (k : ) :
(LieModule.lowerCentralSeries R (I) (I) k) (LieModule.lowerCentralSeries R L (I) k)

Note that the below inequality can be strict. For example the ideal of strictly-upper-triangular 2x2 matrices inside the Lie algebra of upper-triangular 2x2 matrices with k = 1.

theorem LieAlgebra.nilpotent_of_nilpotent_quotient {R : Type u} {L : Type v} [] [] [] {I : LieIdeal R L} (h₁ : I ) (h₂ : LieAlgebra.IsNilpotent R (L I)) :

A central extension of nilpotent Lie algebras is nilpotent.

theorem LieAlgebra.non_trivial_center_of_isNilpotent {R : Type u} {L : Type v} [] [] [] [] [] :
Nontrivial ()
theorem LieIdeal.map_lowerCentralSeries_le {R : Type u} {L : Type v} {L' : Type w} [] [] [] [LieRing L'] [LieAlgebra R L'] (k : ) {f : L →ₗ⁅R L'} :
theorem LieIdeal.lowerCentralSeries_map_eq {R : Type u} {L : Type v} {L' : Type w} [] [] [] [LieRing L'] [LieAlgebra R L'] (k : ) {f : L →ₗ⁅R L'} (h : ) :
theorem Function.Injective.lieAlgebra_isNilpotent {R : Type u} {L : Type v} {L' : Type w} [] [] [] [LieRing L'] [LieAlgebra R L'] [h₁ : ] {f : L →ₗ⁅R L'} (h₂ : ) :
theorem Function.Surjective.lieAlgebra_isNilpotent {R : Type u} {L : Type v} {L' : Type w} [] [] [] [LieRing L'] [LieAlgebra R L'] [h₁ : ] {f : L →ₗ⁅R L'} (h₂ : ) :
theorem LieEquiv.nilpotent_iff_equiv_nilpotent {R : Type u} {L : Type v} {L' : Type w} [] [] [] [LieRing L'] [LieAlgebra R L'] (e : L ≃ₗ⁅R L') :
theorem LieHom.isNilpotent_range {R : Type u} {L : Type v} {L' : Type w} [] [] [] [LieRing L'] [LieAlgebra R L'] [] (f : L →ₗ⁅R L') :
@[simp]
theorem LieAlgebra.isNilpotent_range_ad_iff {R : Type u} {L : Type v} [] [] [] :

Note that this result is not quite a special case of LieModule.isNilpotent_range_toEndomorphism_iff which concerns nilpotency of the (ad R L).range-module L, whereas this result concerns nilpotency of the (ad R L).range-module (ad R L).range.

instance instIsNilpotentSubtypeMemLieSubalgebraTop {R : Type u} {L : Type v} [] [] [] [h : ] :
Equations
• =
def LieIdeal.lcs {R : Type u_1} {L : Type u_2} [] [] [] (I : LieIdeal R L) (M : Type u_3) [] [Module R M] [] (k : ) :

Given a Lie module M over a Lie algebra L together with an ideal I of L, this is the lower central series of M as an I-module. The advantage of using this definition instead of LieModule.lowerCentralSeries R I M is that its terms are Lie submodules of M as an L-module, rather than just as an I-module.

See also LieIdeal.coe_lcs_eq.

Equations
Instances For
@[simp]
theorem LieIdeal.lcs_zero {R : Type u_1} {L : Type u_2} [] [] [] (I : LieIdeal R L) (M : Type u_3) [] [Module R M] [] :
I.lcs M 0 =
@[simp]
theorem LieIdeal.lcs_succ {R : Type u_1} {L : Type u_2} [] [] [] (I : LieIdeal R L) (M : Type u_3) [] [Module R M] [] (k : ) :
I.lcs M (k + 1) = I, I.lcs M k
theorem LieIdeal.lcs_top {R : Type u_1} {L : Type u_2} [] [] [] (M : Type u_3) [] [Module R M] [] (k : ) :
.lcs M k =
theorem LieIdeal.coe_lcs_eq {R : Type u_1} {L : Type u_2} [] [] [] (I : LieIdeal R L) (M : Type u_3) [] [Module R M] [] [LieModule R L M] (k : ) :
(I.lcs M k) = (LieModule.lowerCentralSeries R (I) M k)
theorem LieAlgebra.ad_nilpotent_of_nilpotent (R : Type u) {A : Type v} [] [Ring A] [Algebra R A] {a : A} (h : ) :
theorem LieSubalgebra.isNilpotent_ad_of_isNilpotent_ad {R : Type u} [] {L : Type v} [] [] (K : ) {x : K} (h : IsNilpotent (() x)) :
theorem LieAlgebra.isNilpotent_ad_of_isNilpotent {R : Type u} {A : Type v} [] [Ring A] [Algebra R A] {L : } {x : L} (h : ) :
@[simp]
theorem LieSubmodule.lowerCentralSeries_tensor_eq_baseChange (R : Type u_1) (A : Type u_2) (L : Type u_3) (M : Type u_4) [] [] [] [] [Module R M] [] [LieModule R L M] [] [Algebra R A] (k : ) :
instance LieModule.instIsNilpotentTensor (R : Type u_1) (A : Type u_2) (L : Type u_3) (M : Type u_4) [] [] [] [] [Module R M] [] [LieModule R L M] [] [Algebra R A] [] :
Equations
• =