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

Tags

lie algebra, lower central series, nilpotent

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.

Equations

• LieSubmodule.lcs k = (fun (N : LieSubmodule R L M) => ⁅⊤, N⁆)^[k]

@[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) : LieSubmodule.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) : LieSubmodule.lcs (k + 1) N = ⁅⊤, LieSubmodule.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₁ : LieSubmodule R L M} {N₂ : LieSubmodule R L M} {k : ℕ} : LieSubmodule.lcs k (N₁ ⊔ N₂) = LieSubmodule.lcs k N₁ ⊔ LieSubmodule.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.

Equations

• LieModule.lowerCentralSeries R L M k = LieSubmodule.lcs k ⊤

@[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] : LieModule.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 : ℕ) : LieModule.lowerCentralSeries R L M (k + 1) = ⁅⊤, LieModule.lowerCentralSeries R 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) : LieSubmodule.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 = LieSubmodule.comap N.incl (LieSubmodule.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] : LieSubmodule.map N.incl (LieModule.lowerCentralSeries R L (↥N) k) = LieSubmodule.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 (LieModule.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 : ℕ), LieModule.lowerCentralSeries R L M k = LieModule.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] : LieModule.IsTrivial L M ↔ LieModule.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 : ℕ) : (⇑((LieModule.toEnd R L M) x))^[k] m ∈ LieModule.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 : L) (y : L) (m : M) (k : ℕ) : (⇑((LieModule.toEnd R L M) x ∘ₗ (LieModule.toEnd R L M) y))^[k] m ∈ LieModule.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 (LieModule.lowerCentralSeries R L M k) ≤ LieModule.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 (LieModule.lowerCentralSeries R L M k) = LieModule.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 ≤ LieModule.lowerCentralSeries R L L k

class LieModule.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] : Prop

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

• nilpotent : ∃ (k : ℕ), LieModule.lowerCentralSeries R L M k = ⊥

theorem LieModule.IsNilpotent.nilpotent {R : Type u} {L : Type v} {M : Type w} : ∀ {inst : CommRing R} {inst_1 : LieRing L} {inst_2 : LieAlgebra R L} {inst_3 : AddCommGroup M} {inst_4 : Module R M} {inst_5 : LieRingModule L M} [self : LieModule.IsNilpotent R L M], ∃ (k : ℕ), LieModule.lowerCentralSeries R L M k = ⊥

theorem LieModule.exists_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.IsNilpotent R L M] : ∃ (k : ℕ), LieModule.lowerCentralSeries R L M k = ⊥

@[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.IsNilpotent R L M] : ⨅ (k : ℕ), LieModule.lowerCentralSeries R 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.IsNilpotent R L M ↔ ∃ (k : ℕ), LieModule.lowerCentralSeries R L M k = ⊥

See also LieModule.isNilpotent_iff_exists_ucs_eq_top.

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 R L ↥N ↔ ∃ (k : ℕ), LieSubmodule.lcs k N = ⊥

@[instance 100]

instance LieModule.trivialIsNilpotent (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.IsTrivial L M] : LieModule.IsNilpotent R L M

Equations

• ⋯ = ⋯

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] [hM : LieModule.IsNilpotent R L M] : ∃ (k : ℕ), ∀ (x : L), (LieModule.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] [LieModule.IsNilpotent R L M] (x : L) : IsNilpotent ((LieModule.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] [LieModule.IsNilpotent R L M] (x : L) (y : L) : IsNilpotent ((LieModule.toEnd R L M) x ∘ₗ (LieModule.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] [LieModule.IsNilpotent R L M] (x : L) : ((LieModule.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 ≤ LieModule.maxTrivSubmodule R L M) (h₂ : LieModule.IsNilpotent R L (M ⧸ N)) : LieModule.IsNilpotent R 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] : LieModule.IsNilpotent R L (M ⧸ N) ↔ ∃ (k : ℕ), LieModule.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 : LieModule.IsNilpotent R L (M ⧸ N)) : ⨅ (k : ℕ), LieModule.lowerCentralSeries R L M k ≤ N

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

Equations

• LieModule.nilpotencyLength R L M = sInf {k : ℕ | LieModule.lowerCentralSeries R L M k = ⊥}

@[simp]

theorem LieModule.nilpotencyLength_eq_zero_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.IsNilpotent R L M] : LieModule.nilpotencyLength R 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] (k : ℕ) : LieModule.nilpotencyLength R L M = k + 1 ↔ LieModule.lowerCentralSeries R L M (k + 1) = ⊥ ∧ LieModule.lowerCentralSeries R L M k ≠ ⊥

@[simp]

theorem LieModule.nilpotencyLength_eq_one_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] [Nontrivial M] : LieModule.nilpotencyLength R L M = 1 ↔ LieModule.IsTrivial L M

theorem LieModule.isTrivial_of_nilpotencyLength_le_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.IsNilpotent R L M] (h : LieModule.nilpotencyLength R L M ≤ 1) : LieModule.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, ⊥.

Equations

