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
• LieModule.maxNilpotentSubmodule
• LieAlgebra.maxNilpotentIdeal

Tags

lie algebra, lower central series, nilpotent, max nilpotent ideal

def LieSubmodule.lcs {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] (k : ℕ) : LieSubmodule R L M → LieSubmodule 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.

@[simp]

theorem LieSubmodule.lcs_zero {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) : lcs 0 N = N

@[simp]

theorem LieSubmodule.lcs_succ {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] (k : ℕ) (N : LieSubmodule R L M) : lcs (k + 1) N = ⁅⊤, lcs k N⁆

@[simp]

theorem LieSubmodule.lcs_sup {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] {N₁ N₂ : LieSubmodule R L M} {k : ℕ} : lcs k (N₁ ⊔ N₂) = lcs k N₁ ⊔ lcs k N₂

def LieModule.lowerCentralSeries (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] (k : ℕ) : LieSubmodule R L M

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

@[simp]

theorem LieModule.lowerCentralSeries_zero (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] : lowerCentralSeries R L M 0 = ⊤

@[simp]

theorem LieModule.lowerCentralSeries_succ (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] (k : ℕ) : lowerCentralSeries R L M (k + 1) = ⁅⊤, lowerCentralSeries R L M k⁆

theorem LieModule.coe_lowerCentralSeries_eq_int (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (k : ℕ) : ↑(lowerCentralSeries R L M k) = ↑(lowerCentralSeries ℤ L M k)

theorem LieSubmodule.lcs_le_self {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] (k : ℕ) (N : LieSubmodule R L M) : lcs k N ≤ N

theorem LieSubmodule.lowerCentralSeries_eq_lcs_comap {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] (k : ℕ) (N : LieSubmodule R L M) [LieModule R L M] : LieModule.lowerCentralSeries R L (↥N) k = comap N.incl (lcs k N)

theorem LieSubmodule.lowerCentralSeries_map_eq_lcs {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] (k : ℕ) (N : LieSubmodule R L M) [LieModule R L M] : map N.incl (LieModule.lowerCentralSeries R L (↥N) k) = lcs k N

theorem LieSubmodule.lowerCentralSeries_eq_bot_iff_lcs_eq_bot {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] (k : ℕ) (N : LieSubmodule R L M) [LieModule R L M] : LieModule.lowerCentralSeries R L (↥N) k = ⊥ ↔ lcs k N = ⊥

theorem LieModule.antitone_lowerCentralSeries (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] : Antitone (lowerCentralSeries R L M)

theorem LieModule.eventually_iInf_lowerCentralSeries_eq (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [IsArtinian R M] : ∀ᶠ (l : ℕ) in Filter.atTop, ⨅ (k : ℕ), lowerCentralSeries R L M k = lowerCentralSeries R L M l

theorem LieModule.trivial_iff_lower_central_eq_bot (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] : IsTrivial L M ↔ lowerCentralSeries R L M 1 = ⊥

theorem LieModule.iterate_toEnd_mem_lowerCentralSeries (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (x : L) (m : M) (k : ℕ) : (⇑((toEnd R L M) x))^[k] m ∈ lowerCentralSeries R L M k

theorem LieModule.iterate_toEnd_mem_lowerCentralSeries₂ (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (x y : L) (m : M) (k : ℕ) : (⇑((toEnd R L M) x ∘ₗ (toEnd R L M) y))^[k] m ∈ lowerCentralSeries R L M (2 * k)

theorem LieModule.map_lowerCentralSeries_le {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] (k : ℕ) {M₂ : Type w₁} [AddCommGroup M₂] [Module R M₂] [LieRingModule L M₂] [LieModule R L M₂] [LieModule R L M] (f : M →ₗ⁅R,L⁆ M₂) : LieSubmodule.map f (lowerCentralSeries R L M k) ≤ lowerCentralSeries R L M₂ k

theorem LieModule.map_lowerCentralSeries_eq {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] (k : ℕ) {M₂ : Type w₁} [AddCommGroup M₂] [Module R M₂] [LieRingModule L M₂] [LieModule R L M₂] [LieModule R L M] {f : M →ₗ⁅R,L⁆ M₂} (hf : Function.Surjective ⇑f) : LieSubmodule.map f (lowerCentralSeries R L M k) = lowerCentralSeries R L M₂ k

theorem LieModule.derivedSeries_le_lowerCentralSeries (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (k : ℕ) : LieAlgebra.derivedSeries R L k ≤ lowerCentralSeries R L L k

class LieModule.IsNilpotent (L : Type v) (M : Type w) [LieRing L] [AddCommGroup M] [LieRingModule L M] : Prop

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

• mk_int :: (
• nilpotent_int : ∃ (k : ℕ), lowerCentralSeries ℤ L M k = ⊥
• )

theorem LieModule.isNilpotent_iff_int (L : Type v) (M : Type w) [LieRing L] [AddCommGroup M] [LieRingModule L M] : IsNilpotent L M ↔ ∃ (k : ℕ), lowerCentralSeries ℤ L M k = ⊥

theorem LieModule.isNilpotent_iff (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] : IsNilpotent L M ↔ ∃ (k : ℕ), lowerCentralSeries R L M k = ⊥

See also LieModule.isNilpotent_iff_exists_ucs_eq_top.

theorem LieModule.IsNilpotent.nilpotent (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [IsNilpotent L M] : ∃ (k : ℕ), lowerCentralSeries R L M k = ⊥

theorem LieModule.IsNilpotent.mk {R : Type u} {L : Type v} (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {k : ℕ} (h : lowerCentralSeries R L M k = ⊥) : IsNilpotent L M

@[simp]

theorem LieModule.iInf_lowerCentralSeries_eq_bot_of_isNilpotent (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [IsNilpotent L M] : ⨅ (k : ℕ), lowerCentralSeries R L M k = ⊥

theorem LieSubmodule.isNilpotent_iff_exists_lcs_eq_bot {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (N : LieSubmodule R L M) : LieModule.IsNilpotent L ↥N ↔ ∃ (k : ℕ), lcs k N = ⊥

@[instance 100]

instance LieModule.trivialIsNilpotent (L : Type v) (M : Type w) [LieRing L] [AddCommGroup M] [LieRingModule L M] [IsTrivial L M] : IsNilpotent L M

instance LieModule.instIsNilpotentSup (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (M₁ M₂ : LieSubmodule R L M) [IsNilpotent L ↥M₁] [IsNilpotent L ↥M₂] : IsNilpotent L ↥(M₁ ⊔ M₂)

theorem LieModule.exists_forall_pow_toEnd_eq_zero (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [IsNilpotent L M] : ∃ (k : ℕ), ∀ (x : L), (toEnd R L M) x ^ k = 0

theorem LieModule.isNilpotent_toEnd_of_isNilpotent (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [IsNilpotent L M] (x : L) : _root_.IsNilpotent ((toEnd R L M) x)

theorem LieModule.isNilpotent_toEnd_of_isNilpotent₂ (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [IsNilpotent L M] (x y : L) : _root_.IsNilpotent ((toEnd R L M) x ∘ₗ (toEnd R L M) y)

@[simp]

theorem LieModule.maxGenEigenSpace_toEnd_eq_top (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [IsNilpotent L M] (x : L) : ((toEnd R L M) x).maxGenEigenspace 0 = ⊤

theorem LieModule.nilpotentOfNilpotentQuotient (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {N : LieSubmodule R L M} (h₁ : N ≤ maxTrivSubmodule R L M) (h₂ : IsNilpotent L (M ⧸ N)) : IsNilpotent L M

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) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) [LieModule R L M] : IsNilpotent L (M ⧸ N) ↔ ∃ (k : ℕ), lowerCentralSeries R L M k ≤ N

theorem LieModule.iInf_lcs_le_of_isNilpotent_quot (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) [LieModule R L M] (h : IsNilpotent L (M ⧸ N)) : ⨅ (k : ℕ), lowerCentralSeries R L M k ≤ N

noncomputable def LieModule.nilpotencyLength (L : Type v) (M : Type w) [LieRing L] [AddCommGroup M] [LieRingModule 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.

@[simp]

theorem LieModule.nilpotencyLength_eq_zero_iff (L : Type v) (M : Type w) [LieRing L] [AddCommGroup M] [LieRingModule L M] [IsNilpotent L M] : nilpotencyLength L M = 0 ↔ Subsingleton M

theorem LieModule.nilpotencyLength_eq_succ_iff (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (k : ℕ) : nilpotencyLength L M = k + 1 ↔ lowerCentralSeries R L M (k + 1) = ⊥ ∧ lowerCentralSeries R L M k ≠ ⊥

@[simp]

theorem LieModule.nilpotencyLength_eq_one_iff (L : Type v) (M : Type w) [LieRing L] [AddCommGroup M] [LieRingModule L M] [Nontrivial M] : nilpotencyLength L M = 1 ↔ IsTrivial L M

theorem LieModule.isTrivial_of_nilpotencyLength_le_one (L : Type v) (M : Type w) [LieRing L] [AddCommGroup M] [LieRingModule L M] [IsNilpotent L M] (h : nilpotencyLength L M ≤ 1) : IsTrivial L M

noncomputable def LieModule.lowerCentralSeriesLast (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] : LieSubmodule R L 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, ⊥.

theorem LieModule.lowerCentralSeriesLast_le_max_triv (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] : lowerCentralSeriesLast R L M ≤ maxTrivSubmodule R L M

theorem LieModule.nontrivial_lowerCentralSeriesLast (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [Nontrivial M] [IsNilpotent L M] : Nontrivial ↥(lowerCentralSeriesLast R L M)

theorem LieModule.lowerCentralSeriesLast_le_of_not_isTrivial (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [IsNilpotent L M] (h : ¬IsTrivial L M) : lowerCentralSeriesLast R L M ≤ lowerCentralSeries R L M 1

theorem LieModule.disjoint_lowerCentralSeries_maxTrivSubmodule_iff (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [IsNilpotent L M] : Disjoint (lowerCentralSeries R L M 1) (maxTrivSubmodule R L M) ↔ IsTrivial L M

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) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [Nontrivial M] [IsNilpotent L M] : Nontrivial ↥(maxTrivSubmodule R L M)

@[simp]

theorem LieModule.coe_lcs_range_toEnd_eq (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (k : ℕ) : ↑(lowerCentralSeries R (↥(toEnd R L M).range) M k) = ↑(lowerCentralSeries R L M k)

@[simp]

theorem LieModule.isNilpotent_range_toEnd_iff (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] : IsNilpotent (↥(toEnd R L M).range) M ↔ IsNilpotent L M

def LieSubmodule.ucs {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (k : ℕ) : LieSubmodule R L M → LieSubmodule R L M

The upper (aka ascending) central series.

See also LieSubmodule.lcs.

@[simp]

theorem LieSubmodule.ucs_zero {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) [LieModule R L M] : ucs 0 N = N

@[simp]

theorem LieSubmodule.ucs_succ {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) [LieModule R L M] (k : ℕ) : ucs (k + 1) N = (ucs k N).normalizer

theorem LieSubmodule.ucs_add {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) [LieModule R L M] (k l : ℕ) : ucs (k + l) N = ucs k (ucs l N)

theorem LieSubmodule.ucs_mono {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] {N₁ N₂ : LieSubmodule R L M} [LieModule R L M] (k : ℕ) (h : N₁ ≤ N₂) : ucs k N₁ ≤ ucs k N₂

theorem LieSubmodule.ucs_eq_self_of_normalizer_eq_self {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] {N₁ : LieSubmodule R L M} [LieModule R L M] (h : N₁.normalizer = N₁) (k : ℕ) : ucs k N₁ = N₁

theorem LieSubmodule.ucs_le_of_normalizer_eq_self {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] {N₁ : LieSubmodule R L M} [LieModule R L M] (h : N₁.normalizer = N₁) (k : ℕ) : ucs 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} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] {N₁ N₂ : LieSubmodule R L M} [LieModule R L M] (l k : ℕ) : lcs (l + k) N₁ ≤ N₂ ↔ lcs l N₁ ≤ ucs k N₂

theorem LieSubmodule.lcs_le_iff {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] {N₁ N₂ : LieSubmodule R L M} [LieModule R L M] (k : ℕ) : lcs k N₁ ≤ N₂ ↔ N₁ ≤ ucs k N₂

theorem LieSubmodule.gc_lcs_ucs {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (k : ℕ) : GaloisConnection (fun (N : LieSubmodule R L M) => lcs k N) fun (N : LieSubmodule R L M) => ucs k N

theorem LieSubmodule.ucs_eq_top_iff {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) [LieModule R L M] (k : ℕ) : ucs k N = ⊤ ↔ LieModule.lowerCentralSeries R L M k ≤ N

theorem LieModule.isNilpotent_iff_exists_ucs_eq_top (R : Type u) {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] : IsNilpotent L M ↔ ∃ (k : ℕ), LieSubmodule.ucs k ⊥ = ⊤

theorem LieSubmodule.ucs_comap_incl {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) [LieModule R L M] (k : ℕ) : comap N.incl (ucs k ⊥) = ucs k ⊥

theorem LieSubmodule.isNilpotent_iff_exists_self_le_ucs {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) [LieModule R L M] : LieModule.IsNilpotent L ↥N ↔ ∃ (k : ℕ), N ≤ ucs k ⊥

theorem LieSubmodule.ucs_bot_one {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] : ucs 1 ⊥ = LieModule.maxTrivSubmodule R L M

theorem lieModule_lcs_map_le {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {L₂ : Type u_1} {M₂ : Type u_2} [LieRing L₂] [LieAlgebra R L₂] [AddCommGroup M₂] [Module R M₂] [LieRingModule L₂ M₂] {f : L →ₗ⁅R⁆ L₂} {g : M →ₗ[R] M₂} (hfg : ∀ (x : L) (m : M), ⁅f x, g m⁆ = g ⁅x, m⁆) (k : ℕ) : Submodule.map g ↑(LieModule.lowerCentralSeries R L M k) ≤ ↑(LieModule.lowerCentralSeries R L₂ M₂ k)

theorem Function.Injective.lieModuleIsNilpotent {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {L₂ : Type u_1} {M₂ : Type u_2} [LieRing L₂] [LieAlgebra R L₂] [AddCommGroup M₂] [Module R M₂] [LieRingModule L₂ M₂] {f : L →ₗ⁅R⁆ L₂} {g : M →ₗ[R] M₂} (hfg : ∀ (x : L) (m : M), ⁅f x, g m⁆ = g ⁅x, m⁆) [LieModule R L₂ M₂] (hg_inj : Injective ⇑g) [LieModule.IsNilpotent L₂ M₂] : LieModule.IsNilpotent L M

theorem Function.Surjective.lieModule_lcs_map_eq {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {L₂ : Type u_1} {M₂ : Type u_2} [LieRing L₂] [LieAlgebra R L₂] [AddCommGroup M₂] [Module R M₂] [LieRingModule L₂ M₂] {f : L →ₗ⁅R⁆ L₂} {g : M →ₗ[R] M₂} (hfg : ∀ (x : L) (m : M), ⁅f x, g m⁆ = g ⁅x, m⁆) [LieModule R L₂ M₂] (hf_surj : Surjective ⇑f) (hg_surj : Surjective ⇑g) (k : ℕ) : Submodule.map g ↑(LieModule.lowerCentralSeries R L M k) = ↑(LieModule.lowerCentralSeries R L₂ M₂ k)

theorem Function.Surjective.lieModuleIsNilpotent {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {L₂ : Type u_1} {M₂ : Type u_2} [LieRing L₂] [LieAlgebra R L₂] [AddCommGroup M₂] [Module R M₂] [LieRingModule L₂ M₂] {f : L →ₗ⁅R⁆ L₂} {g : M →ₗ[R] M₂} (hfg : ∀ (x : L) (m : M), ⁅f x, g m⁆ = g ⁅x, m⁆) [LieModule R L₂ M₂] (hf_surj : Surjective ⇑f) (hg_surj : Surjective ⇑g) [LieModule.IsNilpotent L M] : LieModule.IsNilpotent L₂ M₂

theorem Equiv.lieModule_isNilpotent_iff {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {L₂ : Type u_1} {M₂ : Type u_2} [LieRing L₂] [LieAlgebra R L₂] [AddCommGroup M₂] [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⁆) : LieModule.IsNilpotent L M ↔ LieModule.IsNilpotent L₂ M₂

@[simp]

theorem LieModule.isNilpotent_of_top_iff {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] : IsNilpotent (↥⊤) M ↔ IsNilpotent L M

@[simp]

theorem LieModule.isNilpotent_of_top_iff' {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] : IsNilpotent L ↥⊤ ↔ IsNilpotent L M

theorem LieModule.isNilpotent_of_le (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (M₁ M₂ : LieSubmodule R L M) (h₁ : M₁ ≤ M₂) [IsNilpotent L ↥M₂] : IsNilpotent L ↥M₁

def LieModule.maxNilpotentSubmodule (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] : LieSubmodule R L M

The max nilpotent submodule is the sSup of all nilpotent submodules.

instance LieModule.instMaxNilpotentSubmoduleIsNilpotent (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [IsNoetherian R M] : IsNilpotent L ↥(maxNilpotentSubmodule R L M)

theorem LieModule.isNilpotent_iff_le_maxNilpotentSubmodule (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [IsNoetherian R M] (N : LieSubmodule R L M) : IsNilpotent L ↥N ↔ N ≤ maxNilpotentSubmodule R L M

@[simp]

theorem LieModule.maxNilpotentSubmodule_eq_top_of_isNilpotent (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [IsNilpotent L M] : maxNilpotentSubmodule R L M = ⊤

@[instance 100]

instance LieAlgebra.isSolvable_of_isNilpotent (L : Type v) [LieRing L] [hL : LieModule.IsNilpotent L L] : IsSolvable L

@[reducible, inline]

abbrev LieRing.IsNilpotent (L : Type v) [LieRing L] : Prop

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

theorem LieAlgebra.nilpotent_ad_of_nilpotent_algebra (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing.IsNilpotent L] : ∃ (k : ℕ), ∀ (x : L), (ad R L) x ^ k = 0

theorem coe_lowerCentralSeries_ideal_quot_eq {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {I : LieIdeal R L} (k : ℕ) : ↑(LieModule.lowerCentralSeries R L (L ⧸ I) k) = ↑(LieModule.lowerCentralSeries R (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 LieModule.coe_lowerCentralSeries_ideal_le {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {I : LieIdeal R L} (k : ℕ) : ↑(lowerCentralSeries R (↥I) (↥I) k) ≤ ↑(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} [CommRing R] [LieRing L] [LieAlgebra R L] {I : LieIdeal R L} (h₁ : I ≤ center R L) (h₂ : LieRing.IsNilpotent (L ⧸ I)) : LieRing.IsNilpotent L

A central extension of nilpotent Lie algebras is nilpotent.

theorem LieAlgebra.non_trivial_center_of_isNilpotent {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] [Nontrivial L] [LieRing.IsNilpotent L] : Nontrivial ↥(center R L)

theorem LieIdeal.map_lowerCentralSeries_le {R : Type u} {L : Type v} {L' : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] (k : ℕ) {f : L →ₗ⁅R⁆ L'} : map f (LieModule.lowerCentralSeries R L L k) ≤ LieModule.lowerCentralSeries R L' L' k

theorem LieIdeal.lowerCentralSeries_map_eq {R : Type u} {L : Type v} {L' : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] (k : ℕ) {f : L →ₗ⁅R⁆ L'} (h : Function.Surjective ⇑f) : map f (LieModule.lowerCentralSeries R L L k) = LieModule.lowerCentralSeries R L' L' k

theorem Function.Injective.lieAlgebra_isNilpotent {R : Type u} {L : Type v} {L' : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] [h₁ : LieRing.IsNilpotent L'] {f : L →ₗ⁅R⁆ L'} (h₂ : Injective ⇑f) : LieRing.IsNilpotent L

theorem Function.Surjective.lieAlgebra_isNilpotent {R : Type u} {L : Type v} {L' : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] [h₁ : LieRing.IsNilpotent L] {f : L →ₗ⁅R⁆ L'} (h₂ : Surjective ⇑f) : LieRing.IsNilpotent L'

theorem LieEquiv.nilpotent_iff_equiv_nilpotent {R : Type u} {L : Type v} {L' : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] (e : L ≃ₗ⁅R⁆ L') : LieRing.IsNilpotent L ↔ LieRing.IsNilpotent L'

theorem LieHom.isNilpotent_range {R : Type u} {L : Type v} {L' : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] [LieRing.IsNilpotent L] (f : L →ₗ⁅R⁆ L') : LieRing.IsNilpotent ↥f.range

@[simp]

theorem LieAlgebra.isNilpotent_range_ad_iff {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] : LieRing.IsNilpotent ↥(ad R L).range ↔ LieRing.IsNilpotent L

Note that this result is not quite a special case of LieModule.isNilpotent_range_toEnd_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} [CommRing R] [LieRing L] [LieAlgebra R L] [h : LieRing.IsNilpotent L] : LieRing.IsNilpotent ↥⊤

def LieIdeal.lcs {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) (M : Type u_3) [AddCommGroup M] [Module R M] [LieRingModule L M] (k : ℕ) : LieSubmodule R L 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 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.

@[simp]

theorem LieIdeal.lcs_zero {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) (M : Type u_3) [AddCommGroup M] [Module R M] [LieRingModule L M] : I.lcs M 0 = ⊤

@[simp]

theorem LieIdeal.lcs_succ {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) (M : Type u_3) [AddCommGroup M] [Module R M] [LieRingModule L M] (k : ℕ) : I.lcs M (k + 1) = ⁅I, I.lcs M k⁆

theorem LieIdeal.lcs_top {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (M : Type u_3) [AddCommGroup M] [Module R M] [LieRingModule L M] (k : ℕ) : ⊤.lcs M k = LieModule.lowerCentralSeries R L M k

theorem LieIdeal.coe_lcs_eq {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) (M : Type u_3) [AddCommGroup M] [Module R M] [LieRingModule L M] (k : ℕ) [LieModule R L M] : ↑(I.lcs M k) = ↑(LieModule.lowerCentralSeries R (↥I) M k)

instance LieIdeal.instIsNilpotentSubtypeMemLieSubmoduleOfIsNilpotent {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) [LieModule.IsNilpotent L ↥I] : LieRing.IsNilpotent ↥I

theorem LieAlgebra.ad_nilpotent_of_nilpotent (R : Type u) {A : Type v} [CommRing R] [Ring A] [Algebra R A] {a : A} (h : IsNilpotent a) : IsNilpotent ((ad R A) a)

theorem LieSubalgebra.isNilpotent_ad_of_isNilpotent_ad {R : Type u} [CommRing R] {L : Type v} [LieRing L] [LieAlgebra R L] (K : LieSubalgebra R L) {x : ↥K} (h : IsNilpotent ((LieAlgebra.ad R L) ↑x)) : IsNilpotent ((LieAlgebra.ad R ↥K) x)

theorem LieAlgebra.isNilpotent_ad_of_isNilpotent {R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A] {L : LieSubalgebra R A} {x : ↥L} (h : IsNilpotent ↑x) : IsNilpotent ((ad R ↥L) x)

@[simp]

theorem LieSubmodule.lowerCentralSeries_tensor_eq_baseChange (R : Type u_1) (A : Type u_2) (L : Type u_3) (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [CommRing A] [Algebra R A] (k : ℕ) : LieModule.lowerCentralSeries A (TensorProduct R A L) (TensorProduct R A M) k = baseChange A (LieModule.lowerCentralSeries R L M k)

instance LieModule.instIsNilpotentTensor (R : Type u_1) (A : Type u_2) (L : Type u_3) (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [CommRing A] [Algebra R A] [IsNilpotent L M] : IsNilpotent (TensorProduct R A L) (TensorProduct R A M)

def LieAlgebra.maxNilpotentIdeal (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] : LieSubmodule R L L

The max nilpotent ideal of a Lie algebra. It is defined as the max nilpotent Lie submodule of L under the adjoint action.

instance LieAlgebra.maxNilpotentIdealIsNilpotent (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] [IsNoetherian R L] : LieModule.IsNilpotent L ↥(maxNilpotentIdeal R L)

theorem LieAlgebra.LieIdeal.isNilpotent_iff_le_maxNilpotentIdeal (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] [IsNoetherian R L] (I : LieIdeal R L) : LieModule.IsNilpotent L ↥I ↔ I ≤ maxNilpotentIdeal R L

theorem LieAlgebra.center_le_maxNilpotentIdeal (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] : center R L ≤ maxNilpotentIdeal R L

theorem LieAlgebra.maxNilpotentIdeal_le_radical (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] : maxNilpotentIdeal R L ≤ radical R L

@[simp]

theorem LieAlgebra.maxNilpotentIdeal_eq_top_of_isNilpotent (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing.IsNilpotent L] : maxNilpotentIdeal R L = ⊤