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