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.

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.

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
@[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] :
@[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] :
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) =
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_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') :
@[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] :
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) :