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.genWeightSpaceOf
• LieModule.genWeightSpace
• LieModule.Weight
• LieModule.posFittingCompOf
• LieModule.posFittingComp
• LieModule.iSup_ucs_eq_genWeightSpace_zero
• LieModule.iInf_lowerCentralSeries_eq_posFittingComp
• LieModule.isCompl_genWeightSpace_zero_posFittingComp
• LieModule.iSupIndep_genWeightSpace
• LieModule.iSup_genWeightSpace_eq_top

References

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

Tags

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

def LieModule.weightSpace {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] (χ : L → R) : LieSubmodule R L M

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

theorem LieModule.mem_weightSpace {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] (χ : L → R) (m : M) : m ∈ weightSpace M χ ↔ ∀ (x : L), ⁅x, m⁆ = χ x • m

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) (x : L) : LinearMap.range (↑g ∘ₗ TensorProduct.mapIncl (((toEnd R L M₁) x).maxGenEigenspace χ₁) (((toEnd R L M₂) x).maxGenEigenspace χ₂)) ≤ ((toEnd R L M₃) x).maxGenEigenspace (χ₁ + χ₂)

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

theorem LieModule.lie_mem_maxGenEigenspace_toEnd {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} {x y : L} {m : M} (hy : y ∈ ((toEnd R L L) x).maxGenEigenspace χ₁) (hm : m ∈ ((toEnd R L M) x).maxGenEigenspace χ₂) : ⁅y, m⁆ ∈ ((toEnd R L M) x).maxGenEigenspace (χ₁ + χ₂)

