LieAlgebra.isNilpotent_iff_forall
theorem LieAlgebra.isNilpotent_iff_forall :
∀ {R : Type u₁} {L : Type u₂} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
[inst_3 : IsNoetherian R L], LieAlgebra.IsNilpotent R L ↔ ∀ (x : L), IsNilpotent ((LieAlgebra.ad R L) x)
Engel's theorem states that for any Lie algebra `L` over a commutative ring `R`, where `R` is Noetherian and `L` is a Lie ring, `L` is nilpotent if and only if every element `x` of `L` is nilpotent in the adjoint representation. In other words, a Lie algebra is nilpotent if and only if for every element in the algebra, some natural number power of its adjoint action equals zero.
More concisely: A Lie algebra over a Noetherian commutative ring is nilpotent if and only if every element's adjoint representation is nilpotent.
|
LieModule.isNilpotent_iff_forall
theorem LieModule.isNilpotent_iff_forall :
∀ {R : Type u₁} {L : Type u₂} {M : Type u₄} [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 : IsNoetherian R L],
LieModule.IsNilpotent R L M ↔ ∀ (x : L), IsNilpotent ((LieModule.toEndomorphism R L M) x)
Engel's theorem states that for any given types `R`, `L`, and `M` where `R` is a commutative ring, `L` is a Lie ring, and `M` is an additively commutative group that is also a module over `R` and a Lie ring module over `L`. Additionally, if `M` is a Lie module over `R`, `L`, and itself, and `L` is Noetherian over `R`, then `M` is nilpotent as a Lie module if and only if every endomorphism of `M` induced by an element of `L` (obtained via the `LieModule.toEndomorphism` function) is a nilpotent element. Here, a nilpotent element is defined as an element such that some natural number power of it equals zero. Thus, this theorem connects the nilpotency of a Lie module with the nilpotency of its endomorphisms.
More concisely: Engel's theorem states that a Lie module over a commutative ring and a Lie ring is nilpotent if and only if every endomorphism of it induced by an element of the Lie ring is a nilpotent element.
|
LieAlgebra.isEngelian_of_isNoetherian
theorem LieAlgebra.isEngelian_of_isNoetherian :
∀ {R : Type u₁} {L : Type u₂} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
[inst_3 : IsNoetherian R L], LieAlgebra.IsEngelian R L
The theorem `LieAlgebra.isEngelian_of_isNoetherian` in Lean 4 is a formulation of Engel's theorem. Specifically, it states that if you have a type `R` representing a commutative ring, and a type `L` representing a Lie algebra over `R`, and if this Lie algebra is Noetherian, then the Lie algebra is Engelian. This version of Engel's theorem implies all traditional forms of Engel's theorem via `LieModule.nontrivial_max_triv_of_isNilpotent`, `LieModule.isNilpotent_iff_forall`, and `LieAlgebra.isNilpotent_iff_forall`.
More concisely: If `L` is a Lie algebra over a commutative ring `R` and `L` is Noetherian, then `L` is Engelian.
|
LieModule.isNilpotent_iff_forall'
theorem LieModule.isNilpotent_iff_forall' :
∀ {R : Type u₁} {L : Type u₂} {M : Type u₄} [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 : IsNoetherian R M],
LieModule.IsNilpotent R L M ↔ ∀ (x : L), IsNilpotent ((LieModule.toEndomorphism R L M) x)
Engel's theorem, as stated in this Lean 4 theorem, asserts that for any types `R`, `L`, and `M` where `R` is a commutative ring, `L` is a Lie ring, `M` is a module over `R` which is also an additive commutative group, `L` is a Lie algebra over `R`, `M` is a Lie ring-module over `L`, and `M` is also a Lie module over `R` and `L`, under the assumption that `M` is Noetherian over `R`, the Lie module `M` is nilpotent if and only if for all elements `x` in `L`, the endomorphism of `M` induced by `x` is nilpotent in the sense that some power of it equals zero. In the context of the theorem, nilpotency of an element means that there exists some natural number `n` such that raising the element to the `n`-th power yields zero.
More concisely: Engel's theorem states that a Lie module over a commutative ring is nilpotent if and only if the endomorphism of the module induced by each element in the Lie algebra is nilpotent.
|