Theorems · Definition · nonassociative algebras

LieModule.weightSpaceOfIsLieTower

(R : Type u_1) →
  {L : Type u_2} →
    {A : Type u_3} →
      (V : Type u_4) →
        [inst : CommRing R] →
          [IsPrincipalIdealRing R] →
            [IsDomain R] →
              [CharZero R] →
                [inst_4 : LieRing L] →
                  [inst_5 : LieAlgebra R L] →
                    [inst_6 : LieRing A] →
                      [inst_7 : LieAlgebra R A] →
                        [inst_8 : Bracket L A] →
                          [inst_9 : Bracket A L] →
                            [inst_10 : AddCommGroup V] →
                              [inst_11 : Module R V] →
                                [Module.Free R V] →
                                  [Module.Finite R V] →
                                    [inst_14 : LieRingModule L V] →
                                      [LieModule R L V] →
                                        [inst_16 : LieRingModule A V] →
                                          [LieModule R A V] →
                                            [IsLieTower L A V] → [IsLieTower A L V] → (A → R) → LieSubmodule R L V

The weight space of V with respect to χ : A → R, a priori a Lie submodule for A, is also a Lie submodule for L.

Defined in

Mathlib.Algebra.Lie.LieTheorem

Cited by

2 results in Mathlib

Foundations

Depth 124 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingIsPrincipalIdealRingIsDomainCharZeroLieRingLieAlgebraLieRingLieAlgebraBracketBracketAddCommGroupModuleModule.FreeModule.FiniteLieRingModuleLieModuleLieRingModuleLieModuleIsLieTowerIsLieTower