LieAlgebra.derivedSeriesOfIdeal_le_self
theorem LieAlgebra.derivedSeriesOfIdeal_le_self :
∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (I : LieIdeal R L)
(k : ℕ), LieAlgebra.derivedSeriesOfIdeal R L k I ≤ I
The theorem `LieAlgebra.derivedSeriesOfIdeal_le_self` states that for any commutative ring `R` and a Lie ring `L` that has a structure of a Lie algebra over `R`, for any Lie ideal `I` of `L` and any natural number `k`, the `k`-th derived series of the Lie ideal `I` is a subset of `I` itself. In other words, applying the derived series operation `k` times to the Lie ideal `I` will not produce any elements outside `I`.
More concisely: For any commutative ring R, Lie algebra L over R, Lie ideal I of L, and natural number k, the k-th derived series of I is contained in I.
|
LieAlgebra.derivedSeriesOfIdeal_le
theorem LieAlgebra.derivedSeriesOfIdeal_le :
∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {I J : LieIdeal R L}
{k l : ℕ}, I ≤ J → l ≤ k → LieAlgebra.derivedSeriesOfIdeal R L k I ≤ LieAlgebra.derivedSeriesOfIdeal R L l J
The theorem `LieAlgebra.derivedSeriesOfIdeal_le` states that for any commutative ring `R`, any Lie ring `L`, any Lie algebra `L` over `R`, and any two Lie ideals `I` and `J` of this Lie algebra, along with two natural numbers `k` and `l`, if Lie ideal `I` is a subset of Lie ideal `J` and `l` is less than or equal to `k`, then the `k`-th derived series of the ideal `I` is a subset of the `l`-th derived series of the ideal `J`. In other words, this theorem shows a monotonic property of the derived series of an ideal in a Lie algebra: The derived series of a smaller ideal and higher order is contained in the derived series of a larger ideal and lower order.
More concisely: For any commutative ring R, Lie ring L, Lie algebra L over R, Lie ideals I and J of L, and natural numbers k ≥ l, if I ⊆ J and k ≤ l then d^k(I) ⊆ d^l(J), where d^i denotes the i-th derived series of an ideal.
|
LieAlgebra.derivedSeriesOfIdeal_zero
theorem LieAlgebra.derivedSeriesOfIdeal_zero :
∀ (R : Type u) (L : Type v) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (I : LieIdeal R L),
LieAlgebra.derivedSeriesOfIdeal R L 0 I = I
The theorem `LieAlgebra.derivedSeriesOfIdeal_zero` states that for any given commutative ring `R`, Lie ring `L` and a corresponding Lie algebra, and an ideal `I` of the Lie algebra, the zeroth term of the derived series of the ideal `I` is the ideal `I` itself. In other words, the initial term of the derived series of an ideal in a Lie algebra is the ideal itself.
More concisely: The zeroth term of the derived series of an ideal in a Lie algebra is the ideal itself.
|
LieAlgebra.LieIdeal.solvable_iff_le_radical
theorem LieAlgebra.LieIdeal.solvable_iff_le_radical :
∀ (R : Type u) (L : Type v) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
[inst_3 : IsNoetherian R L] (I : LieIdeal R L), LieAlgebra.IsSolvable R ↥↑I ↔ I ≤ LieAlgebra.radical R L
The theorem `LieAlgebra.LieIdeal.solvable_iff_le_radical` states that for any commutative ring `R`, Lie ring `L` and Lie algebra structure on `L` over `R`, if `L` is Noetherian over `R`, then any Lie ideal `I` of this Lie algebra is solvable if and only if `I` is a subideal of the radical of the Lie algebra. In other words, a Lie ideal is solvable precisely when it is contained within the radical of the Lie algebra, under the condition that the Lie algebra is Noetherian.
More concisely: A Lie ideal of a Noetherian Lie algebra over a commutative ring is solvable if and only if it is contained in the radical of the Lie algebra.
|
LieAlgebra.derivedSeriesOfIdeal_succ
theorem LieAlgebra.derivedSeriesOfIdeal_succ :
∀ (R : Type u) (L : Type v) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (I : LieIdeal R L)
(k : ℕ),
LieAlgebra.derivedSeriesOfIdeal R L (k + 1) I =
⁅LieAlgebra.derivedSeriesOfIdeal R L k I, LieAlgebra.derivedSeriesOfIdeal R L k I⁆
The theorem `LieAlgebra.derivedSeriesOfIdeal_succ` states that for any commutative ring `R`, any Lie ring `L` which is also a Lie algebra over `R`, any Lie ideal `I` of `L`, and any natural number `k`, the (k + 1)-th derived series of the Lie ideal `I` is equal to the Lie bracket of the k-th derived series of `I` with itself. In mathematical terms, it says that if we define a sequence inductively where the next element is the Lie bracket of the current element with itself, then this sequence corresponds exactly to the derived series of the Lie ideal.
More concisely: For any commutative ring R, Lie algebra L over R, Lie ideal I of L, and natural number k, the (k+1)-th derived series of I equals the Lie bracket of the k-th derived series of I.
|