# mathlibdocumentation

algebra.lie.nilpotent

# 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 #

• lie_module.lower_central_series
• lie_module.is_nilpotent

## Tags #

lie algebra, lower central series, nilpotent

def lie_submodule.lcs {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] (k : ) :
M 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 lie_module.lower_central_series_eq_lcs_comap and lie_module.lower_central_series_map_eq_lcs below, as well as lie_submodule.ucs.

Equations
@[simp]
theorem lie_submodule.lcs_zero {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] (N : M) :
= N
@[simp]
theorem lie_submodule.lcs_succ {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] (k : ) (N : M) :
def lie_module.lower_central_series (R : Type u) (L : Type v) (M : Type w) [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] (k : ) :
M

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

Equations
@[simp]
theorem lie_module.lower_central_series_zero (R : Type u) (L : Type v) (M : Type w) [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] :
@[simp]
theorem lie_module.lower_central_series_succ (R : Type u) (L : Type v) (M : Type w) [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] (k : ) :
(k + 1) =
theorem lie_submodule.lcs_le_self {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] (k : ) (N : M) :
N
theorem lie_submodule.lower_central_series_eq_lcs_comap {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] (k : ) (N : M) :
theorem lie_submodule.lower_central_series_map_eq_lcs {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] (k : ) (N : M) :
=
theorem lie_module.antitone_lower_central_series (R : Type u) (L : Type v) (M : Type w) [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] :
theorem lie_module.trivial_iff_lower_central_eq_bot (R : Type u) (L : Type v) (M : Type w) [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] :
theorem lie_module.iterate_to_endomorphism_mem_lower_central_series (R : Type u) (L : Type v) (M : Type w) [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] (x : L) (m : M) (k : ) :
( M) x)^[k] m
theorem lie_module.map_lower_central_series_le {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] {M₂ : Type w₁} [add_comm_group M₂] [ M₂] [ M₂] [ L M₂] (k : ) (f : M →ₗ⁅R,L M₂) :
k) k
theorem lie_module.derived_series_le_lower_central_series (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [ L] (k : ) :
@[class]
structure lie_module.is_nilpotent (R : Type u) (L : Type v) (M : Type w) [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] :
Prop
• nilpotent : ∃ (k : ),

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

Instances of this typeclass
theorem lie_module.is_nilpotent_iff (R : Type u) (L : Type v) (M : Type w) [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] :
∃ (k : ),

See also lie_module.is_nilpotent_iff_exists_ucs_eq_top.

theorem lie_submodule.is_nilpotent_iff_exists_lcs_eq_bot {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] (N : M) :
∃ (k : ),
@[protected, instance]
def lie_module.trivial_is_nilpotent (R : Type u) (L : Type v) (M : Type w) [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M]  :
theorem lie_module.nilpotent_endo_of_nilpotent_module (R : Type u) (L : Type v) (M : Type w) [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] [hM : M] :
∃ (k : ), ∀ (x : L), M) x ^ k = 0
theorem lie_module.infi_max_gen_zero_eigenspace_eq_top_of_nilpotent (R : Type u) (L : Type v) (M : Type w) [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] [ M] :
(⨅ (x : L), 0) =

For a nilpotent Lie module, the weight space of the 0 weight is the whole module.

This result will be used downstream to show that weight spaces are Lie submodules, at which time it will be possible to state it in the language of weight spaces.

theorem lie_module.nilpotent_of_nilpotent_quotient (R : Type u) (L : Type v) (M : Type w) [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] {N : M} (h₁ : N ) (h₂ : (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 lie_algebra.nilpotent_of_nilpotent_quotient below for the corresponding result for Lie algebras.

noncomputable def lie_module.nilpotency_length (R : Type u) (L : Type v) (M : Type w) [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L 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
theorem lie_module.nilpotency_length_eq_zero_iff (R : Type u) (L : Type v) (M : Type w) [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] [ M] :
theorem lie_module.nilpotency_length_eq_succ_iff (R : Type u) (L : Type v) (M : Type w) [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] (k : ) :
= k + 1 (k + 1) =
noncomputable def lie_module.lower_central_series_last (R : Type u) (L : Type v) (M : Type w) [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] :
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
• = lie_module.lower_central_series_last._match_1 R L M M)
• lie_module.lower_central_series_last._match_1 R L M (k + 1) =
• lie_module.lower_central_series_last._match_1 R L M 0 =
theorem lie_module.lower_central_series_last_le_max_triv (R : Type u) (L : Type v) (M : Type w) [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] :
theorem lie_module.nontrivial_lower_central_series_last (R : Type u) (L : Type v) (M : Type w) [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] [nontrivial M] [ M] :
theorem lie_module.nontrivial_max_triv_of_is_nilpotent (R : Type u) (L : Type v) (M : Type w) [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] [nontrivial M] [ M] :
@[simp]
theorem lie_module.coe_lcs_range_to_endomorphism_eq (R : Type u) (L : Type v) (M : Type w) [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] (k : ) :
M k) = k)
@[simp]
theorem lie_module.is_nilpotent_range_to_endomorphism_iff (R : Type u) (L : Type v) (M : Type w) [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] :
M
def lie_submodule.ucs {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] (k : ) :
M M