def LieModule.genWeightSpaceOf {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] [LieRing.IsNilpotent L] (χ : 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 genWeightSpaceOf M χ x is the maximal generalized χ-eigenspace of the action of x on M.

It is a Lie submodule because L is nilpotent.

theorem LieModule.mem_genWeightSpaceOf {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] [LieRing.IsNilpotent L] (χ : R) (x : L) (m : M) : m ∈ genWeightSpaceOf M χ x ↔ ∃ (k : ℕ), (((toEnd R L M) x - χ • 1) ^ k) m = 0

theorem LieModule.coe_genWeightSpaceOf_zero {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] [LieRing.IsNilpotent L] (x : L) : ↑(genWeightSpaceOf M 0 x) = ⨆ (k : ℕ), LinearMap.ker ((toEnd R L M) x ^ k)

def LieModule.genWeightSpace {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] [LieRing.IsNilpotent L] (χ : 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 genWeightSpace 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.

theorem LieModule.mem_genWeightSpace {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] [LieRing.IsNilpotent L] (χ : L → R) (m : M) : m ∈ genWeightSpace M χ ↔ ∀ (x : L), ∃ (k : ℕ), (((toEnd R L M) x - χ x • 1) ^ k) m = 0

theorem LieModule.genWeightSpace_le_genWeightSpaceOf {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] [LieRing.IsNilpotent L] (x : L) (χ : L → R) : genWeightSpace M χ ≤ genWeightSpaceOf M (χ x) x

theorem LieModule.weightSpace_le_genWeightSpace {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] [LieRing.IsNilpotent L] (χ : L → R) : weightSpace M χ ≤ genWeightSpace M χ

structure LieModule.Weight (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] [LieRing.IsNilpotent L] : 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.

• genWeightSpace_ne_bot' : genWeightSpace 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] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [LieRing.IsNilpotent L] : FunLike (Weight R L M) L R

@[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] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [LieRing.IsNilpotent L] (χ : L → R) (h : genWeightSpace M χ ≠ ⊥) : ⇑{ toFun := χ, genWeightSpace_ne_bot' := h } = χ

theorem LieModule.Weight.genWeightSpace_ne_bot {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] [LieRing.IsNilpotent L] (χ : Weight R L M) : genWeightSpace M ⇑χ ≠ ⊥

theorem LieModule.Weight.ext {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] [LieRing.IsNilpotent L] {χ₁ χ₂ : Weight R L M} (h : ∀ (x : L), χ₁ x = χ₂ x) : χ₁ = χ₂

theorem LieModule.Weight.ext_iff {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] [LieRing.IsNilpotent L] {χ₁ χ₂ : Weight R L M} : χ₁ = χ₂ ↔ ∀ (x : L), χ₁ x = χ₂ x

theorem LieModule.Weight.ext_iff' {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] [LieRing.IsNilpotent L] {χ₁ χ₂ : Weight R L M} : ⇑χ₁ = ⇑χ₂ ↔ χ₁ = χ₂

theorem LieModule.Weight.exists_ne_zero {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] [LieRing.IsNilpotent L] (χ : Weight R L M) : ∃ x ∈ genWeightSpace M ⇑χ, x ≠ 0

instance LieModule.Weight.instIsEmptyOfSubsingleton {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] [LieRing.IsNilpotent L] [Subsingleton M] : IsEmpty (Weight R L M)

instance LieModule.Weight.instZeroOfNontrivialSubtypeMemLieSubmoduleGenWeightSpaceOfNatForall {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] [LieRing.IsNilpotent L] [Nontrivial ↥(genWeightSpace M 0)] : Zero (Weight R L M)

@[simp]

theorem LieModule.Weight.coe_zero {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] [LieRing.IsNilpotent L] [Nontrivial ↥(genWeightSpace M 0)] : ⇑0 = 0

theorem LieModule.Weight.zero_apply {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] [LieRing.IsNilpotent L] [Nontrivial ↥(genWeightSpace M 0)] (x : L) : 0 x = 0

def LieModule.Weight.IsZero {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] [LieRing.IsNilpotent L] (χ : 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.

@[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] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [LieRing.IsNilpotent L] {χ : Weight R L M} (hχ : χ.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] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [LieRing.IsNilpotent L] (χ : Weight R L M) : ⇑χ = 0 ↔ χ.IsZero

theorem LieModule.Weight.isZero_iff_eq_zero {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] [LieRing.IsNilpotent L] [Nontrivial ↥(genWeightSpace M 0)] {χ : Weight R L M} : χ.IsZero ↔ χ = 0

theorem LieModule.Weight.isZero_zero {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] [LieRing.IsNilpotent L] [Nontrivial ↥(genWeightSpace M 0)] : IsZero 0

@[reducible, inline]

abbrev LieModule.Weight.IsNonZero {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] [LieRing.IsNilpotent L] (χ : Weight R L M) : Prop

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

theorem LieModule.Weight.isNonZero_iff_ne_zero {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] [LieRing.IsNilpotent L] [Nontrivial ↥(genWeightSpace M 0)] {χ : Weight R L M} : χ.IsNonZero ↔ χ ≠ 0

noncomputable instance LieModule.Weight.instDecidablePredIsNonZero {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] [LieRing.IsNilpotent L] : DecidablePred IsNonZero

def LieModule.Weight.equivSetOf (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] [LieRing.IsNilpotent L] : Weight R L M ≃ ↑{χ : L → R | genWeightSpace M χ ≠ ⊥}

The set of weights is equivalent to a subtype.

theorem LieModule.Weight.genWeightSpaceOf_ne_bot {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] [LieRing.IsNilpotent L] (χ : Weight R L M) (x : L) : genWeightSpaceOf M (χ x) x ≠ ⊥

theorem LieModule.Weight.hasEigenvalueAt {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] [LieRing.IsNilpotent L] (χ : Weight R L M) (x : L) : ((toEnd R L M) x).HasEigenvalue (χ x)

theorem LieModule.Weight.apply_eq_zero_of_isNilpotent {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] [LieRing.IsNilpotent L] [NoZeroSMulDivisors R M] [IsReduced R] (x : L) (h : _root_.IsNilpotent ((toEnd R L M) x)) (χ : Weight R L M) : χ x = 0

@[simp]

theorem LieModule.zero_genWeightSpace_eq_top_of_nilpotent' {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] [LieRing.IsNilpotent L] [IsNilpotent L M] : genWeightSpace M 0 = ⊤

See also the more useful form LieModule.zero_genWeightSpace_eq_top_of_nilpotent.

theorem LieModule.coe_genWeightSpace_of_top {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] [LieRing.IsNilpotent L] (χ : L → R) : ↑(genWeightSpace M (χ ∘ ⇑⊤.incl)) = ↑(genWeightSpace M χ)

@[simp]

theorem LieModule.zero_genWeightSpace_eq_top_of_nilpotent {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] [LieRing.IsNilpotent L] [IsNilpotent L M] : genWeightSpace M 0 = ⊤

theorem LieModule.exists_genWeightSpace_le_ker_of_isNoetherian {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] [LieRing.IsNilpotent L] [IsNoetherian R M] (χ : L → R) (x : L) : ∃ (k : ℕ), ↑(genWeightSpace M χ) ≤ LinearMap.ker (((toEnd R L M) x - (algebraMap R (Module.End R M)) (χ x)) ^ k)

theorem LieModule.exists_genWeightSpace_zero_le_ker_of_isNoetherian (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] [LieRing.IsNilpotent L] [IsNoetherian R M] (x : L) : ∃ (k : ℕ), ↑(genWeightSpace M 0) ≤ LinearMap.ker ((toEnd R L M) x ^ k)

theorem LieModule.isNilpotent_toEnd_sub_algebraMap {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] [LieRing.IsNilpotent L] [IsNoetherian R M] (χ : L → R) (x : L) : _root_.IsNilpotent ((toEnd R L ↥(genWeightSpace M χ)) x - (algebraMap R (Module.End R ↥(genWeightSpace M χ))) (χ x))

theorem LieModule.isNilpotent_toEnd_genWeightSpace_zero {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] [LieRing.IsNilpotent L] [IsNoetherian R M] (x : L) : _root_.IsNilpotent ((toEnd R L ↥(genWeightSpace M 0)) x)

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

instance LieModule.instIsNilpotentSubtypeMemLieSubmoduleGenWeightSpaceOfNatForallOfIsNoetherian {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] [LieRing.IsNilpotent L] [IsNoetherian R M] : IsNilpotent L ↥(genWeightSpace M 0)

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

@[simp]

theorem LieModule.genWeightSpace_zero_normalizer_eq_self (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] [LieRing.IsNilpotent L] : (genWeightSpace M 0).normalizer = genWeightSpace M 0

theorem LieModule.iSup_ucs_le_genWeightSpace_zero (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] [LieRing.IsNilpotent L] : ⨆ (k : ℕ), LieSubmodule.ucs k ⊥ ≤ genWeightSpace M 0

theorem LieModule.iSup_ucs_eq_genWeightSpace_zero (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] [LieRing.IsNilpotent L] [IsNoetherian R M] : ⨆ (k : ℕ), LieSubmodule.ucs k ⊥ = genWeightSpace 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] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [LieRing.IsNilpotent L] (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 := toEnd 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₀ = genWeightSpaceOf M 0 x and M₁ = posFittingCompOf R M x.

It is a Lie submodule because L is nilpotent.

theorem LieModule.mem_posFittingCompOf (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] [LieRing.IsNilpotent L] (x : L) (m : M) : m ∈ posFittingCompOf R M x ↔ ∀ (k : ℕ), ∃ (n : M), ((toEnd 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] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [LieRing.IsNilpotent L] (x : L) (k : ℕ) : posFittingCompOf R M x ≤ 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] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [LieRing.IsNilpotent L] [IsNilpotent L M] (x : L) : 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] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [LieRing.IsNilpotent L] : 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.

theorem LieModule.mem_posFittingComp (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] [LieRing.IsNilpotent L] (m : M) : m ∈ posFittingComp R L M ↔ m ∈ ⨆ (x : L), 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] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [LieRing.IsNilpotent L] (x : L) : posFittingCompOf R M x ≤ 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] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [LieRing.IsNilpotent L] : posFittingComp R L M ≤ ⨅ (k : ℕ), 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] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [LieRing.IsNilpotent L] [IsNoetherian R M] [IsArtinian R M] : ⨅ (k : ℕ), lowerCentralSeries R L M k = posFittingComp R L M

