mathlib documentation

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 #

Tags #

lie algebra, lower central series, nilpotent

def lie_module.lower_central_series (R : Type u) (L : Type v) (M : Type w) [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] (k : ) :

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] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R 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] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] (k : ) :
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] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] (x : L) (m : M) (k : ) :
@[class]
structure lie_module.is_nilpotent (R : Type u) (L : Type v) (M : Type w) [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] :
Prop

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

Instances
@[instance]
def lie_module.trivial_is_nilpotent (R : Type u) (L : Type v) (M : Type w) [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] [lie_module.is_trivial 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] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] [hM : lie_module.is_nilpotent R L M] :
∃ (k : ), ∀ (x : L), (lie_module.to_endomorphism R L M) x ^ k = 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.

@[instance]
def lie_algebra.is_nilpotent (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [lie_algebra R 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] [lie_algebra R L] [lie_algebra.is_nilpotent R L] :
∃ (k : ), ∀ (x : L), (lie_algebra.ad R L) x ^ k = 0
theorem lie_ideal.lower_central_series_map_le {R : Type u} {L : Type v} {L' : Type w} [comm_ring R] [lie_ring L] [lie_algebra R L] [lie_ring L'] [lie_algebra R L'] (k : ) {f : L →ₗ⁅R L'} :
theorem lie_ideal.lower_central_series_map_eq {R : Type u} {L : Type v} {L' : Type w} [comm_ring R] [lie_ring L] [lie_algebra R L] [lie_ring L'] [lie_algebra R L'] (k : ) {f : L →ₗ⁅R L'} (h : function.surjective f) :
theorem function.injective.lie_algebra_is_nilpotent {R : Type u} {L : Type v} {L' : Type w} [comm_ring R] [lie_ring L] [lie_algebra R L] [lie_ring L'] [lie_algebra R L'] [h₁ : lie_algebra.is_nilpotent R 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] [lie_algebra R L] [lie_ring L'] [lie_algebra R L'] [h₁ : lie_algebra.is_nilpotent R 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] [lie_algebra R L] [lie_ring L'] [lie_algebra R L'] (e : L ≃ₗ⁅R L') :
theorem lie_algebra.ad_nilpotent_of_nilpotent (R : Type u) {A : Type v} [comm_ring R] [ring A] [algebra R A] {a : A} (h : is_nilpotent a) :
theorem lie_algebra.is_nilpotent_ad_of_is_nilpotent {R : Type u} {A : Type v} [comm_ring R] [ring A] [algebra R A] {L : lie_subalgebra R A} {x : L} (h : is_nilpotent x) :