# Documentation

Mathlib.Algebra.Lie.Weights.Basic

# Weight spaces of Lie modules of nilpotent Lie algebras #

Just as a key tool when studying the behaviour of a linear operator is to decompose the space on which it acts into a sum of (generalised) eigenspaces, a key tool when studying a representation M of Lie algebra L is to decompose M into a sum of simultaneous eigenspaces of x as x ranges over L. These simultaneous generalised eigenspaces are known as the weight spaces of M.

When L is nilpotent, it follows from the binomial theorem that weight spaces are Lie submodules.

Basic definitions and properties of the above ideas are provided in this file.

## Main definitions #

• LieModule.weightSpaceOf
• LieModule.weightSpace
• LieModule.posFittingCompOf
• LieModule.posFittingComp
• LieModule.iSup_ucs_eq_weightSpace_zero
• LieModule.iInf_lowerCentralSeries_eq_posFittingComp
• LieModule.isCompl_weightSpace_zero_posFittingComp
• LieModule.independent_weightSpace
• LieModule.iSup_weightSpace_eq_top

## Tags #

lie character, eigenvalue, eigenspace, weight, weight vector, root, root vector

theorem LieModule.weight_vector_multiplication {R : Type u_2} {L : Type u_3} [] [] [] (M₁ : Type u_5) (M₂ : Type u_6) (M₃ : Type u_7) [] [Module R M₁] [] [LieModule R L M₁] [] [Module R M₂] [] [LieModule R L M₂] [] [Module R M₃] [] [LieModule R L M₃] (g : TensorProduct R M₁ M₂ →ₗ⁅R,L M₃) (χ₁ : R) (χ₂ : R) (x : L) :
LinearMap.range (LinearMap.comp (g) (TensorProduct.mapIncl 𝕎(M₁, χ₁, x) 𝕎(M₂, χ₂, x))) 𝕎(M₃, χ₁ + χ₂, x)

See also bourbaki1975b Chapter VII §1.1, Proposition 2 (ii).

theorem LieModule.lie_mem_maxGenEigenspace_toEndomorphism {R : Type u_2} {L : Type u_3} {M : Type u_4} [] [] [] [] [Module R M] [] [LieModule R L M] {χ₁ : R} {χ₂ : R} {x : L} {y : L} {m : M} (hy : y 𝕎(L, χ₁, x)) (hm : m 𝕎(M, χ₂, x)) :
y, m 𝕎(M, χ₁ + χ₂, x)
def LieModule.weightSpaceOf {R : Type u_2} {L : Type u_3} (M : Type u_4) [] [] [] [] [] [Module R M] [] [LieModule R L M] (χ : R) (x : L) :

If M is a representation of a nilpotent Lie algebra L, χ is a scalar, and x : L, then weightSpaceOf M χ x is the maximal generalized χ-eigenspace of the action of x on M.

It is a Lie submodule because L is nilpotent.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem LieModule.mem_weightSpaceOf {R : Type u_2} {L : Type u_3} (M : Type u_4) [] [] [] [] [] [Module R M] [] [LieModule R L M] (χ : R) (x : L) (m : M) :
m ∃ (k : ), ((() x - χ 1) ^ k) m = 0
theorem LieModule.coe_weightSpaceOf_zero {R : Type u_2} {L : Type u_3} (M : Type u_4) [] [] [] [] [] [Module R M] [] [LieModule R L M] (x : L) :
() = ⨆ (k : ), LinearMap.ker (() x ^ k)
def LieModule.weightSpace {R : Type u_2} {L : Type u_3} (M : Type u_4) [] [] [] [] [] [Module R M] [] [LieModule R L M] (χ : LR) :

If M is a representation of a nilpotent Lie algebra L and χ : L → R is a family of scalars, then weightSpace M χ is the intersection of the maximal generalized χ x-eigenspaces of the action of x on M as x ranges over L.

It is a Lie submodule because L is nilpotent.

Equations
Instances For
theorem LieModule.mem_weightSpace {R : Type u_2} {L : Type u_3} (M : Type u_4) [] [] [] [] [] [Module R M] [] [LieModule R L M] (χ : LR) (m : M) :
∀ (x : L), ∃ (k : ), ((() x - χ x 1) ^ k) m = 0
theorem LieModule.weightSpace_le_weightSpaceOf {R : Type u_2} {L : Type u_3} (M : Type u_4) [] [] [] [] [] [Module R M] [] [LieModule R L M] (x : L) (χ : LR) :
@[simp]
theorem LieModule.zero_weightSpace_eq_top_of_nilpotent' {R : Type u_2} {L : Type u_3} (M : Type u_4) [] [] [] [] [] [Module R M] [] [LieModule R L M] [] :