See also LieModule.iSup_ucs_eq_genWeightSpace_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] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [LieRing.IsNilpotent L] [IsNilpotent L M] : 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] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [LieRing.IsNilpotent L] {M₂ : Type u_5} [AddCommGroup M₂] [Module R M₂] [LieRingModule L M₂] [LieModule R L M₂] (f : M →ₗ⁅R,L⁆ M₂) : LieSubmodule.map f (posFittingComp R L M) ≤ posFittingComp R L M₂

theorem LieModule.map_genWeightSpace_le {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] [LieRing.IsNilpotent L] {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 (genWeightSpace M χ) ≤ genWeightSpace M₂ χ

theorem LieModule.comap_genWeightSpace_eq_of_injective {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] [LieRing.IsNilpotent L] {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 (genWeightSpace M₂ χ) = genWeightSpace M χ

theorem LieModule.map_genWeightSpace_eq_of_injective {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] [LieRing.IsNilpotent L] {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 (genWeightSpace M χ) = genWeightSpace M₂ χ ⊓ f.range

theorem LieModule.map_genWeightSpace_eq {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] [LieRing.IsNilpotent L] {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 (genWeightSpace M χ) = genWeightSpace 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] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [LieRing.IsNilpotent L] {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 (posFittingComp R L M) = 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] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [LieRing.IsNilpotent L] [IsNoetherian R M] [IsArtinian R M] {N₁ N₂ : LieSubmodule R L M} (h : Codisjoint N₁ N₂) : LieSubmodule.map N₁.incl (posFittingComp R L ↥N₁) ⊔ LieSubmodule.map N₂.incl (posFittingComp R L ↥N₂) = posFittingComp R L M

theorem LieModule.genWeightSpace_genWeightSpaceOf_map_incl {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] [LieRing.IsNilpotent L] (x : L) (χ : L → R) : LieSubmodule.map (genWeightSpaceOf M (χ x) x).incl (genWeightSpace (↥(genWeightSpaceOf M (χ x) x)) χ) = genWeightSpace M χ

theorem LieModule.isCompl_genWeightSpaceOf_zero_posFittingCompOf (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] [LieRing.IsNilpotent L] [IsNoetherian R M] [IsArtinian R M] (x : L) : IsCompl (genWeightSpaceOf M 0 x) (posFittingCompOf R M x)

theorem LieModule.isCompl_genWeightSpace_zero_posFittingComp (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] [LieRing.IsNilpotent L] [IsNoetherian R M] [IsArtinian R M] : IsCompl (genWeightSpace M 0) (posFittingComp R L M)

This is the Fitting decomposition of the Lie module M.

theorem LieModule.disjoint_genWeightSpaceOf (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] [LieRing.IsNilpotent L] [NoZeroSMulDivisors R M] {x : L} {φ₁ φ₂ : R} (h : φ₁ ≠ φ₂) : Disjoint (genWeightSpaceOf M φ₁ x) (genWeightSpaceOf M φ₂ x)

theorem LieModule.disjoint_genWeightSpace (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] [LieRing.IsNilpotent L] [NoZeroSMulDivisors R M] {χ₁ χ₂ : L → R} (h : χ₁ ≠ χ₂) : Disjoint (genWeightSpace M χ₁) (genWeightSpace M χ₂)

theorem LieModule.injOn_genWeightSpace (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] [LieRing.IsNilpotent L] [NoZeroSMulDivisors R M] : Set.InjOn (fun (χ : L → R) => genWeightSpace M χ) {χ : L → R | genWeightSpace M χ ≠ ⊥}

theorem LieModule.iSupIndep_genWeightSpace (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] [LieRing.IsNilpotent L] [NoZeroSMulDivisors R M] : iSupIndep fun (χ : L → R) => genWeightSpace M χ

Lie module weight spaces are independent.

See also LieModule.iSupIndep_genWeightSpace'.

theorem LieModule.iSupIndep_genWeightSpace' (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] [LieRing.IsNilpotent L] [NoZeroSMulDivisors R M] : iSupIndep fun (χ : Weight R L M) => genWeightSpace M ⇑χ

theorem LieModule.iSupIndep_genWeightSpaceOf (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] [LieRing.IsNilpotent L] [NoZeroSMulDivisors R M] (x : L) : iSupIndep fun (χ : R) => genWeightSpaceOf M χ x

theorem LieModule.finite_genWeightSpaceOf_ne_bot (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] [LieRing.IsNilpotent L] [NoZeroSMulDivisors R M] [IsNoetherian R M] (x : L) : {χ : R | genWeightSpaceOf M χ x ≠ ⊥}.Finite

theorem LieModule.finite_genWeightSpace_ne_bot (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] [LieRing.IsNilpotent L] [NoZeroSMulDivisors R M] [IsNoetherian R M] : {χ : L → R | genWeightSpace M χ ≠ ⊥}.Finite

instance LieModule.Weight.instFinite (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] [LieRing.IsNilpotent L] [NoZeroSMulDivisors R M] [IsNoetherian R M] : Finite (Weight R L M)

noncomputable instance LieModule.Weight.instFintype (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] [LieRing.IsNilpotent L] [NoZeroSMulDivisors R M] [IsNoetherian R M] : Fintype (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 endomorphism of M defined by any x : L is triangularizable.

• maxGenEigenspace_eq_top (x : L) : ⨆ (φ : R), ((toEnd R L M) x).maxGenEigenspace φ = ⊤

instance LieModule.instIsTriangularizableSubtypeMemLieSubalgebra (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] (L' : LieSubalgebra R L) [IsTriangularizable R L M] : IsTriangularizable R (↥L') M

instance LieModule.instIsTriangularizableSubtypeMemLieSubmodule (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] (I : LieIdeal R L) [IsTriangularizable R L M] : IsTriangularizable R (↥I) M

instance LieModule.instIsTriangularizableSubtypeEndMemLieSubalgebraRangeToEnd (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] [IsTriangularizable R L M] : IsTriangularizable R (↥(toEnd R L M).range) M

@[simp]

theorem LieModule.iSup_genWeightSpaceOf_eq_top (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] [LieRing.IsNilpotent L] [IsTriangularizable R L M] (x : L) : ⨆ (φ : R), genWeightSpaceOf M φ x = ⊤

@[simp]

theorem LieModule.trace_toEnd_genWeightSpace (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] [LieRing.IsNilpotent L] [IsDomain R] [IsPrincipalIdealRing R] [Module.Free R M] [Module.Finite R M] (χ : L → R) (x : L) : (LinearMap.trace R ↥(genWeightSpace M χ)) ((toEnd R L ↥(genWeightSpace M χ)) x) = Module.finrank R ↥(genWeightSpace 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] : IsTriangularizable K L M

instance LieModule.instIsTriangularizableSubtypeMemLieSubmodule_1 (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) [IsTriangularizable K L M] : IsTriangularizable K L ↥N

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

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

See also LieModule.iSup_genWeightSpace_eq_top'.

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