The upper (aka ascending) central series.

See also lie_submodule.lcs.

Equations
@[simp]
theorem lie_submodule.ucs_zero {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] (N : M) :
= N
@[simp]
theorem lie_submodule.ucs_succ {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] (N : M) (k : ) :
theorem lie_submodule.ucs_add {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] (N : M) (k l : ) :
theorem lie_submodule.ucs_mono {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] {N₁ N₂ : M} (k : ) (h : N₁ N₂) :
theorem lie_submodule.ucs_eq_self_of_centralizer_eq_self {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] {N₁ : M} (h : N₁.centralizer = N₁) (k : ) :
= N₁
theorem lie_submodule.ucs_le_of_centralizer_eq_self {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] {N₁ : M} (h : N₁.centralizer = N₁) (k : ) :
N₁

If a Lie module M contains a self-centralizing 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 lie_submodule.lcs_add_le_iff {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] {N₁ N₂ : M} (l k : ) :
lie_submodule.lcs (l + k) N₁ N₂
theorem lie_submodule.lcs_le_iff {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] {N₁ N₂ : M} (k : ) :
N₂ N₁
theorem lie_submodule.gc_lcs_ucs {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] (k : ) :
galois_connection (λ (N : M), (λ (N : M),
theorem lie_submodule.ucs_eq_top_iff {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] (N : M) (k : ) :
N
theorem lie_module.is_nilpotent_iff_exists_ucs_eq_top {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] :
∃ (k : ),
theorem lie_submodule.ucs_comap_incl {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] (N : M) (k : ) :
theorem lie_submodule.is_nilpotent_iff_exists_self_le_ucs {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] (N : M) :
∃ (k : ),
theorem function.surjective.lie_module_lcs_map_eq {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] {L₂ : Type u_1} {M₂ : Type u_2} [lie_ring L₂] [ L₂] [add_comm_group M₂] [ M₂] [ M₂] [ L₂ M₂] {f : L →ₗ⁅R L₂} {g : M →ₗ[R] M₂} (hf : function.surjective f) (hg : function.surjective g) (hfg : ∀ (x : L) (m : M), f x,g m = g x,m) (k : ) :
k) = M₂ k)
theorem function.surjective.lie_module_is_nilpotent {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] {L₂ : Type u_1} {M₂ : Type u_2} [lie_ring L₂] [ L₂] [add_comm_group M₂] [ M₂] [ M₂] [ L₂ M₂] {f : L →ₗ⁅R L₂} {g : M →ₗ[R] M₂} (hf : function.surjective f) (hg : function.surjective g) (hfg : ∀ (x : L) (m : M), f x,g m = g x,m) [ M] :
M₂
theorem equiv.lie_module_is_nilpotent_iff {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] {L₂ : Type u_1} {M₂ : Type u_2} [lie_ring L₂] [ L₂] [add_comm_group M₂] [ M₂] [ M₂] [ L₂ M₂] (f : L ≃ₗ⁅R L₂) (g : M ≃ₗ[R] M₂) (hfg : ∀ (x : L) (m : M), f x,g m = g x,m) :
M₂
@[simp]
theorem lie_module.is_nilpotent_of_top_iff {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] :
@[protected, instance]
def lie_algebra.is_solvable_of_is_nilpotent (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [ L] [hL : L] :
@[reducible]
def lie_algebra.is_nilpotent (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [ L] :
Prop

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

theorem lie_algebra.nilpotent_ad_of_nilpotent_algebra (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [ L]  :
∃ (k : ), ∀ (x : L), L) x ^ k = 0
theorem lie_algebra.infi_max_gen_zero_eigenspace_eq_top_of_nilpotent (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [ L]  :
(⨅ (x : L), 0) =

See also lie_algebra.zero_root_space_eq_top_of_nilpotent.

theorem coe_lower_central_series_ideal_quot_eq {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [ L] {I : L} (k : ) :
(L I) k) = (L I) (L I) 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 lie_module.coe_lower_central_series_ideal_le {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [ L] {I : L} (k : ) :
k) 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 lie_algebra.nilpotent_of_nilpotent_quotient {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [ L] {I : L} (h₁ : I ) (h₂ : (L I)) :

A central extension of nilpotent Lie algebras is nilpotent.

theorem lie_algebra.non_trivial_center_of_is_nilpotent {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [ L] [nontrivial L]  :
theorem lie_ideal.map_lower_central_series_le {R : Type u} {L : Type v} {L' : Type w} [comm_ring R] [lie_ring L] [ L] [lie_ring L'] [ L'] (k : ) {f : L →ₗ⁅R L'} :
k) k
theorem lie_ideal.lower_central_series_map_eq {R : Type u} {L : Type v} {L' : Type w} [comm_ring R] [lie_ring L] [ L] [lie_ring L'] [ L'] (k : ) {f : L →ₗ⁅R L'} (h : function.surjective f) :
k) = k
theorem function.injective.lie_algebra_is_nilpotent {R : Type u} {L : Type v} {L' : Type w} [comm_ring R] [lie_ring L] [ L] [lie_ring L'] [ L'] [h₁ : L'] {f : L →ₗ⁅R L'} (h₂ : function.injective f) :
theorem function.surjective.lie_algebra_is_nilpotent {R : Type u} {L : Type v} {L' : Type w} [comm_ring R] [lie_ring L] [ L] [lie_ring L'] [ L'] [h₁ : L] {f : L →ₗ⁅R L'} (h₂ : function.surjective f) :
theorem lie_equiv.nilpotent_iff_equiv_nilpotent {R : Type u} {L : Type v} {L' : Type w} [comm_ring R] [lie_ring L] [ L] [lie_ring L'] [ L'] (e : L ≃ₗ⁅R L') :
theorem lie_hom.is_nilpotent_range {R : Type u} {L : Type v} {L' : Type w} [comm_ring R] [lie_ring L] [ L] [lie_ring L'] [ L'] (f : L →ₗ⁅R L') :
@[simp]
theorem lie_algebra.is_nilpotent_range_ad_iff {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [ L] :

Note that this result is not quite a special case of lie_module.is_nilpotent_range_to_endomorphism_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.

@[protected, instance]
def has_top.top.lie_algebra.is_nilpotent {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [ L] [h : L] :
def lie_ideal.lcs {R : Type u_1} {L : Type u_2} [comm_ring R] [lie_ring L] [ L] (I : L) (M : Type u_3) [ M] [ M] [ L M] (k : ) :
M

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 lie_module.lower_central_series 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 lie_ideal.coe_lcs_eq.

Equations
@[simp]
theorem lie_ideal.lcs_zero {R : Type u_1} {L : Type u_2} [comm_ring R] [lie_ring L] [ L] (I : L) (M : Type u_3) [ M] [ M] [ L M] :
I.lcs M 0 =
@[simp]
theorem lie_ideal.lcs_succ {R : Type u_1} {L : Type u_2} [comm_ring R] [lie_ring L] [ L] (I : L) (M : Type u_3) [ M] [ M] [ L M] (k : ) :
I.lcs M (k + 1) = I,I.lcs M k
theorem lie_ideal.lcs_top {R : Type u_1} {L : Type u_2} [comm_ring R] [lie_ring L] [ L] (M : Type u_3) [ M] [ M] [ L M] (k : ) :
.lcs M k =
theorem lie_ideal.coe_lcs_eq {R : Type u_1} {L : Type u_2} [comm_ring R] [lie_ring L] [ L] (I : L) (M : Type u_3) [ M] [ M] [ L M] (k : ) :
(I.lcs M k) = k)
theorem lie_algebra.ad_nilpotent_of_nilpotent (R : Type u) {A : Type v} [comm_ring R] [ring A] [ A] {a : A} (h : is_nilpotent a) :
theorem lie_subalgebra.is_nilpotent_ad_of_is_nilpotent_ad {R : Type u} [comm_ring R] {L : Type v} [lie_ring L] [ L] (K : L) {x : K} (h : is_nilpotent ( L) x)) :
theorem lie_algebra.is_nilpotent_ad_of_is_nilpotent {R : Type u} {A : Type v} [comm_ring R] [ring A] [ A] {L : A} {x : L} (h : is_nilpotent x) :