LieModule.finite_weightSpace_ne_bot
theorem LieModule.finite_weightSpace_ne_bot :
∀ (R : Type u_2) (L : Type u_3) (M : Type u_4) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
[inst_3 : LieAlgebra.IsNilpotent R L] [inst_4 : AddCommGroup M] [inst_5 : Module R M] [inst_6 : LieRingModule L M]
[inst_7 : LieModule R L M] [inst_8 : NoZeroSMulDivisors R M] [inst_9 : IsNoetherian R M],
{χ | LieModule.weightSpace M χ ≠ ⊥}.Finite
The theorem `LieModule.finite_weightSpace_ne_bot` states that for any commutative ring `R`, any Lie ring `L`, and any module `M` over `R`, if `L` is a nilpotent Lie algebra over `R`, `M` is an additive commutative group and a module over `R`, `L` acts on `M` making `M` a Lie module over `L` under `R`, `R` has no zero divisors when scalar multiplying `M`, and `M` is a Noetherian module over `R`, then the set of linear functionals (or weights) `χ` such that the weight space of `M` under `χ` is not the zero submodule is finite. In other words, there are only finitely many weights that give non-zero weight spaces, under the given conditions.
More concisely: Given a commutative ring R, a Lie ring L over R, and an R-module M making M a Lie module over L under R such that L is nilpotent, M is a Noetherian, commutative additive group, and R has no zero divisors when scalar multiplying M, the set of weights χ for which the weight space of M under χ is non-zero is finite.
|
LieModule.isNilpotent_toEndomorphism_weightSpace_zero
theorem LieModule.isNilpotent_toEndomorphism_weightSpace_zero :
∀ {R : Type u_2} {L : Type u_3} (M : Type u_4) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
[inst_3 : LieAlgebra.IsNilpotent R L] [inst_4 : AddCommGroup M] [inst_5 : Module R M] [inst_6 : LieRingModule L M]
[inst_7 : LieModule R L M] [inst_8 : IsNoetherian R M] (x : L),
IsNilpotent ((LieModule.toEndomorphism R L ↥↑(LieModule.weightSpace M 0)) x)
The theorem `LieModule.isNilpotent_toEndomorphism_weightSpace_zero` states that for any commutative ring `R`, Lie ring `L` and a type `M`, if `L` is a nilpotent Lie algebra over `R`, and `M` is a Noetherian `R`-module that also forms a Lie module over `L`, then the action of any element of `L` on the zero weight space of `M` is a nilpotent endomorphism. In other words, there exists a natural number `n` such that applying the action `n` times results in the zero transformation. This captures a key property of nilpotent Lie algebras acting on Noetherian Lie modules.
More concisely: Given a commutative ring `R`, a Lie ring `L` over `R`, and a Noetherian `R`-module `M` that is also a Lie module over `L`, if `L` is nilpotent then any endomorphism of the zero weight space of `M` induced by an element of `L` is nilpotent.
|
LieModule.zero_weightSpace_eq_top_of_nilpotent'
theorem LieModule.zero_weightSpace_eq_top_of_nilpotent' :
∀ {R : Type u_2} {L : Type u_3} (M : Type u_4) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
[inst_3 : LieAlgebra.IsNilpotent R L] [inst_4 : AddCommGroup M] [inst_5 : Module R M] [inst_6 : LieRingModule L M]
[inst_7 : LieModule R L M] [inst_8 : LieModule.IsNilpotent R L M], LieModule.weightSpace M 0 = ⊤
This theorem states that for any type `M` (which has the structure of an additive commutative group, a `R`-module, a Lie ring module over `L`, and a Lie module over `L`), if the Lie module `L` over itself and `M` over `L` are both nilpotent, then the zero weight space of `M` is the entire space (denoted by `⊤`). Specifically, this result refers to the situation where `L` is a nilpotent Lie algebra, and `M` is a nilpotent module over `L`. The weight space of `M` at `0` being the entire space means that every element of `M` is annihilated by some sufficiently high power of the adjoint action of `L`.
More concisely: If `L` is a nilpotent Lie algebra and `M` is a nilpotent Lie module over `L`, then the zero weight space of `M` equals the entire space if and only if `L` and `M` are both nilpotent as Lie modules over themselves.
|
LieModule.iInf_lowerCentralSeries_eq_posFittingComp
theorem LieModule.iInf_lowerCentralSeries_eq_posFittingComp :
∀ (R : Type u_2) (L : Type u_3) (M : Type u_4) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
[inst_3 : LieAlgebra.IsNilpotent R L] [inst_4 : AddCommGroup M] [inst_5 : Module R M] [inst_6 : LieRingModule L M]
[inst_7 : LieModule R L M] [inst_8 : IsNoetherian R M] [inst_9 : IsArtinian R M],
⨅ k, LieModule.lowerCentralSeries R L M k = LieModule.posFittingComp R L M
This theorem states that for any commutative ring `R`, Lie ring `L`, and module `M` over `R`, if `L` is a nilpotent Lie algebra over `R`, `M` is an additive commutative group and a module over `R`, `M` becomes a Lie ring module under `L`, and `M` is a Lie module under `L` and `R`, in addition to `M` being Noetherian and Artinian, then the infimum of the lower central series of Lie submodules of `M` over all natural numbers `k` is equal to the positive fitting component of the Lie module. The positive fitting component of a module is a particular submodule associated to it, and the lower central series of a module is a descending sequence of submodules. Noetherian and Artinian conditions are properties of modules related to their submodules; a Noetherian module has the ascending chain condition, and an Artinian module has the descending chain condition.
More concisely: For any commutative ring `R`, Lie ring `L` over `R`, and Noetherian and Artinian module `M` over `R` that is both a Lie ring module and a Lie module under `L` and `R`, the infimum of the lower central series of Lie submodules of `M` equals the positive fitting component of `M`.
|
LieModule.iSup_ucs_eq_weightSpace_zero
theorem LieModule.iSup_ucs_eq_weightSpace_zero :
∀ (R : Type u_2) (L : Type u_3) (M : Type u_4) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
[inst_3 : LieAlgebra.IsNilpotent R L] [inst_4 : AddCommGroup M] [inst_5 : Module R M] [inst_6 : LieRingModule L M]
[inst_7 : LieModule R L M] [inst_8 : IsNoetherian R M], ⨆ k, LieSubmodule.ucs k ⊥ = LieModule.weightSpace M 0
This theorem, `LieModule.iSup_ucs_eq_weightSpace_zero`, states that for any given commutative ring R, Lie ring L, and type M, provided that L is a nilpotent Lie algebra over R, M is an additive commutative group and a module over R, L is a Lie ring module over M, and M is a Noetherian R-module, the supremum of the ascending central series of the zero Lie submodule is equal to the zero weight space of M. In mathematical terms, this could be expressed as: for a nilpotent Lie algebra, the top of the upper central series of the trivial module is the zero weight space.
More concisely: For a nilpotent Lie algebra L over a commutative ring R, the supremum of the ascending central series of the trivial module coincides with the zero weight space of L as an L-module.
|
LieModule.isCompl_weightSpace_zero_posFittingComp
theorem LieModule.isCompl_weightSpace_zero_posFittingComp :
∀ (R : Type u_2) (L : Type u_3) (M : Type u_4) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
[inst_3 : LieAlgebra.IsNilpotent R L] [inst_4 : AddCommGroup M] [inst_5 : Module R M] [inst_6 : LieRingModule L M]
[inst_7 : LieModule R L M] [inst_8 : IsNoetherian R M] [inst_9 : IsArtinian R M],
IsCompl (LieModule.weightSpace M 0) (LieModule.posFittingComp R L M)
This theorem, known as the "Fitting decomposition of the Lie module `M`", states that for any commutative ring `R`, any Lie ring `L`, and any module `M`, given the conditions that `L` is a nilpotent Lie algebra over `R`, `M` is an additive commutative group and a module over `R`, `M` is a Lie ring module over `L`, `M` is a Lie module over the Lie algebra `L` and `R`, `M` is Noetherian over `R`, and `M` is Artinian over `R`, the weight space of `M` at zero and the positive Fitting component of `M` are complementary subspaces (i.e., their sum is the whole space and their intersection is the zero subspace).
More concisely: Given a commutative ring R, a Lie ring L over R, and an additive commutative group and R-module M that is a Lie module over L and over R, Noetherian, Artinian, and a Lie ring module over L, the weight space of M at zero and its positive Fitting component have zero intersection and sum up to M.
|