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_of_weightSpace_ne_bot: 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

@[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] [NoZeroSMulDivisors R M] [IsNoetherian R M] (χ : { x : L → R // x ∈ 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] [NoZeroSMulDivisors R M] [IsNoetherian R M] (χ : { x : L → R // x ∈ 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 χ = { toAddHom := { toFun := ↑χ, map_add' := (_ : ∀ (x y : L), ↑χ (x + y) = ↑χ x + ↑χ y) }, map_smul' := (_ : ∀ (t : R) (x : L), ↑χ (t • x) = t • ↑χ x) }

@[simp]

theorem LieModule.weight.toLinear_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] [NoZeroSMulDivisors R M] [IsNoetherian R M] (χ : { x : L → R // x ∈ LieModule.weight R L M }) (x : L) (y : L) : ↑χ ⁅x, y⁆ = 0

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

• (_ : LieModule.LinearWeights R L M) = (_ : LieModule.LinearWeights R L M)

theorem LieModule.trace_comp_toEndomorphism_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.toEndomorphism R L ↥↑(LieModule.weightSpace M χ))) = FiniteDimensional.finrank R ↥↑(LieModule.weightSpace M χ) • χ

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

• (_ : LieModule.LinearWeights R L M) = (_ : LieModule.LinearWeights R L M)

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.instLieRingModuleSubtypeMemSubmoduleToSemiringToCommSemiringToAddCommMonoidInstMembershipSetLikeToSubmoduleShiftedWeightSpaceAddCommGroupToRing (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

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

@[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.instLieModuleSubtypeMemSubmoduleToSemiringToCommSemiringToAddCommMonoidInstMembershipSetLikeToSubmoduleShiftedWeightSpaceAddCommGroupToRingInstModuleSubtypeMemSubmoduleToSemiringToCommSemiringToAddCommMonoidInstMembershipSetLikeToSubmoduleAddCommMonoidInstLieRingModuleSubtypeMemSubmoduleToSemiringToCommSemiringToAddCommMonoidInstMembershipSetLikeToSubmoduleShiftedWeightSpaceAddCommGroupToRing (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

• (_ : LieModule R L ↥↑(LieModule.shiftedWeightSpace R L M χ)) = (_ : LieModule R L ↥↑(LieModule.shiftedWeightSpace R L M χ))

@[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 χ)), (LinearEquiv.symm (LieModule.shiftedWeightSpace.shift R L M χ)) 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.toEndomorphism_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.toEndomorphism R L ↥↑(LieModule.shiftedWeightSpace R L M χ)) x = (LinearEquiv.conj (LieModule.shiftedWeightSpace.shift R L M χ)) ((LieModule.toEndomorphism R L ↥↑(LieModule.weightSpace M χ)) x - χ x • LinearMap.id)

instance LieModule.shiftedWeightSpace.instIsNilpotentSubtypeMemSubmoduleToSemiringToCommSemiringToAddCommMonoidInstMembershipSetLikeToSubmoduleShiftedWeightSpaceAddCommGroupToRingInstModuleSubtypeMemSubmoduleToSemiringToCommSemiringToAddCommMonoidInstMembershipSetLikeToSubmoduleAddCommMonoidInstLieRingModuleSubtypeMemSubmoduleToSemiringToCommSemiringToAddCommMonoidInstMembershipSetLikeToSubmoduleShiftedWeightSpaceAddCommGroupToRing (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

• (_ : LieModule.IsNilpotent R L ↥↑(LieModule.shiftedWeightSpace R L M χ)) = (_ : LieModule.IsNilpotent R L ↥↑(LieModule.shiftedWeightSpace R L M χ))

theorem LieModule.exists_forall_lie_eq_smul_of_weightSpace_ne_bot (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] (hχ : LieModule.weightSpace 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.