Documentation

Mathlib.Algebra.Lie.Weights.Basic

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 #

References #

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 (((LieModule.toEnd R L M₁) x).maxGenEigenspace χ₁) (((LieModule.toEnd R L M₂) x).maxGenEigenspace χ₂)) ((LieModule.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} {χ₂ : R} {x : L} {y : L} {m : M} (hy : y ((LieModule.toEnd R L L) x).maxGenEigenspace χ₁) (hm : m ((LieModule.toEnd R L M) x).maxGenEigenspace χ₂) :
y, m ((LieModule.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] [LieAlgebra.IsNilpotent R L] (χ : R) (x : L) :

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.

Equations
Instances For
    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] [LieAlgebra.IsNilpotent R L] (χ : R) (x : L) (m : M) :
    m LieModule.genWeightSpaceOf M χ x ∃ (k : ), (((LieModule.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] [LieAlgebra.IsNilpotent R L] (x : L) :
    (LieModule.genWeightSpaceOf M 0 x) = ⨆ (k : ), LinearMap.ker ((LieModule.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] [LieAlgebra.IsNilpotent R L] (χ : LR) :

    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.

    Equations
    Instances For
      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] [LieAlgebra.IsNilpotent R L] (χ : LR) (m : M) :
      m LieModule.genWeightSpace M χ ∀ (x : L), ∃ (k : ), (((LieModule.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] [LieAlgebra.IsNilpotent R L] (x : L) (χ : LR) :
      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] [LieAlgebra.IsNilpotent R 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.

      Instances For
        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] [LieAlgebra.IsNilpotent R L] :
        Equations
        @[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] [LieAlgebra.IsNilpotent R L] (χ : LR) (h : LieModule.genWeightSpace M χ ) :
        { toFun := χ, genWeightSpace_ne_bot' := h } = χ
        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] [LieAlgebra.IsNilpotent R L] {χ₁ : LieModule.Weight R L M} {χ₂ : LieModule.Weight R L M} :
        χ₁ = χ₂ ∀ (x : L), χ₁ x = χ₂ x
        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] [LieAlgebra.IsNilpotent R L] {χ₁ : LieModule.Weight R L M} {χ₂ : LieModule.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] [LieAlgebra.IsNilpotent R L] {χ₁ : LieModule.Weight R L M} {χ₂ : LieModule.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] [LieAlgebra.IsNilpotent R L] (χ : LieModule.Weight R L M) :
        xLieModule.genWeightSpace M χ, x 0
        Equations
        • =
        Equations
        • LieModule.Weight.instZeroOfNontrivialSubtypeMemLieSubmoduleGenWeightSpaceOfNatForall = { zero := { toFun := 0, genWeightSpace_ne_bot' := } }
        @[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] [LieAlgebra.IsNilpotent R L] [Nontrivial (LieModule.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] [LieAlgebra.IsNilpotent R L] [Nontrivial (LieModule.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] [LieAlgebra.IsNilpotent R L] (χ : LieModule.Weight R L M) :

        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
        • χ.IsZero = (χ = 0)
        Instances For
          @[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] [LieAlgebra.IsNilpotent R L] {χ : LieModule.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] [LieAlgebra.IsNilpotent R L] (χ : LieModule.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] [LieAlgebra.IsNilpotent R L] [Nontrivial (LieModule.genWeightSpace M 0)] {χ : LieModule.Weight R L M} :
          χ.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] [LieAlgebra.IsNilpotent R L] (χ : LieModule.Weight R L M) :

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

          Equations
          • χ.IsNonZero = ¬χ.IsZero
          Instances For
            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] [LieAlgebra.IsNilpotent R L] [Nontrivial (LieModule.genWeightSpace M 0)] {χ : LieModule.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] [LieAlgebra.IsNilpotent R L] :
            DecidablePred LieModule.Weight.IsNonZero
            Equations
            • LieModule.Weight.instDecidablePredIsNonZero = Classical.decPred LieModule.Weight.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] [LieAlgebra.IsNilpotent R L] :
            LieModule.Weight R L M {χ : LR | LieModule.genWeightSpace M χ }

            The set of weights is equivalent to a subtype.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              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] [LieAlgebra.IsNilpotent R L] (χ : LieModule.Weight R L M) (x : L) :
              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] [LieAlgebra.IsNilpotent R L] (χ : LieModule.Weight R L M) (x : L) :
              ((LieModule.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] [LieAlgebra.IsNilpotent R L] [NoZeroSMulDivisors R M] [IsReduced R] (x : L) (h : IsNilpotent ((LieModule.toEnd R L M) x)) (χ : LieModule.Weight R L M) :
              χ x = 0
              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] [LieAlgebra.IsNilpotent R L] (χ : LR) :
              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] [LieAlgebra.IsNilpotent R L] [IsNoetherian R M] (χ : LR) (x : L) :
              ∃ (k : ), (LieModule.genWeightSpace M χ) LinearMap.ker (((LieModule.toEnd R L M) x - (algebraMap R (Module.End R 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] [LieAlgebra.IsNilpotent R L] [IsNoetherian R M] (χ : LR) (x : L) :

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

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

              Equations
              • =
              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] [LieAlgebra.IsNilpotent R L] (x : L) :

              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.

              Equations
              Instances For
                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] [LieAlgebra.IsNilpotent R L] (x : L) (m : M) :
                m LieModule.posFittingCompOf R M x ∀ (k : ), ∃ (n : M), ((LieModule.toEnd R L M) x ^ k) n = m
                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] [LieAlgebra.IsNilpotent R L] :

                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
                Instances For
                  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] [LieAlgebra.IsNilpotent R L] (m : 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] [LieAlgebra.IsNilpotent R L] {M₂ : Type u_5} [AddCommGroup M₂] [Module R M₂] [LieRingModule L M₂] [LieModule R L M₂] (f : M →ₗ⁅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] [LieAlgebra.IsNilpotent R L] {M₂ : Type u_5} [AddCommGroup M₂] [Module R M₂] [LieRingModule L M₂] [LieModule R L M₂] {χ : LR} (f : M →ₗ⁅R,L 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] [LieAlgebra.IsNilpotent R L] {M₂ : Type u_5} [AddCommGroup M₂] [Module R M₂] [LieRingModule L M₂] [LieModule R L M₂] {χ : LR} {f : M →ₗ⁅R,L M₂} (hf : Function.Injective f) :
                  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] [LieAlgebra.IsNilpotent R L] {M₂ : Type u_5} [AddCommGroup M₂] [Module R M₂] [LieRingModule L M₂] [LieModule R L M₂] {χ : LR} {f : M →ₗ⁅R,L M₂} (hf : Function.Injective f) :
                  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] [LieAlgebra.IsNilpotent R L] {M₂ : Type u_5} [AddCommGroup M₂] [Module R M₂] [LieRingModule L M₂] [LieModule R L M₂] {χ : LR} (e : M ≃ₗ⁅R,L 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] [LieAlgebra.IsNilpotent R L] {M₂ : Type u_5} [AddCommGroup M₂] [Module R M₂] [LieRingModule L M₂] [LieModule R L M₂] (e : M ≃ₗ⁅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] [LieAlgebra.IsNilpotent R L] [IsNoetherian R M] [IsArtinian R M] {N₁ : LieSubmodule R L M} {N₂ : LieSubmodule R L M} (h : Codisjoint N₁ N₂) :

                  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] [LieAlgebra.IsNilpotent R L] [NoZeroSMulDivisors R M] {x : L} {φ₁ : R} {φ₂ : R} (h : φ₁ φ₂) :
                  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] [LieAlgebra.IsNilpotent R L] [NoZeroSMulDivisors R M] {χ₁ : LR} {χ₂ : LR} (h : χ₁ χ₂) :
                  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] [LieAlgebra.IsNilpotent R L] [NoZeroSMulDivisors R M] :
                  Set.InjOn (fun (χ : LR) => LieModule.genWeightSpace M χ) {χ : LR | LieModule.genWeightSpace M χ }

                  Lie module weight spaces are independent.

                  See also LieModule.independent_genWeightSpace'.

                  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] [LieAlgebra.IsNilpotent R L] [NoZeroSMulDivisors R M] [IsNoetherian R M] (x : L) :
                  {χ : R | LieModule.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] [LieAlgebra.IsNilpotent R L] [NoZeroSMulDivisors R M] [IsNoetherian R M] :
                  {χ : LR | LieModule.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] [LieAlgebra.IsNilpotent R L] [NoZeroSMulDivisors R M] [IsNoetherian R M] :
                  Equations
                  • =
                  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] :

                  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 : ), (((LieModule.toEnd R L M) x).genEigenspace φ) k =
                  Instances
                    theorem LieModule.IsTriangularizable.iSup_eq_top {R : Type u_2} {L : Type u_3} {M : Type u_4} :
                    ∀ {inst : CommRing R} {inst_1 : LieRing L} {inst_2 : LieAlgebra R L} {inst_3 : AddCommGroup M} {inst_4 : Module R M} {inst_5 : LieRingModule L M} {inst_6 : LieModule R L M} [self : LieModule.IsTriangularizable R L M] (x : L), ⨆ (φ : R), ⨆ (k : ), (((LieModule.toEnd R L M) x).genEigenspace φ) k =
                    Equations
                    • =
                    Equations
                    • =
                    @[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] [LieAlgebra.IsNilpotent R L] [LieModule.IsTriangularizable R L M] (x : L) :
                    ⨆ (φ : R), LieModule.genWeightSpaceOf M φ x =
                    Equations
                    • =
                    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] [Field K] [LieAlgebra K L] [Module K M] [LieModule K L M] [LieAlgebra.IsNilpotent K L] [FiniteDimensional K M] [LieModule.IsTriangularizable K L M] :
                    ⨆ (χ : LK), LieModule.genWeightSpace M χ =

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

                    See also LieModule.iSup_genWeightSpace_eq_top'.