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.Weight
• 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

References

• N. Bourbaki, Lie Groups and Lie Algebras, Chapters 7--9

Tags

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

theorem LieModule.weight_vector_multiplication {R : Type u_2} {L : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] (M₁ : Type u_5) (M₂ : Type u_6) (M₃ : Type u_7) [AddCommGroup M₁] [Module R M₁] [LieRingModule L M₁] [LieModule R L M₁] [AddCommGroup M₂] [Module R M₂] [LieRingModule L M₂] [LieModule R L M₂] [AddCommGroup M₃] [Module R M₃] [LieRingModule L M₃] [LieModule R L M₃] (g : TensorProduct R M₁ M₂ →ₗ⁅R,L⁆ M₃) (χ₁ : R) (χ₂ : R) (x : L) : LinearMap.range (↑g ∘ₗ TensorProduct.mapIncl (Module.End.maximalGeneralizedEigenspace ((LieModule.toEndomorphism R L M₁) x) χ₁) (Module.End.maximalGeneralizedEigenspace ((LieModule.toEndomorphism R L M₂) x) χ₂)) ≤ Module.End.maximalGeneralizedEigenspace ((LieModule.toEndomorphism R L 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} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {χ₁ : R} {χ₂ : R} {x : L} {y : L} {m : M} (hy : y ∈ Module.End.maximalGeneralizedEigenspace ((LieModule.toEndomorphism R L L) x) χ₁) (hm : m ∈ Module.End.maximalGeneralizedEigenspace ((LieModule.toEndomorphism R L M) x) χ₂) : ⁅y, m⁆ ∈ Module.End.maximalGeneralizedEigenspace ((LieModule.toEndomorphism R L M) x) (χ₁ + χ₂)

def LieModule.weightSpaceOf {R : Type u_2} {L : Type u_3} (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsNilpotent R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (χ : R) (x : L) : LieSubmodule R L M

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

• LieModule.weightSpaceOf M χ x = let __src := Module.End.maximalGeneralizedEigenspace ((LieModule.toEndomorphism R L M) x) χ; { toSubmodule := __src, lie_mem := ⋯ }

theorem LieModule.mem_weightSpaceOf {R : Type u_2} {L : Type u_3} (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsNilpotent R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (χ : R) (x : L) (m : M) : m ∈ LieModule.weightSpaceOf M χ x ↔ ∃ (k : ℕ), (((LieModule.toEndomorphism R L M) x - χ • 1) ^ k) m = 0

theorem LieModule.coe_weightSpaceOf_zero {R : Type u_2} {L : Type u_3} (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsNilpotent R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (x : L) : ↑(LieModule.weightSpaceOf M 0 x) = ⨆ (k : ℕ), LinearMap.ker ((LieModule.toEndomorphism R L M) x ^ k)

def LieModule.weightSpace {R : Type u_2} {L : Type u_3} (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsNilpotent R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (χ : L → R) : LieSubmodule R L M

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

• LieModule.weightSpace M χ = ⨅ (x : L), LieModule.weightSpaceOf M (χ x) x

theorem LieModule.mem_weightSpace {R : Type u_2} {L : Type u_3} (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsNilpotent R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (χ : L → R) (m : M) : m ∈ LieModule.weightSpace M χ ↔ ∀ (x : L), ∃ (k : ℕ), (((LieModule.toEndomorphism R L M) x - χ x • 1) ^ k) m = 0

theorem LieModule.weightSpace_le_weightSpaceOf {R : Type u_2} {L : Type u_3} (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsNilpotent R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (x : L) (χ : L → R) : LieModule.weightSpace M χ ≤ LieModule.weightSpaceOf M (χ x) x

structure LieModule.Weight (R : Type u_2) (L : Type u_3) (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsNilpotent R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] : Type (max u_2 u_3)

A weight of a Lie module is a map L → R such that the corresponding weight space is non-trivial.

• toFun : L → R

  The family of eigenvalues corresponding to a weight.

• weightSpace_ne_bot : LieModule.weightSpace M self.toFun ≠ ⊥

instance LieModule.Weight.instFunLike {R : Type u_2} {L : Type u_3} (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsNilpotent R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] : FunLike (LieModule.Weight R L M) L R

Equations

• LieModule.Weight.instFunLike M = { coe := fun (χ : LieModule.Weight R L M) => χ.toFun, coe_injective' := ⋯ }

@[simp]

theorem LieModule.Weight.coe_weight_mk {R : Type u_2} {L : Type u_3} (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsNilpotent R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (χ : L → R) (h : LieModule.weightSpace M χ ≠ ⊥) : ⇑{ toFun := χ, weightSpace_ne_bot := h } = χ

def LieModule.Weight.IsZero {R : Type u_2} {L : Type u_3} {M : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsNilpotent R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (χ : LieModule.Weight R L M) : Prop

The proposition that a weight of a Lie module is zero.

We make this definition because we cannot define a Zero (Weight R L M) instance since the weight space of the zero function can be trivial.

Equations

• LieModule.Weight.IsZero χ = (⇑χ = 0)

@[simp]

theorem LieModule.Weight.IsZero.eq {R : Type u_2} {L : Type u_3} {M : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsNilpotent R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {χ : LieModule.Weight R L M} (hχ : LieModule.Weight.IsZero χ) : ⇑χ = 0

@[simp]

theorem LieModule.Weight.coe_eq_zero_iff {R : Type u_2} {L : Type u_3} {M : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsNilpotent R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (χ : LieModule.Weight R L M) : ⇑χ = 0 ↔ LieModule.Weight.IsZero χ

@[inline, reducible]

abbrev LieModule.Weight.IsNonZero {R : Type u_2} {L : Type u_3} {M : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsNilpotent R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (χ : LieModule.Weight R L M) : Prop

The proposition that a weight of a Lie module is non-zero.

Equations

• LieModule.Weight.IsNonZero χ = ¬LieModule.Weight.IsZero χ

def LieModule.Weight.equivSetOf (R : Type u_2) (L : Type u_3) (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsNilpotent R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] : LieModule.Weight R L M ≃ ↑{χ : L → R | LieModule.weightSpace M χ ≠ ⊥}

The set of weights is equivalent to a subtype.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem LieModule.zero_weightSpace_eq_top_of_nilpotent' {R : Type u_2} {L : Type u_3} (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsNilpotent R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [LieModule.IsNilpotent R L M] : LieModule.weightSpace M 0 = ⊤

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) [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsNilpotent R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (χ : L → R) : ↑(LieModule.weightSpace M (χ ∘ ⇑(LieSubalgebra.incl ⊤))) = ↑(LieModule.weightSpace M χ)

@[simp]

theorem LieModule.zero_weightSpace_eq_top_of_nilpotent {R : Type u_2} {L : Type u_3} (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsNilpotent R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [LieModule.IsNilpotent R L M] : LieModule.weightSpace M 0 = ⊤

theorem LieModule.exists_weightSpace_le_ker_of_isNoetherian {R : Type u_2} {L : Type u_3} (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsNilpotent R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [IsNoetherian R M] (χ : L → R) (x : L) : ∃ (k : ℕ), ↑(LieModule.weightSpace M χ) ≤ LinearMap.ker (((LieModule.toEndomorphism R L M) x - (algebraMap R (Module.End R M)) (χ x)) ^ k)

theorem LieModule.exists_weightSpace_zero_le_ker_of_isNoetherian (R : Type u_2) {L : Type u_3} (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsNilpotent R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [IsNoetherian R M] (x : L) : ∃ (k : ℕ), ↑(LieModule.weightSpace M 0) ≤ LinearMap.ker ((LieModule.toEndomorphism R L M) x ^ k)

theorem LieModule.isNilpotent_toEndomorphism_sub_algebraMap {R : Type u_2} {L : Type u_3} (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsNilpotent R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [IsNoetherian R M] (χ : L → R) (x : L) : IsNilpotent ((LieModule.toEndomorphism R L ↥↑(LieModule.weightSpace M χ)) x - (algebraMap R (Module.End R ↥↑(LieModule.weightSpace M χ))) (χ x))

theorem LieModule.isNilpotent_toEndomorphism_weightSpace_zero {R : Type u_2} {L : Type u_3} (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsNilpotent R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [IsNoetherian R M] (x : L) : IsNilpotent ((LieModule.toEndomorphism R L ↥↑(LieModule.weightSpace M 0)) x)

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

instance LieModule.instIsNilpotentSubtypeMemSubmoduleToSemiringToCommSemiringToAddCommMonoidInstMembershipSetLikeToSubmoduleWeightSpaceOfNatForAllToOfNat0InstZeroToZeroToCommMonoidWithZeroAddCommGroupToRingInstModuleSubtypeMemSubmoduleToSemiringToCommSemiringToAddCommMonoidInstMembershipSetLikeToSubmoduleAddCommMonoidInstLieRingModuleSubtypeMemSubmoduleToSemiringToCommSemiringToAddCommMonoidInstMembershipSetLikeToSubmoduleAddCommGroupToRing {R : Type u_2} {L : Type u_3} (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsNilpotent R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [IsNoetherian R M] : LieModule.IsNilpotent R L ↥↑(LieModule.weightSpace M 0)

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) [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsNilpotent R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] : LieSubmodule.normalizer (LieModule.weightSpace M 0) = LieModule.weightSpace M 0

theorem LieModule.iSup_ucs_le_weightSpace_zero (R : Type u_2) (L : Type u_3) (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsNilpotent R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] : ⨆ (k : ℕ), LieSubmodule.ucs k ⊥ ≤ LieModule.weightSpace M 0

theorem LieModule.iSup_ucs_eq_weightSpace_zero (R : Type u_2) (L : Type u_3) (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsNilpotent R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [IsNoetherian R M] : ⨆ (k : ℕ), LieSubmodule.ucs k ⊥ = LieModule.weightSpace M 0

See also LieModule.iInf_lowerCentralSeries_eq_posFittingComp.

def LieModule.posFittingCompOf (R : Type u_2) {L : Type u_3} (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsNilpotent R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (x : L) : LieSubmodule R L M

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

• LieModule.posFittingCompOf R M x = { toSubmodule := ⨅ (k : ℕ), LinearMap.range ((LieModule.toEndomorphism R L M) x ^ k), lie_mem := ⋯ }

theorem LieModule.mem_posFittingCompOf (R : Type u_2) {L : Type u_3} {M : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsNilpotent R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (x : L) (m : M) : m ∈ LieModule.posFittingCompOf R M x ↔ ∀ (k : ℕ), ∃ (n : M), ((LieModule.toEndomorphism R L M) x ^ k) n = m

@[simp]

theorem LieModule.posFittingCompOf_le_lowerCentralSeries (R : Type u_2) {L : Type u_3} (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsNilpotent R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (x : L) (k : ℕ) : LieModule.posFittingCompOf R M x ≤ LieModule.lowerCentralSeries R L M k

@[simp]

theorem LieModule.posFittingCompOf_eq_bot_of_isNilpotent (R : Type u_2) {L : Type u_3} (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsNilpotent R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [LieModule.IsNilpotent R L M] (x : L) : LieModule.posFittingCompOf R M x = ⊥

def LieModule.posFittingComp (R : Type u_2) (L : Type u_3) (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsNilpotent R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] : LieSubmodule 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

• LieModule.posFittingComp R L M = ⨆ (x : L), LieModule.posFittingCompOf R M x

theorem LieModule.mem_posFittingComp (R : Type u_2) (L : Type u_3) (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsNilpotent R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (m : M) : m ∈ LieModule.posFittingComp R L M ↔ m ∈ ⨆ (x : L), LieModule.posFittingCompOf R M x

theorem LieModule.posFittingCompOf_le_posFittingComp (R : Type u_2) (L : Type u_3) (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsNilpotent R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (x : L) : LieModule.posFittingCompOf R M x ≤ LieModule.posFittingComp R L M

theorem LieModule.posFittingComp_le_iInf_lowerCentralSeries (R : Type u_2) (L : Type u_3) (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsNilpotent R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] : LieModule.posFittingComp R L M ≤ ⨅ (k : ℕ), LieModule.lowerCentralSeries R L M k

@[simp]

theorem LieModule.iInf_lowerCentralSeries_eq_posFittingComp (R : Type u_2) (L : Type u_3) (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsNilpotent R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [IsNoetherian R M] [IsArtinian R M] : ⨅ (k : ℕ), LieModule.lowerCentralSeries R L M k = LieModule.posFittingComp R L M

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) [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsNilpotent R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [LieModule.IsNilpotent R L M] : LieModule.posFittingComp R L M = ⊥

theorem LieModule.map_posFittingComp_le {R : Type u_2} {L : Type u_3} {M : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsNilpotent R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {M₂ : Type u_5} [AddCommGroup M₂] [Module R M₂] [LieRingModule L M₂] [LieModule R L M₂] (f : M →ₗ⁅R,L⁆ M₂) : LieSubmodule.map f (LieModule.posFittingComp R L M) ≤ LieModule.posFittingComp R L M₂

theorem LieModule.map_weightSpace_le {R : Type u_2} {L : Type u_3} {M : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsNilpotent R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {M₂ : Type u_5} [AddCommGroup M₂] [Module R M₂] [LieRingModule L M₂] [LieModule R L M₂] {χ : L → R} (f : M →ₗ⁅R,L⁆ M₂) : LieSubmodule.map f (LieModule.weightSpace M χ) ≤ LieModule.weightSpace M₂ χ

theorem LieModule.comap_weightSpace_eq_of_injective {R : Type u_2} {L : Type u_3} {M : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsNilpotent R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {M₂ : Type u_5} [AddCommGroup M₂] [Module R M₂] [LieRingModule L M₂] [LieModule R L M₂] {χ : L → R} {f : M →ₗ⁅R,L⁆ M₂} (hf : Function.Injective ⇑f) : LieSubmodule.comap f (LieModule.weightSpace M₂ χ) = LieModule.weightSpace M χ

theorem LieModule.map_weightSpace_eq_of_injective {R : Type u_2} {L : Type u_3} {M : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsNilpotent R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {M₂ : Type u_5} [AddCommGroup M₂] [Module R M₂] [LieRingModule L M₂] [LieModule R L M₂] {χ : L → R} {f : M →ₗ⁅R,L⁆ M₂} (hf : Function.Injective ⇑f) : LieSubmodule.map f (LieModule.weightSpace M χ) = LieModule.weightSpace M₂ χ ⊓ LieModuleHom.range f

theorem LieModule.map_weightSpace_eq {R : Type u_2} {L : Type u_3} {M : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsNilpotent R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {M₂ : Type u_5} [AddCommGroup M₂] [Module R M₂] [LieRingModule L M₂] [LieModule R L M₂] {χ : L → R} (e : M ≃ₗ⁅R,L⁆ M₂) : LieSubmodule.map e.toLieModuleHom (LieModule.weightSpace M χ) = LieModule.weightSpace M₂ χ

theorem LieModule.map_posFittingComp_eq {R : Type u_2} {L : Type u_3} {M : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsNilpotent R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {M₂ : Type u_5} [AddCommGroup M₂] [Module R M₂] [LieRingModule L M₂] [LieModule R L M₂] (e : M ≃ₗ⁅R,L⁆ M₂) : LieSubmodule.map e.toLieModuleHom (LieModule.posFittingComp R L M) = LieModule.posFittingComp R L M₂

theorem LieModule.posFittingComp_map_incl_sup_of_codisjoint {R : Type u_2} {L : Type u_3} {M : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsNilpotent R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [IsNoetherian R M] [IsArtinian R M] {N₁ : LieSubmodule R L M} {N₂ : LieSubmodule R L M} (h : Codisjoint N₁ N₂) : LieSubmodule.map (LieSubmodule.incl N₁) (LieModule.posFittingComp R L ↥↑N₁) ⊔ LieSubmodule.map (LieSubmodule.incl N₂) (LieModule.posFittingComp R L ↥↑N₂) = LieModule.posFittingComp R L M

theorem LieModule.weightSpace_weightSpaceOf_map_incl {R : Type u_2} {L : Type u_3} {M : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsNilpotent R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (x : L) (χ : L → R) : LieSubmodule.map (LieSubmodule.incl (LieModule.weightSpaceOf M (χ x) x)) (LieModule.weightSpace (↥↑(LieModule.weightSpaceOf M (χ x) x)) χ) = LieModule.weightSpace M χ

theorem LieModule.isCompl_weightSpaceOf_zero_posFittingCompOf (R : Type u_2) (L : Type u_3) (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsNilpotent R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [IsNoetherian R M] [IsArtinian R M] (x : L) : IsCompl (LieModule.weightSpaceOf M 0 x) (LieModule.posFittingCompOf R M x)

theorem LieModule.isCompl_weightSpace_zero_posFittingComp (R : Type u_2) (L : Type u_3) (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsNilpotent R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [IsNoetherian R M] [IsArtinian R M] : IsCompl (LieModule.weightSpace M 0) (LieModule.posFittingComp R L M)

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) [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsNilpotent R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [NoZeroSMulDivisors R M] {x : L} {φ₁ : R} {φ₂ : R} (h : φ₁ ≠ φ₂) : Disjoint (LieModule.weightSpaceOf M φ₁ x) (LieModule.weightSpaceOf M φ₂ x)

theorem LieModule.disjoint_weightSpace (R : Type u_2) (L : Type u_3) (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsNilpotent R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [NoZeroSMulDivisors R M] {χ₁ : L → R} {χ₂ : L → R} (h : χ₁ ≠ χ₂) : Disjoint (LieModule.weightSpace M χ₁) (LieModule.weightSpace M χ₂)

theorem LieModule.injOn_weightSpace (R : Type u_2) (L : Type u_3) (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsNilpotent R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [NoZeroSMulDivisors R M] : Set.InjOn (fun (χ : L → R) => LieModule.weightSpace M χ) {χ : L → R | LieModule.weightSpace M χ ≠ ⊥}

theorem LieModule.independent_weightSpace (R : Type u_2) (L : Type u_3) (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsNilpotent R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [NoZeroSMulDivisors R M] : CompleteLattice.Independent fun (χ : L → R) => LieModule.weightSpace M χ

Lie module weight spaces are independent.

See also LieModule.independent_weightSpace'.

theorem LieModule.independent_weightSpace' (R : Type u_2) (L : Type u_3) (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsNilpotent R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [NoZeroSMulDivisors R M] : CompleteLattice.Independent fun (χ : LieModule.Weight R L M) => LieModule.weightSpace M ⇑χ

theorem LieModule.independent_weightSpaceOf (R : Type u_2) (L : Type u_3) (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsNilpotent R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [NoZeroSMulDivisors R M] (x : L) : CompleteLattice.Independent fun (χ : R) => LieModule.weightSpaceOf M χ x

theorem LieModule.finite_weightSpaceOf_ne_bot (R : Type u_2) (L : Type u_3) (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsNilpotent R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [NoZeroSMulDivisors R M] [IsNoetherian R M] (x : L) : Set.Finite {χ : R | LieModule.weightSpaceOf M χ x ≠ ⊥}

theorem LieModule.finite_weightSpace_ne_bot (R : Type u_2) (L : Type u_3) (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsNilpotent R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [NoZeroSMulDivisors R M] [IsNoetherian R M] : Set.Finite {χ : L → R | LieModule.weightSpace M χ ≠ ⊥}

instance LieModule.Weight.instFinite (R : Type u_2) (L : Type u_3) (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsNilpotent R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [NoZeroSMulDivisors R M] [IsNoetherian R M] : Finite (LieModule.Weight R L M)

Equations

• ⋯ = ⋯

noncomputable instance LieModule.Weight.instFintype (R : Type u_2) (L : Type u_3) (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsNilpotent R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [NoZeroSMulDivisors R M] [IsNoetherian R M] : Fintype (LieModule.Weight R L M)

Equations

• LieModule.Weight.instFintype R L M = Fintype.ofFinite (LieModule.Weight R L M)

class LieModule.IsTriangularizable (R : Type u_2) (L : Type u_3) (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] : Prop

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 : ℕ), (Module.End.generalizedEigenspace ((LieModule.toEndomorphism R L M) x) φ) k = ⊤

@[simp]

theorem LieModule.iSup_weightSpaceOf_eq_top (R : Type u_2) (L : Type u_3) (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsNilpotent R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [LieModule.IsTriangularizable R L M] (x : L) : ⨆ (φ : R), LieModule.weightSpaceOf M φ x = ⊤

@[simp]

theorem LieModule.trace_toEndomorphism_weightSpace (R : Type u_2) (L : Type u_3) (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsNilpotent R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [IsDomain R] [IsPrincipalIdealRing R] [Module.Free R M] [Module.Finite R M] (χ : L → R) (x : L) : (LinearMap.trace R ↥↑(LieModule.weightSpace M χ)) ((LieModule.toEndomorphism R L ↥↑(LieModule.weightSpace M χ)) x) = FiniteDimensional.finrank R ↥↑(LieModule.weightSpace M χ) • χ x

instance LieModule.instIsTriangularizableOfIsAlgClosed (K : Type u_1) (L : Type u_3) (M : Type u_4) [LieRing L] [AddCommGroup M] [LieRingModule L M] [Field K] [LieAlgebra K L] [Module K M] [LieModule K L M] [FiniteDimensional K M] [IsAlgClosed K] : LieModule.IsTriangularizable K L M

Equations

• ⋯ = ⋯

instance LieModule.instIsTriangularizableSubtypeMemSubmoduleToSemiringToCommSemiringToCommRingToEuclideanDomainToAddCommMonoidInstMembershipSetLikeToSubmoduleAddCommGroupToRingToDivisionRingInstModuleSubtypeMemSubmoduleToSemiringToCommSemiringToAddCommMonoidInstMembershipSetLikeToSubmoduleAddCommMonoidInstLieRingModuleSubtypeMemSubmoduleToSemiringToCommSemiringToAddCommMonoidInstMembershipSetLikeToSubmoduleAddCommGroupToRingInstLieModule (K : Type u_1) (L : Type u_3) (M : Type u_4) [LieRing L] [AddCommGroup M] [LieRingModule L M] [Field K] [LieAlgebra K L] [Module K M] [LieModule K L M] [FiniteDimensional K M] (N : LieSubmodule K L M) [LieModule.IsTriangularizable K L M] : LieModule.IsTriangularizable K L ↥↑N

Equations

• ⋯ = ⋯

theorem LieModule.iSup_weightSpace_eq_top (K : Type u_1) (L : Type u_3) (M : Type u_4) [LieRing L] [AddCommGroup M] [LieRingModule L M] [Field K] [LieAlgebra K L] [Module K M] [LieModule K L M] [LieAlgebra.IsNilpotent K L] [FiniteDimensional K M] [LieModule.IsTriangularizable K L M] : ⨆ (χ : L → K), LieModule.weightSpace M χ = ⊤

For a triangularizable Lie module in finite dimensions, the weight spaces span the entire space.

See also LieModule.iSup_weightSpace_eq_top'.

theorem LieModule.iSup_weightSpace_eq_top' (K : Type u_1) (L : Type u_3) (M : Type u_4) [LieRing L] [AddCommGroup M] [LieRingModule L M] [Field K] [LieAlgebra K L] [Module K M] [LieModule K L M] [LieAlgebra.IsNilpotent K L] [FiniteDimensional K M] [LieModule.IsTriangularizable K L M] : ⨆ (χ : LieModule.Weight K L M), LieModule.weightSpace M ⇑χ = ⊤