See also the more useful form LieModule.zero_weightSpace_eq_top_of_nilpotent.

theorem LieModule.coe_weightSpace_of_top {R : Type u_2} {L : Type u_3} (M : Type u_4) [] [] [] [] [] [Module R M] [] [LieModule R L M] (χ : LR) :
() = ()
@[simp]
theorem LieModule.zero_weightSpace_eq_top_of_nilpotent {R : Type u_2} {L : Type u_3} (M : Type u_4) [] [] [] [] [] [Module R M] [] [LieModule R L M] [] :
theorem LieModule.exists_weightSpace_le_ker_of_isNoetherian {R : Type u_2} {L : Type u_3} (M : Type u_4) [] [] [] [] [] [Module R M] [] [LieModule R L M] [] (χ : LR) (x : L) :
∃ (k : ), () LinearMap.ker ((() x - (algebraMap R ()) (χ x)) ^ k)
theorem LieModule.exists_weightSpace_zero_le_ker_of_isNoetherian (R : Type u_2) {L : Type u_3} (M : Type u_4) [] [] [] [] [] [Module R M] [] [LieModule R L M] [] (x : L) :
∃ (k : ), () LinearMap.ker (() x ^ k)
theorem LieModule.isNilpotent_toEndomorphism_sub_algebraMap {R : Type u_2} {L : Type u_3} (M : Type u_4) [] [] [] [] [] [Module R M] [] [LieModule R L M] [] (χ : LR) (x : L) :
IsNilpotent (() x - (algebraMap R (Module.End R ())) (χ x))
theorem LieModule.isNilpotent_toEndomorphism_weightSpace_zero {R : Type u_2} {L : Type u_3} (M : Type u_4) [] [] [] [] [] [Module R M] [] [LieModule R L M] [] (x : L) :

A (nilpotent) Lie algebra acts nilpotently on the zero weight space of a Noetherian Lie module.

By Engel's theorem, the zero weight space of a Noetherian Lie module is nilpotent.

Equations
• (_ : ) = (_ : )
@[simp]
theorem LieModule.weightSpace_zero_normalizer_eq_self (R : Type u_2) (L : Type u_3) (M : Type u_4) [] [] [] [] [] [Module R M] [] [LieModule R L M] :
theorem LieModule.iSup_ucs_le_weightSpace_zero (R : Type u_2) (L : Type u_3) (M : Type u_4) [] [] [] [] [] [Module R M] [] [LieModule R L M] :
⨆ (k : ),
theorem LieModule.iSup_ucs_eq_weightSpace_zero (R : Type u_2) (L : Type u_3) (M : Type u_4) [] [] [] [] [] [Module R M] [] [LieModule R L M] [] :
⨆ (k : ), =

See also LieModule.iInf_lowerCentralSeries_eq_posFittingComp.

def LieModule.posFittingCompOf (R : Type u_2) {L : Type u_3} (M : Type u_4) [] [] [] [] [] [Module R M] [] [LieModule R L M] (x : L) :

If M is a representation of a nilpotent Lie algebra L, and x : L, then posFittingCompOf R M x is the infimum of the decreasing system range φₓ ⊇ range φₓ² ⊇ range φₓ³ ⊇ ⋯ where φₓ : End R M := toEndomorphism R L M x. We call this the "positive Fitting component" because with appropriate assumptions (e.g., R is a field and M is finite-dimensional) φₓ induces the so-called Fitting decomposition: M = M₀ ⊕ M₁ where M₀ = weightSpaceOf M 0 x and M₁ = posFittingCompOf R M x.

