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.weightSpaceOf {R : Type u_2} {L : Type u_3} (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsNilpotent R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (χ : R) (x : L) :

If M is a representation of a nilpotent Lie algebra L, χ is a scalar, and x : L, then weightSpaceOf 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_weightSpaceOf {R : Type u_2} {L : Type u_3} (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsNilpotent R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (χ : R) (x : L) (m : M) :
    m LieModule.weightSpaceOf M χ x ∃ (k : ), (((LieModule.toEnd R L M) x - χ 1) ^ k) m = 0
    theorem LieModule.coe_weightSpaceOf_zero {R : Type u_2} {L : Type u_3} (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsNilpotent R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (x : L) :
    (LieModule.weightSpaceOf M 0 x) = ⨆ (k : ), LinearMap.ker ((LieModule.toEnd R L M) x ^ k)
    def LieModule.weightSpace {R : Type u_2} {L : Type u_3} (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsNilpotent R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (χ : LR) :

    If M is a representation of a nilpotent Lie algebra L and χ : L → R is a family of scalars, then weightSpace 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_weightSpace {R : Type u_2} {L : Type u_3} (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsNilpotent R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (χ : LR) (m : M) :
      m LieModule.weightSpace M χ ∀ (x : L), ∃ (k : ), (((LieModule.toEnd R L M) x - χ x 1) ^ k) m = 0
      theorem LieModule.weightSpace_le_weightSpaceOf {R : Type u_2} {L : Type u_3} (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsNilpotent R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (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] [LieAlgebra.IsNilpotent R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] :
      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
        theorem LieModule.Weight.weightSpace_ne_bot' {R : Type u_2} {L : Type u_3} {M : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsNilpotent R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (self : LieModule.Weight R L M) :
        instance LieModule.Weight.instFunLike {R : Type u_2} {L : Type u_3} (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsNilpotent R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] :
        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] [LieAlgebra.IsNilpotent R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (χ : LR) (h : LieModule.weightSpace M χ ) :
        { toFun := χ, weightSpace_ne_bot' := h } = χ
        theorem LieModule.Weight.ext {R : Type u_2} {L : Type u_3} {M : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsNilpotent R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {χ₁ : 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] [LieAlgebra.IsNilpotent R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {χ₁ : 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] [LieAlgebra.IsNilpotent R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (χ : LieModule.Weight R L M) :
        xLieModule.weightSpace M χ, x 0
        Equations
        • =
        Equations
        • LieModule.Weight.instZeroOfNontrivialSubtypeMemSubmoduleWeightSpaceOfNatForall = { zero := { toFun := 0, weightSpace_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] [LieAlgebra.IsNilpotent R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [Nontrivial (LieModule.weightSpace 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] [LieAlgebra.IsNilpotent R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [Nontrivial (LieModule.weightSpace 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] [LieAlgebra.IsNilpotent R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (χ : 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] [LieAlgebra.IsNilpotent R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {χ : 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] [LieAlgebra.IsNilpotent R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (χ : 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] [LieAlgebra.IsNilpotent R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [Nontrivial (LieModule.weightSpace 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] [LieAlgebra.IsNilpotent R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (χ : 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] [LieAlgebra.IsNilpotent R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [Nontrivial (LieModule.weightSpace M 0)] {χ : LieModule.Weight R L M} :
            χ.IsNonZero χ 0
            def LieModule.Weight.equivSetOf (R : Type u_2) (L : Type u_3) (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsNilpotent R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] :
            LieModule.Weight R L M {χ : LR | LieModule.weightSpace 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.weightSpaceOf_ne_bot {R : Type u_2} {L : Type u_3} {M : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsNilpotent R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (χ : 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] [LieAlgebra.IsNilpotent R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (χ : 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] [LieAlgebra.IsNilpotent R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [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_weightSpace_of_top {R : Type u_2} {L : Type u_3} (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsNilpotent R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (χ : LR) :
              (LieModule.weightSpace M (χ .incl)) = (LieModule.weightSpace M χ)
              theorem LieModule.exists_weightSpace_le_ker_of_isNoetherian {R : Type u_2} {L : Type u_3} (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsNilpotent R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [IsNoetherian R M] (χ : LR) (x : L) :
              ∃ (k : ), (LieModule.weightSpace 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] [LieAlgebra.IsNilpotent R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [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] [LieAlgebra.IsNilpotent R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (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₀ = weightSpaceOf 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] [LieAlgebra.IsNilpotent R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (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] [LieAlgebra.IsNilpotent R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule 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.

                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] [LieAlgebra.IsNilpotent R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (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] [LieAlgebra.IsNilpotent R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {M₂ : Type u_5} [AddCommGroup M₂] [Module R M₂] [LieRingModule L M₂] [LieModule R L M₂] (f : M →ₗ⁅R,L M₂) :
                  theorem LieModule.map_weightSpace_le {R : Type u_2} {L : Type u_3} {M : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsNilpotent R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {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_weightSpace_eq_of_injective {R : Type u_2} {L : Type u_3} {M : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsNilpotent R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {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_weightSpace_eq_of_injective {R : Type u_2} {L : Type u_3} {M : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsNilpotent R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {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_weightSpace_eq {R : Type u_2} {L : Type u_3} {M : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsNilpotent R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {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] [LieAlgebra.IsNilpotent R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {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] [LieAlgebra.IsNilpotent R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [IsNoetherian R M] [IsArtinian R M] {N₁ : LieSubmodule R L M} {N₂ : LieSubmodule R L M} (h : Codisjoint N₁ N₂) :
                  theorem LieModule.weightSpace_weightSpaceOf_map_incl {R : Type u_2} {L : Type u_3} {M : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsNilpotent R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (x : L) (χ : LR) :

                  This is the Fitting decomposition of the Lie module M.

                  theorem LieModule.disjoint_weightSpaceOf (R : Type u_2) (L : Type u_3) (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsNilpotent R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [NoZeroSMulDivisors R M] {x : L} {φ₁ : R} {φ₂ : R} (h : φ₁ φ₂) :
                  theorem LieModule.disjoint_weightSpace (R : Type u_2) (L : Type u_3) (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsNilpotent R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [NoZeroSMulDivisors R M] {χ₁ : LR} {χ₂ : LR} (h : χ₁ χ₂) :
                  theorem LieModule.injOn_weightSpace (R : Type u_2) (L : Type u_3) (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsNilpotent R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [NoZeroSMulDivisors R M] :
                  Set.InjOn (fun (χ : LR) => LieModule.weightSpace M χ) {χ : LR | LieModule.weightSpace M χ }

                  Lie module weight spaces are independent.

                  See also LieModule.independent_weightSpace'.

                  theorem LieModule.finite_weightSpaceOf_ne_bot (R : Type u_2) (L : Type u_3) (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsNilpotent R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [NoZeroSMulDivisors R M] [IsNoetherian R M] (x : L) :
                  {χ : R | LieModule.weightSpaceOf M χ x }.Finite
                  theorem LieModule.finite_weightSpace_ne_bot (R : Type u_2) (L : Type u_3) (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsNilpotent R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [NoZeroSMulDivisors R M] [IsNoetherian R M] :
                  {χ : LR | LieModule.weightSpace 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] [LieAlgebra.IsNilpotent R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [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} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [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_weightSpaceOf_eq_top (R : Type u_2) (L : Type u_3) (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsNilpotent R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [LieModule.IsTriangularizable R L M] (x : L) :
                    ⨆ (φ : R), LieModule.weightSpaceOf M φ x =
                    @[simp]
                    theorem LieModule.trace_toEnd_weightSpace (R : Type u_2) (L : Type u_3) (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsNilpotent 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] (χ : LR) (x : L) :
                    Equations
                    • =
                    Equations
                    • =
                    theorem LieModule.iSup_weightSpace_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.weightSpace M χ =

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

                    See also LieModule.iSup_weightSpace_eq_top'.