LieSubmodule.trivial_lie_oper_zero
theorem LieSubmodule.trivial_lie_oper_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] (N : LieSubmodule R L M)
(I : LieIdeal R L) [inst_6 : LieModule.IsTrivial L M], ⁅I, N⁆ = ⊥
This theorem states that for any commutative ring `R`, Lie ring `L`, additively commutative group `M`, where `L` forms a Lie algebra over `R` and `M` is a `R`-module and a `L`-Lie ring module, any Lie submodule `N` of the Lie module, and any Lie ideal `I` of `L`, if `M` is a trivial Lie module over `L`, then the Lie bracket of the Lie ideal `I` and the Lie submodule `N` equals the zero submodule.
In other words, when `M` is a trivial Lie module over `L`, the action of any element from the Lie ideal on any element from the Lie submodule reduces to zero. This essentially means that in this context, the elements of the Lie ideal act trivially on the Lie submodule.
More concisely: If `L` is a Lie algebra over a commutative ring `R`, `M` is an additively commutative `R`-module and a `L`-Lie ring module, `N` is a Lie submodule of the Lie module `M`, and `I` is a Lie ideal of `L`, then `N` is a trivial `L`-Lie module over `L` implies `[I, N] = {0}`, where `[I, N]` denotes the Lie bracket of `I` and `N`.
|
Mathlib.Algebra.Lie.Abelian._auxLemma.5
theorem Mathlib.Algebra.Lie.Abelian._auxLemma.5 :
∀ (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] (m : M),
(m ∈ LieModule.maxTrivSubmodule R L M) = ∀ (x : L), ⁅x, m⁆ = 0
This theorem, from the Mathlib library for Lean, states that for any types `R`, `L`, and `M`, under the conditions that `R` is a commutative ring, `L` is a Lie ring, `M` is an additive commutative group and a module over `R`, `M` is a Lie ring module for `L`, and `M` is a Lie module for `R` and `L`, an element `m` of `M` belongs to the maximal trivial submodule of the Lie module if and only if for all elements `x` of `L`, the Lie bracket of `x` and `m` is zero.
In mathematical terms, this theorem is about the structure of Lie algebras, a key concept in the theory of algebraic structures. Specifically, it characterizes the elements of the maximal trivial submodule of a Lie module in terms of the Lie bracket operation.
More concisely: An element of a Lie module over a commutative ring is in the maximal trivial submodule if and only if the Lie bracket of any element in the Lie algebra with that element is zero.
|