Documentation

Mathlib.Algebra.Lie.Weights.Linear

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.genWeightSpace 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:

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 #

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

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

Instances
    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] (χ : LR) :
    LieModule.genWeightSpace 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] (χ : LR) :
    LieModule.genWeightSpace 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] (χ : LR) :
    LieModule.genWeightSpace 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) :

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

    Equations
    Instances For
      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} :

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

      Equations
      Instances For

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

        Equations
        • =
        @[deprecated LieModule.trace_comp_toEnd_genWeightSpace_eq]

        Alias of LieModule.trace_comp_toEnd_genWeightSpace_eq.

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

        Equations
        • =
        def LieModule.shiftedGenWeightSpace (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] (χ : LR) :

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

        Equations
        Instances For
          @[simp]
          theorem LieModule.shiftedGenWeightSpace.coe_lie_shiftedGenWeightSpace_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] (χ : LR) [LieModule.LinearWeights R L M] (x : L) (m : (LieModule.shiftedGenWeightSpace R L M χ)) :
          x, m = x, m - χ x m
          Equations
          • =
          @[simp]
          theorem LieModule.shiftedGenWeightSpace.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] (χ : LR) :
          ∀ (a : (LieModule.genWeightSpace M χ)), (LieModule.shiftedGenWeightSpace.shift R L M χ).symm a = a
          @[simp]
          theorem LieModule.shiftedGenWeightSpace.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] (χ : LR) (a : (LieModule.genWeightSpace M χ)) :
          def LieModule.shiftedGenWeightSpace.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] (χ : LR) :

          Forgetting the action of L, the spaces genWeightSpace M χ and shiftedGenWeightSpace R L M χ are equivalent.

          Equations
          Instances For
            theorem LieModule.shiftedGenWeightSpace.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] (χ : LR) [LieModule.LinearWeights R L M] (x : L) :

            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.