Lie modules with linear weights

Given a Lie module M over a nilpotent Lie algebra L with coefficients in R, one frequently studies M via its weights. These are functions χ : L → R whose corresponding weight space LieModule.weightSpace M χ, is non-trivial. If L is Abelian or if R has characteristic zero (and M is finite-dimensional) then such χ are necessarily R-linear. However in general non-linear weights do exist. For example if we take:

• R: the field with two elements (or indeed any perfect field of characteristic two),
• L: sl₂ (this is nilpotent in characteristic two),
• M: the natural two-dimensional representation of L,

then there is a single weight and it is non-linear. (See remark following Proposition 9 of chapter VII, §1.3 in N. Bourbaki, Chapters 7--9.)

We thus introduce a typeclass LieModule.LinearWeights to encode the fact that a Lie module does have linear weights and provide typeclass instances in the two important cases that L is Abelian or R has characteristic zero.

Main definitions

• LieModule.LinearWeights: a typeclass encoding the fact that a given Lie module has linear weights, and furthermore that the weights vanish on the derived ideal.
• LieModule.instLinearWeightsOfCharZero: a typeclass instance encoding the fact that for an Abelian Lie algebra, the weights of any Lie module are linear.
• LieModule.instLinearWeightsOfIsLieAbelian: a typeclass instance encoding the fact that in characteristic zero, the weights of any finite-dimensional Lie module are linear.
• LieModule.exists_forall_lie_eq_smul: existence of simultaneous eigenvectors from existence of simultaneous generalized eigenvectors for Noetherian Lie modules with linear weights.

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

A typeclass encoding the fact that a given Lie module has linear weights, vanishing on the derived ideal.

• map_add : ∀ (χ : L → R), LieModule.weightSpace M χ ≠ ⊥ → ∀ (x y : L), χ (x + y) = χ x + χ y
• map_smul : ∀ (χ : L → R), LieModule.weightSpace M χ ≠ ⊥ → ∀ (t : R) (x : L), χ (t • x) = t • χ x
• map_lie : ∀ (χ : L → R), LieModule.weightSpace M χ ≠ ⊥ → ∀ (x y : L), χ ⁅x, y⁆ = 0

