LieAlgebra.isSemisimple_iff_no_abelian_ideals
theorem LieAlgebra.isSemisimple_iff_no_abelian_ideals :
∀ (R : Type u) (L : Type v) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L],
LieAlgebra.IsSemisimple R L ↔ ∀ (I : LieIdeal R L), IsLieAbelian ↥↑I → I = ⊥
The theorem states that for any commutative ring `R` and any Lie ring `L` that is also a Lie algebra over `R`, the Lie algebra is semisimple if and only if for every Lie ideal `I` of this algebra, if `I` is Abelian (i.e., it is trivial as a Lie module over itself), then `I` must be the zero ideal. In other words, a Lie algebra is semisimple if it does not have any non-zero Abelian ideals.
More concisely: A Lie algebra over a commutative ring is semisimple if and only if it has no non-zero Abelian Lie ideals.
|
LieAlgebra.subsingleton_of_semisimple_lie_abelian
theorem LieAlgebra.subsingleton_of_semisimple_lie_abelian :
∀ (R : Type u) (L : Type v) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
[inst : LieAlgebra.IsSemisimple R L] [h : IsLieAbelian L], Subsingleton L
This theorem states that if `L` is a Lie algebra over a commutative ring `R`, which is also both semisimple and Abelian, then `L` is trivial, meaning it contains only one element. In mathematical terms, this can be written as, for any type `L` that has the structure of a Lie ring, a Lie algebra over a commutative ring `R`, and which is semisimple and Abelian, `L` is a singleton.
More concisely: A semisimple and Abelian Lie algebra over a commutative ring is trivial, i.e., it consists of only one element.
|
LieAlgebra.abelian_radical_iff_solvable_is_abelian
theorem LieAlgebra.abelian_radical_iff_solvable_is_abelian :
∀ (R : Type u) (L : Type v) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
[inst_3 : IsNoetherian R L],
IsLieAbelian ↥↑(LieAlgebra.radical R L) ↔ ∀ (I : LieIdeal R L), LieAlgebra.IsSolvable R ↥↑I → IsLieAbelian ↥↑I
This theorem states that in the context of a commutative ring R and a Lie algebra L over R, with the assumption that L is Noetherian over R, the following two properties are equivalent:
1. The radical of the Lie algebra L is Abelian. Here, the radical of a Lie algebra is defined as the supremum of all its solvable ideals, and an algebra is called Abelian if it is trivial as a module over itself.
2. For every ideal I of the Lie algebra, if this ideal is solvable, then it is also Abelian.
These two properties can serve as possible definitions for a Lie algebra to be reductive. However, it's worth noting that there's no consensus on the definition of 'reductive' when the coefficients are not a field of characteristic zero.
More concisely: In a commutative ring R and a Noetherian Lie algebra L over R, the radical of L is Abelian if and only if every solvable ideal of L is Abelian.
|