It is a Lie submodule because L is nilpotent.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem LieModule.mem_posFittingCompOf (R : Type u_2) {L : Type u_3} {M : Type u_4} [] [] [] [] [] [Module R M] [] [LieModule R L M] (x : L) (m : M) :
m ∀ (k : ), ∃ (n : M), (() x ^ k) n = m
@[simp]
theorem LieModule.posFittingCompOf_le_lowerCentralSeries (R : Type u_2) {L : Type u_3} (M : Type u_4) [] [] [] [] [] [Module R M] [] [LieModule R L M] (x : L) (k : ) :
@[simp]
theorem LieModule.posFittingCompOf_eq_bot_of_isNilpotent (R : Type u_2) {L : Type u_3} (M : Type u_4) [] [] [] [] [] [Module R M] [] [LieModule R L M] [] (x : L) :
def LieModule.posFittingComp (R : Type u_2) (L : Type u_3) (M : Type u_4) [] [] [] [] [] [Module R M] [] [LieModule R L M] :

If M is a representation of a nilpotent Lie algebra L with coefficients in R, then posFittingComp R L M is the span of the positive Fitting components of the action of x on M, as x ranges over L.

It is a Lie submodule because L is nilpotent.

Equations
• = ⨆ (x : L),
Instances For
theorem LieModule.mem_posFittingComp (R : Type u_2) (L : Type u_3) (M : Type u_4) [] [] [] [] [] [Module R M] [] [LieModule R L M] (m : M) :
m m ⨆ (x : L),
theorem LieModule.posFittingCompOf_le_posFittingComp (R : Type u_2) (L : Type u_3) (M : Type u_4) [] [] [] [] [] [Module R M] [] [LieModule R L M] (x : L) :
theorem LieModule.posFittingComp_le_iInf_lowerCentralSeries (R : Type u_2) (L : Type u_3) (M : Type u_4) [] [] [] [] [] [Module R M] [] [LieModule R L M] :
⨅ (k : ),
@[simp]
theorem LieModule.iInf_lowerCentralSeries_eq_posFittingComp (R : Type u_2) (L : Type u_3) (M : Type u_4) [] [] [] [] [] [Module R M] [] [LieModule R L M] [] [] :
⨅ (k : ), =

See also LieModule.iSup_ucs_eq_weightSpace_zero.

@[simp]
theorem LieModule.posFittingComp_eq_bot_of_isNilpotent (R : Type u_2) (L : Type u_3) (M : Type u_4) [] [] [] [] [] [Module R M] [] [LieModule R L M] [] :
theorem LieModule.map_posFittingComp_le {R : Type u_2} {L : Type u_3} {M : Type u_4} [] [] [] [] [] [Module R M] [] [LieModule R L M] {M₂ : Type u_5} [] [Module R M₂] [] [LieModule R L M₂] (f : M →ₗ⁅R,L M₂) :
theorem LieModule.map_weightSpace_le {R : Type u_2} {L : Type u_3} {M : Type u_4} [] [] [] [] [] [Module R M] [] [LieModule R L M] {M₂ : Type u_5} [] [Module R M₂] [] [LieModule R L M₂] {χ : LR} (f : M →ₗ⁅R,L M₂) :
theorem LieModule.comap_weightSpace_eq_of_injective {R : Type u_2} {L : Type u_3} {M : Type u_4} [] [] [] [] [] [Module R M] [] [LieModule R L M] {M₂ : Type u_5} [] [Module R M₂] [] [LieModule R L M₂] {χ : LR} {f : M →ₗ⁅R,L M₂} (hf : ) :
theorem LieModule.map_weightSpace_eq_of_injective {R : Type u_2} {L : Type u_3} {M : Type u_4} [] [] [] [] [] [Module R M] [] [LieModule R L M] {M₂ : Type u_5} [] [Module R M₂] [] [LieModule R L M₂] {χ : LR} {f : M →ₗ⁅R,L M₂} (hf : ) :
theorem LieModule.map_weightSpace_eq {R : Type u_2} {L : Type u_3} {M : Type u_4} [] [] [] [] [] [Module R M] [] [LieModule R L M] {M₂ : Type u_5} [] [Module R M₂] [] [LieModule R L M₂] {χ : LR} (e : M ≃ₗ⁅R,L M₂) :
LieSubmodule.map e.toLieModuleHom () =
theorem LieModule.map_posFittingComp_eq {R : Type u_2} {L : Type u_3} {M : Type u_4} [] [] [] [] [] [Module R M] [] [LieModule R L M] {M₂ : Type u_5} [] [Module R M₂] [] [LieModule R L M₂] (e : M ≃ₗ⁅R,L M₂) :
LieSubmodule.map e.toLieModuleHom () =
theorem LieModule.posFittingComp_map_incl_sup_of_codisjoint {R : Type u_2} {L : Type u_3} {M : Type u_4} [] [] [] [] [] [Module R M] [] [LieModule R L M] [] [] {N₁ : LieSubmodule R L M} {N₂ : LieSubmodule R L M} (h : Codisjoint N₁ N₂) :
theorem LieModule.weightSpace_weightSpaceOf_map_incl {R : Type u_2} {L : Type u_3} {M : Type u_4} [] [] [] [] [] [Module R M] [] [LieModule R L M] (x : L) (χ : LR) :
theorem LieModule.isCompl_weightSpaceOf_zero_posFittingCompOf (R : Type u_2) (L : Type u_3) (M : Type u_4) [] [] [] [] [] [Module R M] [] [LieModule R L M] [] [] (x : L) :
IsCompl () ()
theorem LieModule.isCompl_weightSpace_zero_posFittingComp (R : Type u_2) (L : Type u_3) (M : Type u_4) [] [] [] [] [] [Module R M] [] [LieModule R L M] [] [] :
IsCompl () ()