• LieModule.lowerCentralSeriesLast R L M = match LieModule.nilpotencyLength R L M with | 0 => ⊥ | k.succ => LieModule.lowerCentralSeries R L M k

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] : LieModule.lowerCentralSeriesLast R L M ≤ LieModule.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] [Nontrivial M] [LieModule.IsNilpotent R L M] : Nontrivial ↥(LieModule.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] [LieModule.IsNilpotent R L M] (h : ¬LieModule.IsTrivial L M) : LieModule.lowerCentralSeriesLast R L M ≤ LieModule.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] [LieModule.IsNilpotent R L M] : Disjoint (LieModule.lowerCentralSeries R L M 1) (LieModule.maxTrivSubmodule R L M) ↔ LieModule.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] [LieModule.IsNilpotent R L M] : Nontrivial ↥(LieModule.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 : ℕ) : ↑(LieModule.lowerCentralSeries R (↥(LieModule.toEnd R L M).range) M k) = ↑(LieModule.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] : LieModule.IsNilpotent R (↥(LieModule.toEnd R L M).range) M ↔ LieModule.IsNilpotent R 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.

Equations

• LieSubmodule.ucs k = LieSubmodule.normalizer^[k]

@[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] : LieSubmodule.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 : ℕ) : LieSubmodule.ucs (k + 1) N = (LieSubmodule.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 : ℕ) : LieSubmodule.ucs (k + l) N = LieSubmodule.ucs k (LieSubmodule.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₁ : LieSubmodule R L M} {N₂ : LieSubmodule R L M} [LieModule R L M] (k : ℕ) (h : N₁ ≤ N₂) : LieSubmodule.ucs k N₁ ≤ LieSubmodule.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 : ℕ) : LieSubmodule.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 : ℕ) : LieSubmodule.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₁ : LieSubmodule R L M} {N₂ : LieSubmodule R L M} [LieModule R L M] (l : ℕ) (k : ℕ) : LieSubmodule.lcs (l + k) N₁ ≤ N₂ ↔ LieSubmodule.lcs l N₁ ≤ LieSubmodule.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₁ : LieSubmodule R L M} {N₂ : LieSubmodule R L M} [LieModule R L M] (k : ℕ) : LieSubmodule.lcs k N₁ ≤ N₂ ↔ N₁ ≤ LieSubmodule.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) => LieSubmodule.lcs k N) fun (N : LieSubmodule R L M) => LieSubmodule.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 : ℕ) : LieSubmodule.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] : LieModule.IsNilpotent R 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 : ℕ) : LieSubmodule.comap N.incl (LieSubmodule.ucs k ⊥) = LieSubmodule.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 R L ↥N ↔ ∃ (k : ℕ), N ≤ LieSubmodule.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] : LieSubmodule.ucs 1 ⊥ = LieModule.maxTrivSubmodule R 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₂] [LieModule R 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 : ℕ) : 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₂] [LieModule R 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⁆) [LieModule.IsNilpotent R L M] : LieModule.IsNilpotent R 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 R L M ↔ LieModule.IsNilpotent R 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] : LieModule.IsNilpotent R (↥⊤) M ↔ LieModule.IsNilpotent R 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] : LieModule.IsNilpotent R L ↥⊤ ↔ LieModule.IsNilpotent R L M

@[instance 100]

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

Equations

• ⋯ = ⋯

@[reducible, inline]

abbrev LieAlgebra.IsNilpotent (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] : Prop

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

Equations

• LieAlgebra.IsNilpotent R L = LieModule.IsNilpotent R L L

theorem LieAlgebra.nilpotent_ad_of_nilpotent_algebra (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsNilpotent R L] : ∃ (k : ℕ), ∀ (x : L), (LieAlgebra.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 : ℕ) : ↑(LieModule.lowerCentralSeries R (↥I) (↥I) k) ≤ ↑(LieModule.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 ≤ LieAlgebra.center R L) (h₂ : LieAlgebra.IsNilpotent R (L ⧸ I)) : LieAlgebra.IsNilpotent R 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] [LieAlgebra.IsNilpotent R L] : Nontrivial ↥(LieAlgebra.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'} : LieIdeal.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) : LieIdeal.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₁ : LieAlgebra.IsNilpotent R L'] {f : L →ₗ⁅R⁆ L'} (h₂ : Function.Injective ⇑f) : LieAlgebra.IsNilpotent R 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₁ : LieAlgebra.IsNilpotent R L] {f : L →ₗ⁅R⁆ L'} (h₂ : Function.Surjective ⇑f) : LieAlgebra.IsNilpotent R 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') : LieAlgebra.IsNilpotent R L ↔ LieAlgebra.IsNilpotent R 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'] [LieAlgebra.IsNilpotent R L] (f : L →ₗ⁅R⁆ L') : LieAlgebra.IsNilpotent R ↥f.range

@[simp]

theorem LieAlgebra.isNilpotent_range_ad_iff {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] : LieAlgebra.IsNilpotent R ↥(LieAlgebra.ad R L).range ↔ LieAlgebra.IsNilpotent R 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 : LieAlgebra.IsNilpotent R L] : LieAlgebra.IsNilpotent R ↥⊤

Equations

• ⋯ = ⋯

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.

Equations

• I.lcs M k = (fun (N : LieSubmodule R L M) => ⁅I, N⁆)^[k] ⊤

@[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)

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 ((LieAlgebra.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 ((LieAlgebra.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 = LieSubmodule.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] [LieModule.IsNilpotent R L M] : LieModule.IsNilpotent A (TensorProduct R A L) (TensorProduct R A M)

Equations

• ⋯ = ⋯