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

source
๐Ÿ”ธ coverage
def LieModule.weightSpace {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] (ฯ‡ : L โ†’ R) :
LieSubmodule R L M

If M is a representation of a Lie algebra L and ฯ‡ : L โ†’ R is a family of scalars, then weightSpace M ฯ‡ is the intersection of the ฯ‡ x-eigenspaces of the action of x on M as x ranges over L.

Equations
    Instances For
      source
      ๐Ÿ“ coverage
      theorem LieModule.mem_weightSpace {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] (ฯ‡ : L โ†’ R) (m : M) :
      m โˆˆ weightSpace M ฯ‡ โ†” โˆ€ (x : L), โ…x, mโ† = ฯ‡ x โ€ข m
      source
      ๐Ÿ“ coverage
      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) (x : L) :
      (โ†‘g โˆ˜โ‚— TensorProduct.mapIncl (((toEnd R L Mโ‚) x).maxGenEigenspace ฯ‡โ‚) (((toEnd R L Mโ‚‚) x).maxGenEigenspace ฯ‡โ‚‚)).range โ‰ค ((toEnd R L Mโ‚ƒ) x).maxGenEigenspace (ฯ‡โ‚ + ฯ‡โ‚‚)

      See also bourbaki1975b Chapter VII ยง1.1, Proposition 2 (ii).

      source
      ๐Ÿ“ coverage
      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} {x y : L} {m : M} (hy : y โˆˆ ((toEnd R L L) x).maxGenEigenspace ฯ‡โ‚) (hm : m โˆˆ ((toEnd R L M) x).maxGenEigenspace ฯ‡โ‚‚) :
      โ…y, mโ† โˆˆ ((toEnd R L M) x).maxGenEigenspace (ฯ‡โ‚ + ฯ‡โ‚‚)
      source
      ๐Ÿ”ธ coverage
      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] [LieRing.IsNilpotent L] (ฯ‡ : R) (x : L) :
      LieSubmodule R L M

      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
          source
          ๐Ÿ“ coverage
          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] [LieRing.IsNilpotent L] (ฯ‡ : R) (x : L) (m : M) :
          m โˆˆ genWeightSpaceOf M ฯ‡ x โ†” โˆƒ (k : โ„•), (((toEnd R L M) x - ฯ‡ โ€ข 1) ^ k) m = 0
          source
          ๐Ÿ“ coverage
          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] [LieRing.IsNilpotent L] (x : L) :
          โ†‘(genWeightSpaceOf M 0 x) = โจ† (k : โ„•), ((toEnd R L M) x ^ k).ker
          source
          ๐Ÿ”ธ coverage
          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] [LieRing.IsNilpotent L] (ฯ‡ : L โ†’ R) :
          LieSubmodule R L M

          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
              source
              ๐Ÿ“ coverage
              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] [LieRing.IsNilpotent L] (ฯ‡ : L โ†’ R) (m : M) :
              m โˆˆ genWeightSpace M ฯ‡ โ†” โˆ€ (x : L), โˆƒ (k : โ„•), (((toEnd R L M) x - ฯ‡ x โ€ข 1) ^ k) m = 0
              source
              ๐Ÿ“ coverage
              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] [LieRing.IsNilpotent L] (x : L) (ฯ‡ : L โ†’ R) :
              genWeightSpace M ฯ‡ โ‰ค genWeightSpaceOf M (ฯ‡ x) x
              source
              ๐Ÿ“ coverage
              theorem LieModule.weightSpace_le_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] [LieRing.IsNilpotent L] (ฯ‡ : L โ†’ R) :
              weightSpace M ฯ‡ โ‰ค genWeightSpace M ฯ‡
              source
              ๐Ÿ”ถ coverage
              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] [LieRing.IsNilpotent 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
                source
                ๐Ÿ”ธ coverage
                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] [LieRing.IsNilpotent L] :
                FunLike (Weight R L M) L R
                Equations
                  source
                  ๐Ÿ“ coverage
                  @[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] [LieRing.IsNilpotent L] (ฯ‡ : L โ†’ R) (h : genWeightSpace M ฯ‡ โ‰  โŠฅ) :
                  โ‡‘{ toFun := ฯ‡, genWeightSpace_ne_bot' := h } = ฯ‡
                  source
                  theorem LieModule.Weight.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] [LieRing.IsNilpotent L] (ฯ‡ : Weight R L M) :
                  genWeightSpace M โ‡‘ฯ‡ โ‰  โŠฅ
                  source
                  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] [LieRing.IsNilpotent L] {ฯ‡โ‚ ฯ‡โ‚‚ : Weight R L M} (h : โˆ€ (x : L), ฯ‡โ‚ x = ฯ‡โ‚‚ x) :
                  ฯ‡โ‚ = ฯ‡โ‚‚
                  source
                  ๐Ÿ“ coverage
                  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] [LieRing.IsNilpotent L] {ฯ‡โ‚ ฯ‡โ‚‚ : Weight R L M} :
                  ฯ‡โ‚ = ฯ‡โ‚‚ โ†” โˆ€ (x : L), ฯ‡โ‚ x = ฯ‡โ‚‚ x
                  source
                  ๐Ÿ“ coverage
                  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] [LieRing.IsNilpotent L] {ฯ‡โ‚ ฯ‡โ‚‚ : Weight R L M} :
                  โ‡‘ฯ‡โ‚ = โ‡‘ฯ‡โ‚‚ โ†” ฯ‡โ‚ = ฯ‡โ‚‚
                  source
                  ๐Ÿ“ coverage
                  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] [LieRing.IsNilpotent L] (ฯ‡ : Weight R L M) :
                  โˆƒ x โˆˆ genWeightSpace M โ‡‘ฯ‡, x โ‰  0
                  source
                  ๐Ÿ“ coverage
                  instance LieModule.Weight.instIsEmptyOfSubsingleton {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] [LieRing.IsNilpotent L] [Subsingleton M] :
                  IsEmpty (Weight R L M)
                  source
                  ๐Ÿ”ธ coverage
                  instance LieModule.Weight.instZeroOfNontrivialSubtypeMemLieSubmoduleGenWeightSpaceOfNatForall {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] [LieRing.IsNilpotent L] [Nontrivial โ†ฅ(genWeightSpace M 0)] :
                  Zero (Weight R L M)
                  Equations
                    source
                    ๐Ÿ“ coverage
                    @[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] [LieRing.IsNilpotent L] [Nontrivial โ†ฅ(genWeightSpace M 0)] :
                    โ‡‘0 = 0
                    source
                    ๐Ÿ“ coverage
                    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] [LieRing.IsNilpotent L] [Nontrivial โ†ฅ(genWeightSpace M 0)] (x : L) :
                    0 x = 0
                    source
                    ๐Ÿ”น coverage
                    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] [LieRing.IsNilpotent L] (ฯ‡ : Weight R L M) :
                    Prop

                    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
                      Instances For
                        source
                        ๐Ÿ“ coverage
                        @[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] [LieRing.IsNilpotent L] {ฯ‡ : Weight R L M} (hฯ‡ : ฯ‡.IsZero) :
                        โ‡‘ฯ‡ = 0
                        source
                        ๐Ÿ“ coverage
                        @[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] [LieRing.IsNilpotent L] (ฯ‡ : Weight R L M) :
                        โ‡‘ฯ‡ = 0 โ†” ฯ‡.IsZero
                        source
                        ๐Ÿ“ coverage
                        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] [LieRing.IsNilpotent L] [Nontrivial โ†ฅ(genWeightSpace M 0)] {ฯ‡ : Weight R L M} :
                        ฯ‡.IsZero โ†” ฯ‡ = 0
                        source
                        ๐Ÿ“ coverage
                        theorem LieModule.Weight.isZero_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] [LieRing.IsNilpotent L] [Nontrivial โ†ฅ(genWeightSpace M 0)] :
                        IsZero 0
                        source
                        ๐Ÿ”น coverage
                        @[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] [LieRing.IsNilpotent L] (ฯ‡ : Weight R L M) :
                        Prop

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

                        Equations
                          Instances For
                            source
                            ๐Ÿ“ coverage
                            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] [LieRing.IsNilpotent L] [Nontrivial โ†ฅ(genWeightSpace M 0)] {ฯ‡ : Weight R L M} :
                            ฯ‡.IsNonZero โ†” ฯ‡ โ‰  0
                            source
                            ๐Ÿ”ธ coverage
                            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] [LieRing.IsNilpotent L] :
                            DecidablePred IsNonZero
                            Equations
                              source
                              ๐Ÿ”ธ coverage
                              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] [LieRing.IsNilpotent L] :
                              Weight R L M โ‰ƒ โ†‘{ฯ‡ : L โ†’ R | genWeightSpace M ฯ‡ โ‰  โŠฅ}

                              The set of weights is equivalent to a subtype.

                              Equations
                                Instances For
                                  source
                                  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] [LieRing.IsNilpotent L] (ฯ‡ : Weight R L M) (x : L) :
                                  genWeightSpaceOf M (ฯ‡ x) x โ‰  โŠฅ
                                  source
                                  ๐Ÿ“ coverage
                                  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] [LieRing.IsNilpotent L] (ฯ‡ : Weight R L M) (x : L) :
                                  ((toEnd R L M) x).HasEigenvalue (ฯ‡ x)
                                  source
                                  ๐Ÿ“ coverage
                                  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] [LieRing.IsNilpotent L] [IsDomain R] [Module.IsTorsionFree R M] [IsReduced R] (x : L) (h : _root_.IsNilpotent ((toEnd R L M) x)) (ฯ‡ : Weight R L M) :
                                  ฯ‡ x = 0
                                  source
                                  ๐Ÿ“ coverage
                                  @[simp]
                                  theorem LieModule.zero_genWeightSpace_eq_top_of_nilpotent' {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] [LieRing.IsNilpotent L] [IsNilpotent L M] :
                                  genWeightSpace M 0 = โŠค

                                  See also the more useful form LieModule.zero_genWeightSpace_eq_top_of_nilpotent.

                                  source
                                  ๐Ÿ“ coverage
                                  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] [LieRing.IsNilpotent L] (ฯ‡ : L โ†’ R) :
                                  โ†‘(genWeightSpace M (ฯ‡ โˆ˜ โ‡‘โŠค.incl)) = โ†‘(genWeightSpace M ฯ‡)
                                  source
                                  ๐Ÿ“ coverage
                                  @[simp]
                                  theorem LieModule.zero_genWeightSpace_eq_top_of_nilpotent {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] [LieRing.IsNilpotent L] [IsNilpotent L M] :
                                  genWeightSpace M 0 = โŠค
                                  source
                                  ๐Ÿ“ coverage
                                  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] [LieRing.IsNilpotent L] [IsNoetherian R M] (ฯ‡ : L โ†’ R) (x : L) :
                                  โˆƒ (k : โ„•), โ†‘(genWeightSpace M ฯ‡) โ‰ค LinearMap.ker (((toEnd R L M) x - (algebraMap R (Module.End R M)) (ฯ‡ x)) ^ k)
                                  source
                                  ๐Ÿ“ coverage
                                  theorem LieModule.exists_genWeightSpace_zero_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] [LieRing.IsNilpotent L] [IsNoetherian R M] (x : L) :
                                  โˆƒ (k : โ„•), โ†‘(genWeightSpace M 0) โ‰ค LinearMap.ker ((toEnd R L M) x ^ k)
                                  source
                                  ๐Ÿ“ coverage
                                  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] [LieRing.IsNilpotent L] [IsNoetherian R M] (ฯ‡ : L โ†’ R) (x : L) :
                                  _root_.IsNilpotent ((toEnd R L โ†ฅ(genWeightSpace M ฯ‡)) x - (algebraMap R (Module.End R โ†ฅ(genWeightSpace M ฯ‡))) (ฯ‡ x))
                                  source
                                  ๐Ÿ“ coverage
                                  theorem LieModule.isNilpotent_toEnd_genWeightSpace_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] [LieRing.IsNilpotent L] [IsNoetherian R M] (x : L) :
                                  _root_.IsNilpotent ((toEnd R L โ†ฅ(genWeightSpace M 0)) x)

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

                                  source
                                  ๐Ÿ“ coverage
                                  instance LieModule.instIsNilpotentSubtypeMemLieSubmoduleGenWeightSpaceOfNatForallOfIsNoetherian {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] [LieRing.IsNilpotent L] [IsNoetherian R M] :
                                  IsNilpotent L โ†ฅ(genWeightSpace M 0)

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

                                  source
                                  ๐Ÿ“ coverage
                                  @[simp]
                                  theorem LieModule.genWeightSpace_zero_normalizer_eq_self (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] [LieRing.IsNilpotent L] :
                                  (genWeightSpace M 0).normalizer = genWeightSpace M 0
                                  source
                                  ๐Ÿ“ coverage
                                  theorem LieModule.iSup_ucs_le_genWeightSpace_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] [LieRing.IsNilpotent L] :
                                  โจ† (k : โ„•), LieSubmodule.ucs k โŠฅ โ‰ค genWeightSpace M 0
                                  source
                                  ๐Ÿ“ coverage
                                  theorem LieModule.iSup_ucs_eq_genWeightSpace_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] [LieRing.IsNilpotent L] [IsNoetherian R M] :
                                  โจ† (k : โ„•), LieSubmodule.ucs k โŠฅ = genWeightSpace M 0

                                  See also LieModule.iInf_lowerCentralSeries_eq_posFittingComp.

                                  source
                                  ๐Ÿ”ธ coverage
                                  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] [LieRing.IsNilpotent L] (x : L) :
                                  LieSubmodule R L M

                                  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
                                      source
                                      ๐Ÿ“ coverage
                                      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] [LieRing.IsNilpotent L] (x : L) (m : M) :
                                      m โˆˆ posFittingCompOf R M x โ†” โˆ€ (k : โ„•), โˆƒ (n : M), ((toEnd R L M) x ^ k) n = m
                                      source
                                      ๐Ÿ“ coverage
                                      @[simp]
                                      theorem LieModule.posFittingCompOf_le_lowerCentralSeries (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] [LieRing.IsNilpotent L] (x : L) (k : โ„•) :
                                      posFittingCompOf R M x โ‰ค lowerCentralSeries R L M k
                                      source
                                      ๐Ÿ“ coverage
                                      @[simp]
                                      theorem LieModule.posFittingCompOf_eq_bot_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] [LieRing.IsNilpotent L] [IsNilpotent L M] (x : L) :
                                      posFittingCompOf R M x = โŠฅ
                                      source
                                      ๐Ÿ”ธ coverage
                                      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] [LieRing.IsNilpotent L] :
                                      LieSubmodule 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
                                          source
                                          ๐Ÿ“ coverage
                                          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] [LieRing.IsNilpotent L] (m : M) :
                                          m โˆˆ posFittingComp R L M โ†” m โˆˆ โจ† (x : L), posFittingCompOf R M x
                                          source
                                          ๐Ÿ“ coverage
                                          theorem LieModule.posFittingCompOf_le_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] [LieRing.IsNilpotent L] (x : L) :
                                          posFittingCompOf R M x โ‰ค posFittingComp R L M
                                          source
                                          ๐Ÿ“ coverage
                                          theorem LieModule.posFittingComp_le_iInf_lowerCentralSeries (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] [LieRing.IsNilpotent L] :
                                          posFittingComp R L M โ‰ค โจ… (k : โ„•), lowerCentralSeries R L M k
                                          source
                                          ๐Ÿ“ coverage
                                          @[simp]
                                          theorem LieModule.iInf_lowerCentralSeries_eq_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] [LieRing.IsNilpotent L] [IsNoetherian R M] [IsArtinian R M] :
                                          โจ… (k : โ„•), lowerCentralSeries R L M k = posFittingComp R L M

                                          See also LieModule.iSup_ucs_eq_genWeightSpace_zero.

                                          source
                                          ๐Ÿ“ coverage
                                          @[simp]
                                          theorem LieModule.posFittingComp_eq_bot_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] [LieRing.IsNilpotent L] [IsNilpotent L M] :
                                          posFittingComp R L M = โŠฅ
                                          source
                                          ๐Ÿ“ coverage
                                          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] [LieRing.IsNilpotent L] {Mโ‚‚ : Type u_5} [AddCommGroup Mโ‚‚] [Module R Mโ‚‚] [LieRingModule L Mโ‚‚] [LieModule R L Mโ‚‚] (f : M โ†’โ‚—โ…R,Lโ† Mโ‚‚) :
                                          LieSubmodule.map f (posFittingComp R L M) โ‰ค posFittingComp R L Mโ‚‚
                                          source
                                          ๐Ÿ“ coverage
                                          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] [LieRing.IsNilpotent L] {Mโ‚‚ : Type u_5} [AddCommGroup Mโ‚‚] [Module R Mโ‚‚] [LieRingModule L Mโ‚‚] [LieModule R L Mโ‚‚] {ฯ‡ : L โ†’ R} (f : M โ†’โ‚—โ…R,Lโ† Mโ‚‚) :
                                          LieSubmodule.map f (genWeightSpace M ฯ‡) โ‰ค genWeightSpace Mโ‚‚ ฯ‡
                                          source
                                          ๐Ÿ“ coverage
                                          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] [LieRing.IsNilpotent L] {Mโ‚‚ : Type u_5} [AddCommGroup Mโ‚‚] [Module R Mโ‚‚] [LieRingModule L Mโ‚‚] [LieModule R L Mโ‚‚] {ฯ‡ : L โ†’ R} {f : M โ†’โ‚—โ…R,Lโ† Mโ‚‚} (hf : Function.Injective โ‡‘f) :
                                          LieSubmodule.comap f (genWeightSpace Mโ‚‚ ฯ‡) = genWeightSpace M ฯ‡
                                          source
                                          ๐Ÿ“ coverage
                                          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] [LieRing.IsNilpotent L] {Mโ‚‚ : Type u_5} [AddCommGroup Mโ‚‚] [Module R Mโ‚‚] [LieRingModule L Mโ‚‚] [LieModule R L Mโ‚‚] {ฯ‡ : L โ†’ R} {f : M โ†’โ‚—โ…R,Lโ† Mโ‚‚} (hf : Function.Injective โ‡‘f) :
                                          LieSubmodule.map f (genWeightSpace M ฯ‡) = genWeightSpace Mโ‚‚ ฯ‡ โŠ“ f.range
                                          source
                                          ๐Ÿ“ coverage
                                          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] [LieRing.IsNilpotent L] {Mโ‚‚ : Type u_5} [AddCommGroup Mโ‚‚] [Module R Mโ‚‚] [LieRingModule L Mโ‚‚] [LieModule R L Mโ‚‚] {ฯ‡ : L โ†’ R} (e : M โ‰ƒโ‚—โ…R,Lโ† Mโ‚‚) :
                                          LieSubmodule.map e.toLieModuleHom (genWeightSpace M ฯ‡) = genWeightSpace Mโ‚‚ ฯ‡
                                          source
                                          ๐Ÿ“ coverage
                                          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] [LieRing.IsNilpotent L] {Mโ‚‚ : Type u_5} [AddCommGroup Mโ‚‚] [Module R Mโ‚‚] [LieRingModule L Mโ‚‚] [LieModule R L Mโ‚‚] (e : M โ‰ƒโ‚—โ…R,Lโ† Mโ‚‚) :
                                          LieSubmodule.map e.toLieModuleHom (posFittingComp R L M) = posFittingComp R L Mโ‚‚
                                          source
                                          ๐Ÿ“ coverage
                                          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] [LieRing.IsNilpotent L] [IsNoetherian R M] [IsArtinian R M] {Nโ‚ Nโ‚‚ : LieSubmodule R L M} (h : Codisjoint Nโ‚ Nโ‚‚) :
                                          LieSubmodule.map Nโ‚.incl (posFittingComp R L โ†ฅNโ‚) โŠ” LieSubmodule.map Nโ‚‚.incl (posFittingComp R L โ†ฅNโ‚‚) = posFittingComp R L M
                                          source
                                          ๐Ÿ“ coverage
                                          theorem LieModule.genWeightSpace_genWeightSpaceOf_map_incl {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] [LieRing.IsNilpotent L] (x : L) (ฯ‡ : L โ†’ R) :
                                          LieSubmodule.map (genWeightSpaceOf M (ฯ‡ x) x).incl (genWeightSpace (โ†ฅ(genWeightSpaceOf M (ฯ‡ x) x)) ฯ‡) = genWeightSpace M ฯ‡
                                          source
                                          ๐Ÿ“ coverage
                                          theorem LieModule.isCompl_genWeightSpaceOf_zero_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] [LieRing.IsNilpotent L] [IsNoetherian R M] [IsArtinian R M] (x : L) :
                                          IsCompl (genWeightSpaceOf M 0 x) (posFittingCompOf R M x)
                                          source
                                          ๐Ÿ“ coverage
                                          theorem LieModule.isCompl_genWeightSpace_zero_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] [LieRing.IsNilpotent L] [IsNoetherian R M] [IsArtinian R M] :
                                          IsCompl (genWeightSpace M 0) (posFittingComp R L M)

                                          This is the Fitting decomposition of the Lie module M.

                                          source
                                          ๐Ÿ“ coverage
                                          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] [LieRing.IsNilpotent L] [IsDomain R] [Module.IsTorsionFree R M] {x : L} {ฯ†โ‚ ฯ†โ‚‚ : R} (h : ฯ†โ‚ โ‰  ฯ†โ‚‚) :
                                          Disjoint (genWeightSpaceOf M ฯ†โ‚ x) (genWeightSpaceOf M ฯ†โ‚‚ x)
                                          source
                                          ๐Ÿ“ coverage
                                          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] [LieRing.IsNilpotent L] [IsDomain R] [Module.IsTorsionFree R M] {ฯ‡โ‚ ฯ‡โ‚‚ : L โ†’ R} (h : ฯ‡โ‚ โ‰  ฯ‡โ‚‚) :
                                          Disjoint (genWeightSpace M ฯ‡โ‚) (genWeightSpace M ฯ‡โ‚‚)
                                          source
                                          ๐Ÿ“ coverage
                                          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] [LieRing.IsNilpotent L] [IsDomain R] [Module.IsTorsionFree R M] :
                                          Set.InjOn (fun (ฯ‡ : L โ†’ R) => genWeightSpace M ฯ‡) {ฯ‡ : L โ†’ R | genWeightSpace M ฯ‡ โ‰  โŠฅ}
                                          source
                                          ๐Ÿ“ coverage
                                          theorem LieModule.iSupIndep_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] [LieRing.IsNilpotent L] [IsDomain R] [Module.IsTorsionFree R M] :
                                          iSupIndep fun (ฯ‡ : L โ†’ R) => genWeightSpace M ฯ‡

                                          Lie module weight spaces are independent.

                                          See also LieModule.iSupIndep_genWeightSpace'.

                                          source
                                          ๐Ÿ“ coverage
                                          theorem LieModule.iSupIndep_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] [LieRing.IsNilpotent L] [IsDomain R] [Module.IsTorsionFree R M] :
                                          iSupIndep fun (ฯ‡ : Weight R L M) => genWeightSpace M โ‡‘ฯ‡
                                          source
                                          ๐Ÿ“ coverage
                                          theorem LieModule.iSupIndep_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] [LieRing.IsNilpotent L] [IsDomain R] [Module.IsTorsionFree R M] (x : L) :
                                          iSupIndep fun (ฯ‡ : R) => genWeightSpaceOf M ฯ‡ x
                                          source
                                          ๐Ÿ“ coverage
                                          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] [LieRing.IsNilpotent L] [IsDomain R] [Module.IsTorsionFree R M] [IsNoetherian R M] (x : L) :
                                          {ฯ‡ : R | genWeightSpaceOf M ฯ‡ x โ‰  โŠฅ}.Finite
                                          source
                                          ๐Ÿ“ coverage
                                          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] [LieRing.IsNilpotent L] [IsDomain R] [Module.IsTorsionFree R M] [IsNoetherian R M] :
                                          {ฯ‡ : L โ†’ R | genWeightSpace M ฯ‡ โ‰  โŠฅ}.Finite
                                          source
                                          ๐Ÿ“ coverage
                                          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] [LieRing.IsNilpotent L] [IsDomain R] [Module.IsTorsionFree R M] [IsNoetherian R M] :
                                          Finite (Weight R L M)
                                          source
                                          ๐Ÿ”ธ coverage
                                          noncomputable instance LieModule.Weight.instFintype (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] [LieRing.IsNilpotent L] [IsDomain R] [Module.IsTorsionFree R M] [IsNoetherian R M] :
                                          Fintype (Weight R L M)
                                          Equations
                                            source
                                            ๐Ÿ”ถ coverage
                                            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] :
                                            Prop

                                            A Lie module M of a Lie algebra L is triangularizable if the endomorphism of M defined by any x : L is triangularizable.

                                            Instances
                                              source
                                              ๐Ÿ“ coverage
                                              instance LieModule.instIsTriangularizableSubtypeMemLieSubalgebra (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] (L' : LieSubalgebra R L) [IsTriangularizable R L M] :
                                              IsTriangularizable R (โ†ฅL') M
                                              source
                                              ๐Ÿ“ coverage
                                              instance LieModule.instIsTriangularizableSubtypeMemLieSubmodule (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] (I : LieIdeal R L) [IsTriangularizable R L M] :
                                              IsTriangularizable R (โ†ฅI) M
                                              source
                                              ๐Ÿ“ coverage
                                              instance LieModule.instIsTriangularizableSubtypeEndMemLieSubalgebraRangeToEnd (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] [IsTriangularizable R L M] :
                                              IsTriangularizable R (โ†ฅ(toEnd R L M).range) M
                                              source
                                              ๐Ÿ“ coverage
                                              @[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] [LieRing.IsNilpotent L] [IsTriangularizable R L M] (x : L) :
                                              โจ† (ฯ† : R), genWeightSpaceOf M ฯ† x = โŠค
                                              source
                                              ๐Ÿ“ coverage
                                              @[simp]
                                              theorem LieModule.trace_toEnd_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] [LieRing.IsNilpotent L] [IsDomain R] [IsPrincipalIdealRing R] [Module.Free R M] [Module.Finite R M] (ฯ‡ : L โ†’ R) (x : L) :
                                              (LinearMap.trace R โ†ฅ(genWeightSpace M ฯ‡)) ((toEnd R L โ†ฅ(genWeightSpace M ฯ‡)) x) = Module.finrank R โ†ฅ(genWeightSpace M ฯ‡) โ€ข ฯ‡ x
                                              source
                                              ๐Ÿ“ coverage
                                              instance LieModule.instIsTriangularizableOfIsAlgClosed (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] [FiniteDimensional K M] [IsAlgClosed K] :
                                              IsTriangularizable K L M
                                              source
                                              ๐Ÿ“ coverage
                                              instance LieModule.instIsTriangularizableSubtypeMemLieSubmodule_1 (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] [FiniteDimensional K M] (N : LieSubmodule K L M) [IsTriangularizable K L M] :
                                              IsTriangularizable K L โ†ฅN
                                              source
                                              ๐Ÿ“ coverage
                                              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] [LieRing.IsNilpotent L] [Field K] [LieAlgebra K L] [Module K M] [LieModule K L M] [FiniteDimensional K M] [IsTriangularizable K L M] :
                                              โจ† (ฯ‡ : L โ†’ K), genWeightSpace M ฯ‡ = โŠค

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

                                              See also LieModule.iSup_genWeightSpace_eq_top'.

                                              source
                                              ๐Ÿ“ coverage
                                              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] [LieRing.IsNilpotent L] [Field K] [LieAlgebra K L] [Module K M] [LieModule K L M] [FiniteDimensional K M] [IsTriangularizable K L M] :
                                              โจ† (ฯ‡ : Weight K L M), genWeightSpace M โ‡‘ฯ‡ = โŠค