This is the Fitting decomposition of the Lie module M.

theorem LieModule.disjoint_weightSpaceOf (R : Type u_2) (L : Type u_3) (M : Type u_4) [] [] [] [] [] [Module R M] [] [LieModule R L M] [] {x : L} {φ₁ : R} {φ₂ : R} (h : φ₁ φ₂) :
Disjoint () ()
theorem LieModule.disjoint_weightSpace (R : Type u_2) (L : Type u_3) (M : Type u_4) [] [] [] [] [] [Module R M] [] [LieModule R L M] [] {χ₁ : LR} {χ₂ : LR} (h : χ₁ χ₂) :
Disjoint () ()
theorem LieModule.injOn_weightSpace (R : Type u_2) (L : Type u_3) (M : Type u_4) [] [] [] [] [] [Module R M] [] [LieModule R L M] [] :
Set.InjOn (fun (χ : LR) => ) {χ : LR | }
theorem LieModule.independent_weightSpace (R : Type u_2) (L : Type u_3) (M : Type u_4) [] [] [] [] [] [Module R M] [] [LieModule R L M] [] :
CompleteLattice.Independent fun (χ : LR) =>
theorem LieModule.independent_weightSpaceOf (R : Type u_2) (L : Type u_3) (M : Type u_4) [] [] [] [] [] [Module R M] [] [LieModule R L M] [] (x : L) :
theorem LieModule.finite_weightSpaceOf_ne_bot (R : Type u_2) (L : Type u_3) (M : Type u_4) [] [] [] [] [] [Module R M] [] [LieModule R L M] [] [] (x : L) :
Set.Finite {χ : R | }
theorem LieModule.finite_weightSpace_ne_bot (R : Type u_2) (L : Type u_3) (M : Type u_4) [] [] [] [] [] [Module R M] [] [LieModule R L M] [] [] :
Set.Finite {χ : LR | }
@[inline, reducible]
noncomputable abbrev LieModule.weight (R : Type u_2) (L : Type u_3) (M : Type u_4) [] [] [] [] [] [Module R M] [] [LieModule R L M] [] [] :
Finset (LR)

The collection of weights of a Noetherian Lie module, bundled as a Finset.

Equations
Instances For
class LieModule.IsTriangularizable (R : Type u_2) (L : Type u_3) (M : Type u_4) [] [] [] [] [Module R M] [] [LieModule R L M] :

A Lie module M of a Lie algebra L is triangularizable if the endomorhpism of M defined by any x : L is triangularizable.

• iSup_eq_top : ∀ (x : L), ⨆ (φ : R), ⨆ (k : ), () k =
Instances
@[simp]
theorem LieModule.iSup_weightSpaceOf_eq_top (R : Type u_2) (L : Type u_3) (M : Type u_4) [] [] [] [] [] [Module R M] [] [LieModule R L M] [] (x : L) :
⨆ (φ : R), =
instance LieModule.instIsTriangularizableOfIsAlgClosed (K : Type u_1) (L : Type u_3) (M : Type u_4) [] [] [] [] [] [Module K M] [LieModule K L M] [] [] :
Equations
• (_ : ) = (_ : )
Equations
• (_ : ) = (_ : )
theorem LieModule.iSup_weightSpace_eq_top (K : Type u_1) (L : Type u_3) (M : Type u_4) [] [] [] [] [] [Module K M] [LieModule K L M] [] [] [] :
⨆ (χ : LK), =