theorem LieModule.LinearWeights.map_add {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [LieAlgebra.IsNilpotent R L] [self : LieModule.LinearWeights R L M] (χ : L → R) : LieModule.weightSpace M χ ≠ ⊥ → ∀ (x y : L), χ (x + y) = χ x + χ y

theorem LieModule.LinearWeights.map_smul {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [LieAlgebra.IsNilpotent R L] [self : LieModule.LinearWeights R L M] (χ : L → R) : LieModule.weightSpace M χ ≠ ⊥ → ∀ (t : R) (x : L), χ (t • x) = t • χ x

theorem LieModule.LinearWeights.map_lie {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [LieAlgebra.IsNilpotent R L] [self : LieModule.LinearWeights R L M] (χ : L → R) : LieModule.weightSpace M χ ≠ ⊥ → ∀ (x y : L), χ ⁅x, y⁆ = 0

@[simp]

theorem LieModule.Weight.toLinear_apply (R : Type u_1) (L : Type u_2) (M : Type u_3) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [LieAlgebra.IsNilpotent R L] [LieModule.LinearWeights R L M] (χ : LieModule.Weight R L M) (a : L) : (LieModule.Weight.toLinear R L M χ) a = χ a

def LieModule.Weight.toLinear (R : Type u_1) (L : Type u_2) (M : Type u_3) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [LieAlgebra.IsNilpotent R L] [LieModule.LinearWeights R L M] (χ : LieModule.Weight R L M) : L →ₗ[R] R

A weight of a Lie module, bundled as a linear map.

Equations

• LieModule.Weight.toLinear R L M χ = { toFun := ⇑χ, map_add' := ⋯, map_smul' := ⋯ }

instance LieModule.Weight.instCoeLinearMap (R : Type u_1) (L : Type u_2) (M : Type u_3) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [LieAlgebra.IsNilpotent R L] [LieModule.LinearWeights R L M] : CoeOut (LieModule.Weight R L M) (L →ₗ[R] R)

Equations

• LieModule.Weight.instCoeLinearMap R L M = { coe := LieModule.Weight.toLinear R L M }

instance LieModule.Weight.instLinearMapClass (R : Type u_1) (L : Type u_2) (M : Type u_3) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [LieAlgebra.IsNilpotent R L] [LieModule.LinearWeights R L M] : LinearMapClass (LieModule.Weight R L M) R L R

Equations

• ⋯ = ⋯

@[simp]

theorem LieModule.Weight.apply_lie {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [LieAlgebra.IsNilpotent R L] [LieModule.LinearWeights R L M] {χ : LieModule.Weight R L M} (x : L) (y : L) : χ ⁅x, y⁆ = 0

@[simp]

theorem LieModule.Weight.coe_coe {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [LieAlgebra.IsNilpotent R L] [LieModule.LinearWeights R L M] {χ : LieModule.Weight R L M} : ⇑(LieModule.Weight.toLinear R L M χ) = ⇑χ

@[simp]

theorem LieModule.Weight.coe_toLinear_eq_zero_iff {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [LieAlgebra.IsNilpotent R L] [LieModule.LinearWeights R L M] {χ : LieModule.Weight R L M} : LieModule.Weight.toLinear R L M χ = 0 ↔ χ.IsZero

theorem LieModule.Weight.coe_toLinear_ne_zero_iff {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [LieAlgebra.IsNilpotent R L] [LieModule.LinearWeights R L M] {χ : LieModule.Weight R L M} : LieModule.Weight.toLinear R L M χ ≠ 0 ↔ χ.IsNonZero

@[reducible, inline]

abbrev LieModule.Weight.ker {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [LieAlgebra.IsNilpotent R L] [LieModule.LinearWeights R L M] {χ : LieModule.Weight R L M} : Submodule R L

The kernel of a weight of a Lie module with linear weights.

Equations

• LieModule.Weight.ker = LinearMap.ker (LieModule.Weight.toLinear R L M χ)

instance LieModule.instLinearWeightsOfIsLieAbelian (R : Type u_1) (L : Type u_2) (M : Type u_3) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [IsLieAbelian L] [NoZeroSMulDivisors R M] : LieModule.LinearWeights R L M

For an Abelian Lie algebra, the weights of any Lie module are linear.

Equations

• ⋯ = ⋯

theorem LieModule.trace_comp_toEnd_weightSpace_eq (R : Type u_1) (L : Type u_2) (M : Type u_3) [CommRing R] [LieRing L] [LieAlgebra 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] [LieAlgebra.IsNilpotent R L] (χ : L → R) : ⇑(LinearMap.trace R ↥↑(LieModule.weightSpace M χ) ∘ₗ ↑(LieModule.toEnd R L ↥↑(LieModule.weightSpace M χ))) = FiniteDimensional.finrank R ↥↑(LieModule.weightSpace M χ) • χ

@[deprecated LieModule.trace_comp_toEnd_weightSpace_eq]

theorem LieModule.trace_comp_toEnd_weight_space_eq (R : Type u_1) (L : Type u_2) (M : Type u_3) [CommRing R] [LieRing L] [LieAlgebra 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] [LieAlgebra.IsNilpotent R L] (χ : L → R) : ⇑(LinearMap.trace R ↥↑(LieModule.weightSpace M χ) ∘ₗ ↑(LieModule.toEnd R L ↥↑(LieModule.weightSpace M χ))) = FiniteDimensional.finrank R ↥↑(LieModule.weightSpace M χ) • χ

Alias of LieModule.trace_comp_toEnd_weightSpace_eq.

theorem LieModule.zero_lt_finrank_weightSpace {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra 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] [LieAlgebra.IsNilpotent R L] {χ : L → R} (hχ : LieModule.weightSpace M χ ≠ ⊥) : 0 < FiniteDimensional.finrank R ↥↑(LieModule.weightSpace M χ)

instance LieModule.instLinearWeightsOfCharZero (R : Type u_1) (L : Type u_2) (M : Type u_3) [CommRing R] [LieRing L] [LieAlgebra 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] [LieAlgebra.IsNilpotent R L] [CharZero R] : LieModule.LinearWeights R L M

In characteristic zero, the weights of any finite-dimensional Lie module are linear and vanish on the derived ideal.

Equations

• ⋯ = ⋯

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

A type synonym for the χ-weight space but with the action of x : L on m : weightSpace M χ, shifted to act as ⁅x, m⁆ - χ x • m.

Equations

• LieModule.shiftedWeightSpace R L M χ = LieModule.weightSpace M χ

instance LieModule.shiftedWeightSpace.instLieRingModuleSubtypeMemSubmodule (R : Type u_1) (L : Type u_2) (M : Type u_3) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [LieAlgebra.IsNilpotent R L] [LieModule.LinearWeights R L M] (χ : L → R) : LieRingModule L ↥↑(LieModule.shiftedWeightSpace R L M χ)

Equations

• LieModule.shiftedWeightSpace.instLieRingModuleSubtypeMemSubmodule R L M χ = LieRingModule.mk ⋯ ⋯ ⋯

@[simp]

theorem LieModule.shiftedWeightSpace.coe_lie_shiftedWeightSpace_apply (R : Type u_1) (L : Type u_2) (M : Type u_3) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [LieAlgebra.IsNilpotent R L] [LieModule.LinearWeights R L M] (χ : L → R) (x : L) (m : ↥(LieModule.shiftedWeightSpace R L M χ)) : ↑⁅x, m⁆ = ⁅x, ↑m⁆ - χ x • ↑m

instance LieModule.shiftedWeightSpace.instSubtypeMemSubmodule (R : Type u_1) (L : Type u_2) (M : Type u_3) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [LieAlgebra.IsNilpotent R L] [LieModule.LinearWeights R L M] (χ : L → R) : LieModule R L ↥↑(LieModule.shiftedWeightSpace R L M χ)

Equations

• ⋯ = ⋯

@[simp]

theorem LieModule.shiftedWeightSpace.shift_symm_apply (R : Type u_1) (L : Type u_2) (M : Type u_3) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [LieAlgebra.IsNilpotent R L] (χ : L → R) : ∀ (a : ↥↑(LieModule.weightSpace M χ)), (LieModule.shiftedWeightSpace.shift R L M χ).symm a = a

@[simp]

theorem LieModule.shiftedWeightSpace.shift_apply (R : Type u_1) (L : Type u_2) (M : Type u_3) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [LieAlgebra.IsNilpotent R L] (χ : L → R) (a : ↥↑(LieModule.weightSpace M χ)) : (LieModule.shiftedWeightSpace.shift R L M χ) a = a

def LieModule.shiftedWeightSpace.shift (R : Type u_1) (L : Type u_2) (M : Type u_3) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [LieAlgebra.IsNilpotent R L] (χ : L → R) : ↥↑(LieModule.weightSpace M χ) ≃ₗ[R] ↥↑(LieModule.shiftedWeightSpace R L M χ)

Forgetting the action of L, the spaces weightSpace M χ and shiftedWeightSpace R L M χ are equivalent.

Equations

• LieModule.shiftedWeightSpace.shift R L M χ = LinearEquiv.refl R ↥↑(LieModule.weightSpace M χ)

theorem LieModule.shiftedWeightSpace.toEnd_eq (R : Type u_1) (L : Type u_2) (M : Type u_3) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [LieAlgebra.IsNilpotent R L] [LieModule.LinearWeights R L M] (χ : L → R) (x : L) : (LieModule.toEnd R L ↥↑(LieModule.shiftedWeightSpace R L M χ)) x = (LieModule.shiftedWeightSpace.shift R L M χ).conj ((LieModule.toEnd R L ↥↑(LieModule.weightSpace M χ)) x - χ x • LinearMap.id)

instance LieModule.shiftedWeightSpace.instIsNilpotentSubtypeMemSubmoduleOfIsNoetherian (R : Type u_1) (L : Type u_2) (M : Type u_3) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [LieAlgebra.IsNilpotent R L] [LieModule.LinearWeights R L M] (χ : L → R) [IsNoetherian R M] : LieModule.IsNilpotent R L ↥↑(LieModule.shiftedWeightSpace R L M χ)

By Engel's theorem, if M is Noetherian, the shifted action ⁅x, m⁆ - χ x • m makes the χ-weight space into a nilpotent Lie module.

Equations

• ⋯ = ⋯

theorem LieModule.exists_forall_lie_eq_smul (R : Type u_1) (L : Type u_2) (M : Type u_3) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [LieAlgebra.IsNilpotent R L] [LieModule.LinearWeights R L M] [IsNoetherian R M] (χ : LieModule.Weight R L M) : ∃ (m : M), m ≠ 0 ∧ ∀ (x : L), ⁅x, m⁆ = χ x • m

Given a Lie module M of a Lie algebra L with coefficients in R, if a function χ : L → R has a simultaneous generalized eigenvector for the action of L then it has a simultaneous true eigenvector, provided M is Noetherian and has linear weights.