Mathlib.Algebra.Lie.Normalizer._auxLemma.1
theorem Mathlib.Algebra.Lie.Normalizer._auxLemma.1 :
∀ {R : Type u_1} {L : Type u_2} {M : Type u_3} [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]
(N : LieSubmodule R L M) (m : M), (m ∈ N.normalizer) = ∀ (x : L), ⁅x, m⁆ ∈ N
This theorem from the Mathlib library, specifically from the Algebra.Lie.Normalizer module, states that for any given commutative ring `R`, Lie ring `L`, and additive commutative group `M` that has a `R` module, a Lie `L` ring module, and is a Lie module over `R` and `L`, a certain condition holds. This condition is that for any Lie submodule `N` of `M` and any element `m` of `M`, `m` is in the normalizer of `N` if and only if for every element `x` of `L`, the Lie bracket of `x` and `m` is an element of `N`. In LaTeX mathematics, this is expressed as \(m \in \text{N.normalizer} \Leftrightarrow \forall x \in L, [x,m] \in N\).
More concisely: A Lie ring module M over a commutative ring R, which is also a Lie module over M and has a given Lie submodule N, satisfies the condition that an element m of M is in the normalizer of N if and only if the Lie bracket [x,m] of any x in L lies in N.
|
LieSubalgebra.exists_nested_lieIdeal_ofLe_normalizer
theorem LieSubalgebra.exists_nested_lieIdeal_ofLe_normalizer :
∀ {R : Type u_1} {L : Type u_2} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
{H K : LieSubalgebra R L} (h₁ : H ≤ K),
K ≤ H.normalizer → ∃ I, lieIdealSubalgebra R (↥K) I = LieSubalgebra.ofLe h₁
This theorem states that for any commutative ring `R` and any Lie algebra `L` over `R`, given two Lie subalgebras `H` and `K` of `L` such that `H` is a subset of `K` (`H ≤ K`), if `K` is also a subset of the normalizer of `H` (`K ≤ H.normalizer`), then there exists a Lie ideal `I` such that `I` viewed as a Lie subalgebra of `K` equals to `H` viewed as a Lie subalgebra of `K`. In other words, a Lie subalgebra `H` is an ideal of any Lie subalgebra `K` that contains `H` and is also contained in the normalizer of `H`.
More concisely: If `H` is a Lie subalgebra of a Lie algebra `L` over a commutative ring `R`, and `K` is a Lie subalgebra of `L` containing `H` and contained in `H.normalizer`, then `H` and `I`, where `I` is the ideal generated by `H` in `K`, are equal as Lie subalgebras.
|
LieSubalgebra.ideal_in_normalizer
theorem LieSubalgebra.ideal_in_normalizer :
∀ {R : Type u_1} {L : Type u_2} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
{H : LieSubalgebra R L} {x y : L}, x ∈ H.normalizer → y ∈ H → ⁅x, y⁆ ∈ H
The theorem `LieSubalgebra.ideal_in_normalizer` states that for any commutative ring `R` and any Lie ring `L` with the corresponding Lie algebra structure, and for any Lie subalgebra `H` of `L`, for any two elements `x` and `y` of `L`, if `x` belongs to the normalizer of `H` and `y` belongs to `H`, then the Lie bracket of `x` and `y`, denoted as `⁅x, y⁆`, will belong to `H`. In other words, it asserts that a Lie subalgebra is an ideal of its normalizer.
More concisely: The normalizer of a Lie subalgebra is an ideal in the sense that any Lie bracket of an element from the normalizer with an element from the subalgebra lies in the subalgebra.
|