Nilpotent Lie algebras #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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_submodule.lcs
{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 : ℕ) :
lie_submodule R L M → lie_submodule 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 lie_module.lower_central_series_eq_lcs_comap and
lie_module.lower_central_series_map_eq_lcs below, as well as lie_submodule.ucs.
Equations
- lie_submodule.lcs k = ((λ (N : lie_submodule R L M), ⁅⊤, N⁆)^[k])
@[simp]
theorem
lie_submodule.lcs_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]
(N : lie_submodule R L M) :
lie_submodule.lcs 0 N = N
@[simp]
theorem
lie_submodule.lcs_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 : ℕ)
(N : lie_submodule R L M) :
lie_submodule.lcs (k + 1) N = ⁅⊤, lie_submodule.lcs k N⁆
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 : ℕ) :
lie_submodule R L M
The lower central series of Lie submodules of a Lie module.
Equations
- lie_module.lower_central_series R L M k = lie_submodule.lcs k ⊤
@[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] :
lie_module.lower_central_series R L M 0 = ⊤
@[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 : ℕ) :
lie_module.lower_central_series R L M (k + 1) = ⁅⊤, lie_module.lower_central_series R L M k⁆
theorem
lie_submodule.lcs_le_self
{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 : ℕ)
(N : lie_submodule R L M) :
lie_submodule.lcs k N ≤ 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]
[lie_algebra R L]
[add_comm_group M]
[module R M]
[lie_ring_module L M]
[lie_module R L M]
(k : ℕ)
(N : lie_submodule R L M) :
lie_module.lower_central_series R L ↥N k = lie_submodule.comap N.incl (lie_submodule.lcs k N)
theorem
lie_submodule.lower_central_series_map_eq_lcs
{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 : ℕ)
(N : lie_submodule R L M) :
lie_submodule.map N.incl (lie_module.lower_central_series R L ↥N k) = lie_submodule.lcs k N
theorem
lie_module.antitone_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] :
theorem
lie_module.trivial_iff_lower_central_eq_bot
(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 ↔ lie_module.lower_central_series R L M 1 = ⊥
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 : ℕ) :
⇑(⇑(lie_module.to_endomorphism R L M) x)^[k] m ∈ lie_module.lower_central_series R L M k
theorem
lie_module.map_lower_central_series_le
{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]
{M₂ : Type w₁}
[add_comm_group M₂]
[module R M₂]
[lie_ring_module L M₂]
[lie_module R L M₂]
(k : ℕ)
(f : M →ₗ⁅R,L⁆ M₂) :
lie_submodule.map f (lie_module.lower_central_series R L M k) ≤ lie_module.lower_central_series R L M₂ k
theorem
lie_module.derived_series_le_lower_central_series
(R : Type u)
(L : Type v)
[comm_ring R]
[lie_ring L]
[lie_algebra R L]
(k : ℕ) :
lie_algebra.derived_series R L k ≤ lie_module.lower_central_series R L L 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).
theorem
lie_module.is_nilpotent_iff
(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_nilpotent R L M ↔ ∃ (k : ℕ), lie_module.lower_central_series R L M k = ⊥
theorem
lie_submodule.is_nilpotent_iff_exists_lcs_eq_bot
{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]
(N : lie_submodule R L M) :
lie_module.is_nilpotent R L ↥N ↔ ∃ (k : ℕ), lie_submodule.lcs k N = ⊥
@[protected, 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] :
lie_module.is_nilpotent R 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] :
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]
[lie_algebra R L]
[add_comm_group M]
[module R M]
[lie_ring_module L M]
[lie_module R L M]
[lie_module.is_nilpotent R L M] :
(⨅ (x : L), (⇑(lie_module.to_endomorphism R L M) x).maximal_generalized_eigenspace 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]
[lie_algebra R L]
[add_comm_group M]
[module R M]
[lie_ring_module L M]
[lie_module R L M]
{N : lie_submodule R L M}
(h₁ : N ≤ lie_module.max_triv_submodule R L M)
(h₂ : lie_module.is_nilpotent R L (M ⧸ N)) :
lie_module.is_nilpotent 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 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]
[lie_algebra R L]
[add_comm_group M]
[module R M]
[lie_ring_module L M]
[lie_module R 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
- lie_module.nilpotency_length R L M = has_Inf.Inf {k : ℕ | lie_module.lower_central_series R L M k = ⊥}
theorem
lie_module.nilpotency_length_eq_zero_iff
(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_nilpotent R L M] :
lie_module.nilpotency_length R L M = 0 ↔ subsingleton M
theorem
lie_module.nilpotency_length_eq_succ_iff
(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 : ℕ) :
lie_module.nilpotency_length R L M = k + 1 ↔ lie_module.lower_central_series R L M (k + 1) = ⊥ ∧ lie_module.lower_central_series R L M k ≠ ⊥
noncomputable
def
lie_module.lower_central_series_last
(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_submodule 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
- lie_module.lower_central_series_last R L M = lie_module.lower_central_series_last._match_1 R L M (lie_module.nilpotency_length R L M)
- lie_module.lower_central_series_last._match_1 R L M (k + 1) = lie_module.lower_central_series R L M k
- 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]
[lie_algebra R L]
[add_comm_group M]
[module R M]
[lie_ring_module L M]
[lie_module R 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]
[lie_algebra R L]
[add_comm_group M]
[module R M]
[lie_ring_module L M]
[lie_module R L M]
[nontrivial M]
[lie_module.is_nilpotent R L 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]
[lie_algebra R L]
[add_comm_group M]
[module R M]
[lie_ring_module L M]
[lie_module R L M]
[nontrivial M]
[lie_module.is_nilpotent R L M] :
@[simp]
theorem
lie_module.coe_lcs_range_to_endomorphism_eq
(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 : ℕ) :
↑(lie_module.lower_central_series R ↥((lie_module.to_endomorphism R L M).range) M k) = ↑(lie_module.lower_central_series R L M k)
@[simp]
theorem
lie_module.is_nilpotent_range_to_endomorphism_iff
(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_nilpotent R ↥((lie_module.to_endomorphism R L M).range) M ↔ lie_module.is_nilpotent R L M
def
lie_submodule.ucs
{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 : ℕ) :
lie_submodule R L M → lie_submodule R L M
The upper (aka ascending) central series.
See also lie_submodule.lcs.
Equations
@[simp]
theorem
lie_submodule.ucs_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]
(N : lie_submodule R L M) :
lie_submodule.ucs 0 N = N
@[simp]
theorem
lie_submodule.ucs_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]
(N : lie_submodule R L M)
(k : ℕ) :
lie_submodule.ucs (k + 1) N = (lie_submodule.ucs k N).normalizer
theorem
lie_submodule.ucs_add
{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]
(N : lie_submodule R L M)
(k l : ℕ) :
lie_submodule.ucs (k + l) N = lie_submodule.ucs k (lie_submodule.ucs l N)
theorem
lie_submodule.ucs_mono
{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]
{N₁ N₂ : lie_submodule R L M}
(k : ℕ)
(h : N₁ ≤ N₂) :
lie_submodule.ucs k N₁ ≤ lie_submodule.ucs k N₂
theorem
lie_submodule.ucs_eq_self_of_normalizer_eq_self
{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]
{N₁ : lie_submodule R L M}
(h : N₁.normalizer = N₁)
(k : ℕ) :
lie_submodule.ucs k N₁ = N₁
theorem
lie_submodule.ucs_le_of_normalizer_eq_self
{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]
{N₁ : lie_submodule R L M}
(h : N₁.normalizer = N₁)
(k : ℕ) :
lie_submodule.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
lie_submodule.lcs_add_le_iff
{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]
{N₁ N₂ : lie_submodule R L M}
(l k : ℕ) :
lie_submodule.lcs (l + k) N₁ ≤ N₂ ↔ lie_submodule.lcs l N₁ ≤ lie_submodule.ucs k N₂
theorem
lie_submodule.lcs_le_iff
{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]
{N₁ N₂ : lie_submodule R L M}
(k : ℕ) :
lie_submodule.lcs k N₁ ≤ N₂ ↔ N₁ ≤ lie_submodule.ucs k N₂
theorem
lie_submodule.gc_lcs_ucs
{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 : ℕ) :
galois_connection (λ (N : lie_submodule R L M), lie_submodule.lcs k N) (λ (N : lie_submodule R L M), lie_submodule.ucs k N)
theorem
lie_submodule.ucs_eq_top_iff
{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]
(N : lie_submodule R L M)
(k : ℕ) :
lie_submodule.ucs k N = ⊤ ↔ lie_module.lower_central_series R L M k ≤ N
theorem
lie_module.is_nilpotent_iff_exists_ucs_eq_top
{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_nilpotent R L M ↔ ∃ (k : ℕ), lie_submodule.ucs k ⊥ = ⊤
theorem
lie_submodule.ucs_comap_incl
{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]
(N : lie_submodule R L M)
(k : ℕ) :
theorem
lie_submodule.is_nilpotent_iff_exists_self_le_ucs
{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]
(N : lie_submodule R L M) :
lie_module.is_nilpotent R L ↥N ↔ ∃ (k : ℕ), N ≤ lie_submodule.ucs k ⊥
theorem
function.surjective.lie_module_lcs_map_eq
{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]
{L₂ : Type u_1}
{M₂ : Type u_2}
[lie_ring L₂]
[lie_algebra R L₂]
[add_comm_group M₂]
[module R M₂]
[lie_ring_module L₂ M₂]
[lie_module 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 ↑(lie_module.lower_central_series R L M k) = ↑(lie_module.lower_central_series R L₂ M₂ k)
theorem
function.surjective.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]
{L₂ : Type u_1}
{M₂ : Type u_2}
[lie_ring L₂]
[lie_algebra R L₂]
[add_comm_group M₂]
[module R M₂]
[lie_ring_module L₂ M₂]
[lie_module 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⁆)
[lie_module.is_nilpotent R L M] :
lie_module.is_nilpotent R L₂ M₂
theorem
equiv.lie_module_is_nilpotent_iff
{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]
{L₂ : Type u_1}
{M₂ : Type u_2}
[lie_ring L₂]
[lie_algebra R L₂]
[add_comm_group M₂]
[module R M₂]
[lie_ring_module L₂ M₂]
[lie_module R L₂ M₂]
(f : L ≃ₗ⁅R⁆ L₂)
(g : M ≃ₗ[R] M₂)
(hfg : ∀ (x : L) (m : M), ⁅⇑f x, ⇑g m⁆ = ⇑g ⁅x, m⁆) :
lie_module.is_nilpotent R L M ↔ lie_module.is_nilpotent R L₂ M₂
@[simp]
theorem
lie_module.is_nilpotent_of_top_iff
{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_nilpotent R ↥⊤ M ↔ lie_module.is_nilpotent R L M
@[protected, instance]
def
lie_algebra.is_solvable_of_is_nilpotent
(R : Type u)
(L : Type v)
[comm_ring R]
[lie_ring L]
[lie_algebra R L]
[hL : lie_module.is_nilpotent R L L] :
@[reducible]
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] :
theorem
lie_algebra.infi_max_gen_zero_eigenspace_eq_top_of_nilpotent
(R : Type u)
(L : Type v)
[comm_ring R]
[lie_ring L]
[lie_algebra R L]
[lie_algebra.is_nilpotent R L] :
(⨅ (x : L), (⇑(lie_algebra.ad R L) x).maximal_generalized_eigenspace 0) = ⊤
theorem
coe_lower_central_series_ideal_quot_eq
{R : Type u}
{L : Type v}
[comm_ring R]
[lie_ring L]
[lie_algebra R L]
{I : lie_ideal R L}
(k : ℕ) :
↑(lie_module.lower_central_series R L (L ⧸ I) k) = ↑(lie_module.lower_central_series 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
lie_module.coe_lower_central_series_ideal_le
{R : Type u}
{L : Type v}
[comm_ring R]
[lie_ring L]
[lie_algebra R L]
{I : lie_ideal R L}
(k : ℕ) :
↑(lie_module.lower_central_series R ↥I ↥I k) ≤ ↑(lie_module.lower_central_series 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
lie_algebra.nilpotent_of_nilpotent_quotient
{R : Type u}
{L : Type v}
[comm_ring R]
[lie_ring L]
[lie_algebra R L]
{I : lie_ideal R L}
(h₁ : I ≤ lie_algebra.center R L)
(h₂ : lie_algebra.is_nilpotent R (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]
[lie_algebra R L]
[nontrivial L]
[lie_algebra.is_nilpotent R L] :
theorem
lie_ideal.map_lower_central_series_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'} :
lie_ideal.map f (lie_module.lower_central_series R L L k) ≤ lie_module.lower_central_series R L' L' k
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) :
lie_ideal.map f (lie_module.lower_central_series R L L k) = lie_module.lower_central_series R L' L' k
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_hom.is_nilpotent_range
{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']
[lie_algebra.is_nilpotent R L]
(f : L →ₗ⁅R⁆ L') :
@[simp]
theorem
lie_algebra.is_nilpotent_range_ad_iff
{R : Type u}
{L : Type v}
[comm_ring R]
[lie_ring L]
[lie_algebra R L] :
lie_algebra.is_nilpotent R ↥((lie_algebra.ad R L).range) ↔ lie_algebra.is_nilpotent R L
Note that this result is not quite a special case of
lie_module.is_nilpotent_range_to_endomorphism_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.
@[protected, instance]
def
has_top.top.lie_algebra.is_nilpotent
{R : Type u}
{L : Type v}
[comm_ring R]
[lie_ring L]
[lie_algebra R L]
[h : lie_algebra.is_nilpotent R L] :
def
lie_ideal.lcs
{R : Type u_1}
{L : Type u_2}
[comm_ring R]
[lie_ring L]
[lie_algebra R L]
(I : lie_ideal R L)
(M : Type u_3)
[add_comm_group M]
[module R M]
[lie_ring_module L M]
[lie_module R L M]
(k : ℕ) :
lie_submodule 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
lie_module.lower_central_series 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 lie_ideal.coe_lcs_eq.
@[simp]
theorem
lie_ideal.lcs_zero
{R : Type u_1}
{L : Type u_2}
[comm_ring R]
[lie_ring L]
[lie_algebra R L]
(I : lie_ideal R L)
(M : Type u_3)
[add_comm_group M]
[module R M]
[lie_ring_module L M]
[lie_module R L M] :
@[simp]
theorem
lie_ideal.lcs_succ
{R : Type u_1}
{L : Type u_2}
[comm_ring R]
[lie_ring L]
[lie_algebra R L]
(I : lie_ideal R L)
(M : Type u_3)
[add_comm_group M]
[module R M]
[lie_ring_module L M]
[lie_module R L M]
(k : ℕ) :
theorem
lie_ideal.lcs_top
{R : Type u_1}
{L : Type u_2}
[comm_ring R]
[lie_ring L]
[lie_algebra R L]
(M : Type u_3)
[add_comm_group M]
[module R M]
[lie_ring_module L M]
[lie_module R L M]
(k : ℕ) :
⊤.lcs M k = lie_module.lower_central_series R L M k
theorem
lie_ideal.coe_lcs_eq
{R : Type u_1}
{L : Type u_2}
[comm_ring R]
[lie_ring L]
[lie_algebra R L]
(I : lie_ideal R L)
(M : Type u_3)
[add_comm_group M]
[module R M]
[lie_ring_module L M]
[lie_module R L M]
(k : ℕ) :
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) :
is_nilpotent (⇑(lie_algebra.ad R A) a)
theorem
lie_subalgebra.is_nilpotent_ad_of_is_nilpotent_ad
{R : Type u}
[comm_ring R]
{L : Type v}
[lie_ring L]
[lie_algebra R L]
(K : lie_subalgebra R L)
{x : ↥K}
(h : is_nilpotent (⇑(lie_algebra.ad R L) ↑x)) :
is_nilpotent (⇑(lie_algebra.ad R ↥K) x)
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) :
is_nilpotent (⇑(lie_algebra.ad R ↥L) x)