LieModule.traceForm_apply_lie_apply'
theorem LieModule.traceForm_apply_lie_apply' :
∀ (R : Type u_1) (L : Type u_3) (M : Type u_4) [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]
(x y z : L), ((LieModule.traceForm R L M) ⁅x, y⁆) z = -((LieModule.traceForm R L M) y) ⁅x, z⁆
This theorem states that given a representation `M` of a Lie algebra `L` over a commutative ring `R`, the action of any element `x : L` is skew-adjoint with respect to the trace form. In particular, for any elements `x`, `y`, and `z` of `L`, the action of the Lie bracket of `x` and `y` on `z` under the trace form is equal to the negation of the action of `y` on the Lie bracket of `x` and `z` under the same form.
More concisely: Given a Lie algebra `L` over a commutative ring `R` and a representation `M` of `L`, the trace form is skew-adjoint with respect to the Lie algebra multiplication, that is, for all `x, y, z ∈ L`, `Tr(x [y, z]) = -Tr(y [x, z])`.
|
LieModule.isLieAbelian_of_ker_traceForm_eq_bot
theorem LieModule.isLieAbelian_of_ker_traceForm_eq_bot :
∀ (R : Type u_1) (L : Type u_3) (M : Type u_4) [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 : Module.Free R M] [inst_8 : Module.Finite R M] [inst_9 : LieAlgebra.IsNilpotent R L]
[inst_10 : IsDomain R] [inst_11 : IsPrincipalIdealRing R],
LinearMap.ker (LieModule.traceForm R L M) = ⊥ → IsLieAbelian L
This theorem states that for a given Commutative Ring `R`, Lie Ring `L`, and Additive Commutative Group `M` with appropriate modules, Lie ring modules, and Lie algebra structures, if the Lie algebra is nilpotent and `R` is both a domain and a principal ideal ring, then if the kernel of the trace form of the Lie module is trivial (denoted by the bottom element `⊥`), the Lie algebra `L` is Abelian. In simpler terms, a nilpotent Lie algebra with a representation whose trace form is non-singular (i.e., has no nontrivial kernel) is always Abelian.
More concisely: If `R` is a commutative domain and principal ideal ring, `L` is a nilpotent Lie algebra over a commutative ring `R`, and `M` is an `R`-Lie module with a non-singular trace form, then `L` is an Abelian Lie algebra.
|
LieModule.traceForm_apply_lie_apply
theorem LieModule.traceForm_apply_lie_apply :
∀ (R : Type u_1) (L : Type u_3) (M : Type u_4) [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]
(x y z : L), ((LieModule.traceForm R L M) ⁅x, y⁆) z = ((LieModule.traceForm R L M) x) ⁅y, z⁆
This theorem states that for any given commutative ring `R`, Lie ring `L`, and additive commutative group `M` that is also `R`-module, if `L` acts on `M` as a Lie module, then the trace form of this Lie module behaves nicely with respect to the action of the Lie algebra. Specifically, applying the trace form to the Lie bracket of `x` and `y` (from `L`), and then to `z` (also from `L`), is the same as first applying the trace form to `x` and then to the Lie bracket of `y` and `z`. This property illustrates how the trace form interacts with the Lie bracket operation.
More concisely: For any commutative ring `R`, Lie ring `L`, and `R`-module `M` that is also a Lie `L`-module, the trace form is alternating and satisfies the property that for all `x, y, z` in `L`, `tr(x, [y, z]) = tr(y, [x, z])`.
|
LieSubmodule.traceForm_eq_zero_of_isTrivial
theorem LieSubmodule.traceForm_eq_zero_of_isTrivial :
∀ {R : Type u_1} {L : Type u_3} {M : Type u_4} [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 : Module.Free R M] [inst_8 : Module.Finite R M] [inst_9 : IsDomain R] [inst_10 : IsPrincipalIdealRing R]
(N : LieSubmodule R L M),
∀ I ≤ N.idealizer,
∀ (x : L) {y : L},
y ∈ I →
∀ [inst_11 : LieModule.IsTrivial ↥↑I ↥↑N],
(LinearMap.trace R M) ((LieModule.toEndomorphism R L M) x ∘ₗ (LieModule.toEndomorphism R L M) y) = 0
This theorem asserts that for any Lie Submodule `N` of a Lie Module `M` over a Lie algebra `L` and a commutative ring `R`, given an ideal `I` of the ring which is contained in the idealizer of `N`, for any elements `x` and `y` from the Lie algebra `L` where `y` is in `I`, and if the Lie Module `N` is trivial over the ideal `I`, then the trace of the composition of the endomorphisms of `M` corresponding to `x` and `y` in the Lie Module, is zero. Note that this is a stronger result than it might look, because we only assume that `N` is trivial over `I`, not over all of `L`. This makes the theorem applicable in the important case of an Abelian ideal, where `M = L` and `N = I`.
More concisely: Given a Lie algebra `L`, a Lie submodule `N` of a Lie module `M` over `L`, a commutative ring `R`, an ideal `I` of `R` contained in the idealizer of `N`, and `x, y` in `L` with `y` in `I`, if `N` is trivial over `I`, then the trace of the composition of the endomorphisms of `M` corresponding to `x` and `y` is zero.
|
LieModule.eq_zero_of_mem_weightSpace_mem_posFitting
theorem LieModule.eq_zero_of_mem_weightSpace_mem_posFitting :
∀ (R : Type u_1) (L : Type u_3) (M : Type u_4) [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 : LieAlgebra.IsNilpotent R L] {B : LinearMap.BilinForm R M},
(∀ (x : L) (m n : M), (B ⁅x, m⁆) n = -(B m) ⁅x, n⁆) →
∀ {m₀ m₁ : M}, m₀ ∈ LieModule.weightSpace M 0 → m₁ ∈ LieModule.posFittingComp R L M → (B m₀) m₁ = 0
The theorem `LieModule.eq_zero_of_mem_weightSpace_mem_posFitting` states that given a bilinear form `B` on a representation `M` of a nilpotent Lie algebra `L`, if `B` is invariant under the action of `L` (in the sense that the action of `L` is skew-adjoint with respect to `B`), then the components of the Fitting decomposition of `M` are orthogonal with respect to `B`. More specifically, for any elements `m₀` and `m₁` of `M` such that `m₀` is in the weight space of `M` with weight 0 and `m₁` is in the positive Fitting component of `M`, the bilinear form `B` evaluated at `m₀` and `m₁` is 0.
More concisely: Given a nilpotent Lie algebra `L` acting on a representation `M` with invariant and skew-adjoint bilinear form `B`, the weight space of `M` with weight 0 is orthogonal to the positive Fitting component of `M` with respect to `B`.
|
LieModule.lie_traceForm_eq_zero
theorem LieModule.lie_traceForm_eq_zero :
∀ (R : Type u_1) (L : Type u_3) (M : Type u_4) [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] (x : L),
⁅x, LieModule.traceForm R L M⁆ = 0
This theorem, `LieModule.lie_traceForm_eq_zero`, states that for any commutative ring `R`, any Lie ring `L`, and any module `M` over `R` that is also a Lie module over `L`, the Lie bracket of any element of `L` with the trace form of the Lie module is always zero. This result justifies the use of the term "invariant" in the context of trace forms in the theory of Lie modules.
More concisely: For any commutative ring R, Lie ring L, and Lie module M over R, the Lie bracket of any element of L with the trace form of M is zero.
|
LieAlgebra.IsKilling.killingCompl_top_eq_bot
theorem LieAlgebra.IsKilling.killingCompl_top_eq_bot :
∀ {R : Type u_1} {L : Type u_3} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
[self : LieAlgebra.IsKilling R L], LieIdeal.killingCompl R L ⊤ = ⊥
The theorem `LieAlgebra.IsKilling.killingCompl_top_eq_bot` states that for any commutative ring `R` and any Lie ring `L` that is also a Lie algebra over `R`, if the Lie algebra `L` is Killing (meaning its Killing form is non-singular), then the orthogonal complement of the top element (or the entire space) of the Lie algebra `L` with respect to the Killing form is the bottom element, or the zero ideal. This means that in a Killing Lie algebra, the only vectors orthogonal to all vectors in the Lie algebra are the zero vector.
More concisely: In a commutative ring R with a Killing Lie algebra L over it, the orthogonal complement of the top element of L with respect to the Killing form is the zero ideal.
|
LieModule.traceForm_eq_zero_if_mem_lcs_of_mem_ucs
theorem LieModule.traceForm_eq_zero_if_mem_lcs_of_mem_ucs :
∀ (R : Type u_1) (L : Type u_3) (M : Type u_4) [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] {x y : L}
(k : ℕ), x ∈ ⊤.lcs L k → y ∈ LieSubmodule.ucs k ⊥ → ((LieModule.traceForm R L M) x) y = 0
This theorem states that for any commutative ring `R`, any Lie ring `L`, and any Lie module `M` over `L`, if `x` is an element of the lower central series of `L` at level `k` and `y` is an element of the upper central series of the zero submodule at the same level `k`, then the trace form of the Lie module `M` applied to `x` and `y` equals zero. In other words, the upper and lower central series of a Lie algebra are orthogonal with respect to the trace form of any of its modules.
More concisely: For any commutative ring `R`, Lie ring `L`, and Lie module `M` over `L`, the element-wise application of the trace form of `M` to any element in the lower central series of `L` at level `k` and any element in the upper central series of the zero submodule at the same level `k` equals zero.
|
LieAlgebra.IsKilling.span_weight_eq_top
theorem LieAlgebra.IsKilling.span_weight_eq_top :
∀ (K : Type u_2) (L : Type u_3) [inst : LieRing L] [inst_1 : Field K] [inst_2 : LieAlgebra K L]
[inst_3 : FiniteDimensional K L] (H : LieSubalgebra K L) [inst_4 : H.IsCartanSubalgebra]
[inst_5 : LieModule.IsTriangularizable K (↥H) L] [inst_6 : LieAlgebra.IsKilling K L],
Submodule.span K (Set.range (LieModule.Weight.toLinear K (↥H) L)) = ⊤
The theorem `LieAlgebra.IsKilling.span_weight_eq_top` states that for a given splitting Cartan subalgebra `H` of a finite-dimensional Lie algebra with a non-singular Killing form, the roots corresponding to `H` span the dual space. More specifically, if `L` is a Lie algebra over a field `K`, where `L` has a finite dimension and a non-singular Killing form, and `H` is a splitting Cartan subalgebra of `L` such that the Lie module `L` is triangularizable with respect to `H`, then the span of the set of weights (as a `K`-submodule) is the entire dual space of `H`. This means every element of the dual space can be represented as a linear combination of these root vectors.
More concisely: For a finite-dimensional Lie algebra over a field with a non-singular Killing form and a splitting Cartan subalgebra `H` such that `L` is triangularizable with respect to `H`, the weights span the entire dual space of `H`.
|