LieModule.nilpotentOfNilpotentQuotient
theorem LieModule.nilpotentOfNilpotentQuotient :
∀ (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] [inst_6 : LieModule R L M]
{N : LieSubmodule R L M},
N ≤ LieModule.maxTrivSubmodule R L M → LieModule.IsNilpotent R L (M ⧸ N) → LieModule.IsNilpotent R L M
The theorem `LieModule.nilpotentOfNilpotentQuotient` states that for any commutative ring `R`, Lie ring `L`, and Lie module `M`, and given a Lie submodule `N` that is a subset of the maximum trivial Lie submodule on which the Lie ring acts trivially, if the quotient of `M` by `N` is nilpotent, then `M` itself is also nilpotent. This theorem is the equivalent for Lie modules of the fact that a central extension of nilpotent Lie algebras is nilpotent.
More concisely: If a Lie module over a commutative ring is a quotient of a nilpotent Lie submodule acting trivially on it, then the Lie module is nilpotent.
|
LieSubmodule.lcs_succ
theorem LieSubmodule.lcs_succ :
∀ {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] (k : ℕ) (N : LieSubmodule R L M),
LieSubmodule.lcs (k + 1) N = ⁅⊤, LieSubmodule.lcs k N⁆
This theorem states that for any commutative ring `R`, Lie ring `L`, additive commutative group `M`, module `R M`, and Lie ring module `L M` along with a natural number `k` and a Lie submodule `N`, the Lie central series at (k + 1) for the Lie submodule N, denoted `LieSubmodule.lcs (k + 1) N`, is equivalent to the Lie bracket of the full module with the Lie central series at k for the Lie submodule N, denoted `⁅⊤, LieSubmodule.lcs k N⁆`. In other words, it tells us how to compute the next term in the Lie central series for a given Lie submodule.
More concisely: For any commutative ring `R`, Lie ring `L`, additive commutative group `M`, module `RM`, Lie ring module `LM`, natural number `k`, and Lie submodule `N`, we have `LieSubmodule.lcs (k + 1) N = {x ∈ LM ∣ [x, LieSubmodule.lcs k N] ∈ LieSubmodule.lcs k N}`.
|
LieModule.disjoint_lowerCentralSeries_maxTrivSubmodule_iff
theorem LieModule.disjoint_lowerCentralSeries_maxTrivSubmodule_iff :
∀ (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] [inst_6 : LieModule R L M]
[inst_7 : LieModule.IsNilpotent R L M],
Disjoint (LieModule.lowerCentralSeries R L M 1) (LieModule.maxTrivSubmodule R L M) ↔ LieModule.IsTrivial L M
The theorem `LieModule.disjoint_lowerCentralSeries_maxTrivSubmodule_iff` states that for a nilpotent Lie module `M` of a Lie algebra `L` over a commutative ring `R`, the first term in the lower central series of `M` contains a non-zero element on which `L` acts trivially if and only if the entire action of `L` on `M` is trivial. In other words, the intersection of the first term in the lower central series of `M` and the maximal trivial submodule of `M` is the bottom element of the lattice structure, if and only if the Lie module `M` is trivial. When `M` is the same as `L`, this theorem provides a useful characterisation of Abelian-ness for nilpotent Lie algebras.
More concisely: For a nilpotent Lie module M over a commutative ring R, the first term in its lower central series intersects the maximal trivial submodule trivially if and only if M is the trivial Lie module.
|
LieAlgebra.nilpotent_of_nilpotent_quotient
theorem LieAlgebra.nilpotent_of_nilpotent_quotient :
∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {I : LieIdeal R L},
I ≤ LieAlgebra.center R L → LieAlgebra.IsNilpotent R (L ⧸ I) → LieAlgebra.IsNilpotent R L
The theorem states that for any commutative ring `R` and any Lie algebra `L` over `R`, if `I` is a Lie ideal of `L` which is a subset of the center of `L`, and if the quotient of `L` by `I` is a nilpotent Lie algebra, then `L` itself is a nilpotent Lie algebra. Here, the center of a Lie algebra is defined as the set of elements that commute with all other elements, and a Lie algebra is defined to be nilpotent if it is nilpotent as a Lie module over itself via the adjoint representation.
More concisely: If `I` is a Lie ideal of a Lie algebra `L` over a commutative ring `R` that lies in the center of `L` and `L/I` is a nilpotent Lie algebra, then `L` is a nilpotent Lie algebra.
|
LieModule.lowerCentralSeries_zero
theorem LieModule.lowerCentralSeries_zero :
∀ (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],
LieModule.lowerCentralSeries R L M 0 = ⊤
The theorem `LieModule.lowerCentralSeries_zero` states that for any commutative ring `R`, any Lie ring `L`, and any additive commutative group `M` that is also a module over `R` and a Lie ring module over `L`, the zeroth term of the lower central series of Lie submodules of `M` is the entire module `M` itself, represented by `⊤`. In other words, in the context of Lie algebras, the base of the lower central series is the entire module.
More concisely: For any commutative ring R, Lie ring L, and additive commutative group M being an R-module and a Lie ring module over L, the zeroth term of the lower central series of Lie submodules of M is the entire module M.
|
coe_lowerCentralSeries_ideal_quot_eq
theorem coe_lowerCentralSeries_ideal_quot_eq :
∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {I : LieIdeal R L}
(k : ℕ), ↑(LieModule.lowerCentralSeries R L (L ⧸ I) k) = ↑(LieModule.lowerCentralSeries R (L ⧸ I) (L ⧸ I) k)
This theorem states that for a given ideal `I` of a Lie algebra `L`, the lower central series of the quotient algebra `L/I` is identical whether we regard `L/I` as a module over `L` or as a module over `L/I`. In other words, the sequence of submodules generated by iteratively taking the Lie bracket with the ideal `I`, does not depend on whether we treat `L/I` as a module over the original Lie algebra or the quotient algebra.
It's mentioned here that this result could be generalised, but such generalisation would necessitate the definition of morphisms between Lie modules over different Lie algebras, which is currently missing.
More concisely: The lower central series of a Lie algebra quotient is invariant under the choice of whether to view it as a Lie module over the original algebra or the quotient algebra.
|
LieSubmodule.ucs_le_of_normalizer_eq_self
theorem LieSubmodule.ucs_le_of_normalizer_eq_self :
∀ {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] [inst_6 : LieModule R L M]
{N₁ : LieSubmodule R L M}, N₁.normalizer = N₁ → ∀ (k : ℕ), LieSubmodule.ucs k ⊥ ≤ N₁
The theorem `LieSubmodule.ucs_le_of_normalizer_eq_self` states that for a given Lie module `M`, if it contains a self-normalizing Lie submodule `N₁`, then all terms of the upper central series of `M` are contained within `N₁`. An important application of this is when a Cartan subalgebra `H` is a subset of `L`, in which the roles of `L`, `M`, and `N` are played by `H`, `L`, and `H` respectively.
More concisely: If a Lie module contains a self-normalizing Lie submodule, then all terms of the upper central series of the module are contained within the submodule.
|
LieModule.nilpotencyLength_eq_succ_iff
theorem LieModule.nilpotencyLength_eq_succ_iff :
∀ (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] (k : ℕ),
LieModule.nilpotencyLength R L M = k + 1 ↔
LieModule.lowerCentralSeries R L M (k + 1) = ⊥ ∧ LieModule.lowerCentralSeries R L M k ≠ ⊥
This theorem states that for any commutative ring `R`, Lie ring `L`, and Lie module `M`, and for any natural number `k`, the nilpotency length of the module `M` is `k + 1` if and only if the `(k + 1)`-th term of the lower central series of `M` is the zero module and the `k`-th term of the series is not the zero module. The nilpotency length of a module is the number of inclusions in the lower central series until reaching the zero module, and the lower central series is a sequence of nested submodules of `M` defined using Lie bracket operations.
More concisely: For any commutative ring `R`, Lie ring `L`, and Lie module `M` over `L`, the nilpotency length of `M` is `k+1` if and only if the `(k+1)`-th term of its lower central series is the zero module but the `k`-th term is not.
|
LieSubmodule.ucs_succ
theorem LieSubmodule.ucs_succ :
∀ {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] [inst_6 : LieModule R L M]
(N : LieSubmodule R L M) (k : ℕ), LieSubmodule.ucs (k + 1) N = (LieSubmodule.ucs k N).normalizer
The theorem `LieSubmodule.ucs_succ` states that for any commutative ring `R`, Lie ring `L`, additive commutative group `M`, module `M` over `R`, Lie ring module `M` over `L`, and Lie module `M` over the Lie algebra `L` with coefficients in the ring `R`, any Lie submodule `N` of `M` over the Lie algebra `L` with coefficients in the ring `R`, and any natural number `k`, the `k + 1`-th term of the upper central series of `N` equals the normalizer of the `k`-th term of the upper central series of `N` in the Lie algebra `L` with coefficients in the ring `R`.
In simpler terms, this theorem establishes a recursive relationship for calculating the terms of the upper central series of a Lie submodule.
More concisely: For any Lie submodule `N` of a Lie module `M` over a Lie algebra `L` with coefficients in a commutative ring `R`, the `(k+1)`-th term of the upper central series of `N` is the normalizer of the `k`-th term in `L` for all natural numbers `k`.
|
LieAlgebra.isNilpotent_range_ad_iff
theorem LieAlgebra.isNilpotent_range_ad_iff :
∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L],
LieAlgebra.IsNilpotent R ↥(LieAlgebra.ad R L).range ↔ LieAlgebra.IsNilpotent R L
This theorem states that for any commutative ring `R` and any Lie algebra `L` over `R`, the Lie algebra `L` is nilpotent if and only if the range of the adjoint representation of `L` is nilpotent. Here, nilpotency of a Lie algebra is defined in terms of its structure as a Lie module over itself via the adjoint representation. The result should not be confused with `LieModule.isNilpotent_range_toEndomorphism_iff`, which is about the nilpotency of the module `L` under the action of the range of the adjoint representation, whereas this theorem deals with the nilpotency of the range of the adjoint representation acting on itself.
More concisely: A Lie algebra over a commutative ring is nilpotent if and only if the range of its adjoint representation is nilpotent as a Lie algebra.
|
LieModule.antitone_lowerCentralSeries
theorem LieModule.antitone_lowerCentralSeries :
∀ (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],
Antitone (LieModule.lowerCentralSeries R L M)
This theorem states that the lower central series of Lie submodules of a Lie module, defined over a commutative ring, a Lie ring, and an abelian additive group, is an antitone function. In simpler terms, if `k ≤ l` for natural numbers `k` and `l`, then `LieModule.lowerCentralSeries R L M l ≤ LieModule.lowerCentralSeries R L M k`. This means that as we move up in the sequence (increasing the natural number), the corresponding Lie submodules in the lower central series become smaller or stay the same.
More concisely: The lower central series of a Lie module over a commutative ring is an antitone function with respect to the natural number indices.
|
LieModule.isNilpotent_iff
theorem LieModule.isNilpotent_iff :
∀ (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],
LieModule.IsNilpotent R L M ↔ ∃ k, LieModule.lowerCentralSeries R L M k = ⊥
This theorem is about Lie modules and is in the context of Lie algebras. It states that a Lie module `M`, over a commutative ring `R` and a Lie ring `L`, is nilpotent if and only if there exists a positive integer `k` such that the `k`th term of the lower central series of the Lie module is the bottom element, denoted by `⊥`. The lower central series of a Lie module is a sequence of Lie submodules, where each term is derived from the previous one in a specific way. In this case, the bottom element usually signifies the zero submodule in the context of Lie algebras.
More concisely: A Lie module over a commutative ring and a Lie ring is nilpotent if and only if its lower central series has order equal to the identity element after some term.
|
LieModule.coe_lowerCentralSeries_ideal_le
theorem LieModule.coe_lowerCentralSeries_ideal_le :
∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {I : LieIdeal R L}
(k : ℕ), ↑(LieModule.lowerCentralSeries R (↥↑I) (↥↑I) k) ≤ ↑(LieModule.lowerCentralSeries R L (↥↑I) k)
This theorem states that for any commutative ring `R`, any Lie ring `L` equipped with a Lie algebra structure over `R`, and any Lie ideal `I` of `L`, for any natural number `k`, the `k`th term of the lower central series of the Lie module `I` over `I` is a subobject of the `k`th term of the lower central series of the Lie module `I` over `L`. Note that this inclusion can be strict. For example, when considering the ideal of strictly-upper-triangular 2x2 matrices inside the Lie algebra of upper-triangular 2x2 matrices with `k = 1`.
More concisely: For any commutative ring `R`, any Lie ring `L` over `R` with Lie ideal `I`, the `k`th term of the lower central series of `I` as a Lie module over `I` is included in the `k`th term of the lower central series of `I` as a Lie module over `L`.
|
Mathlib.Algebra.Lie.Nilpotent._auxLemma.5
theorem Mathlib.Algebra.Lie.Nilpotent._auxLemma.5 :
∀ {α : Type u} [inst : LE α] [inst_1 : OrderTop α] {a : α}, (a ≤ ⊤) = True
This theorem, from the Mathlib library in the Algebra.Lie.Nilpotent module, states that for any type `α` that has a less than or equal to (`LE`) operation and an element called `OrderTop` (representing the maximum possible value), any element `a` of type `α` is less than or equal to this maximum value. In mathematical terms, this is saying for all `a` in `α`, `a ≤ ⊤` is always true.
More concisely: For any type `α` with a `LE` order and an `OrderTop` element, every `a` in `α` satisfies `a ≤ OrderTop`.
|
LieModule.lowerCentralSeries_succ
theorem LieModule.lowerCentralSeries_succ :
∀ (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] (k : ℕ),
LieModule.lowerCentralSeries R L M (k + 1) = ⁅⊤, LieModule.lowerCentralSeries R L M k⁆
The theorem `LieModule.lowerCentralSeries_succ` is a statement about the structure of the lower central series of a Lie module. Specifically, it states that for any commutative ring `R`, Lie ring `L`, and additive commutative group `M`, where `M` is a `R`-module and a `L`-module, the `(k + 1)`-th term of the lower central series is generated by the Lie bracket operation on the `k`-th term and the Lie algebra's whole space. This theorem is fundamental in the study of the structure of Lie algebras and their associated modules.
More concisely: For any commutative ring `R`, Lie ring `L`, and additive abelian group `M` being an `R`-module and `L`-module, the lower central series of `M` as a Lie module is generated by the Lie brackets of `M` with itself and the whole space of `M`.
|