Theorems · Definition · nonassociative algebras

LieAlgebra.IsKilling.invtSubmoduleToLieIdeal

{K : Type u_1} →
  {L : Type u_2} →
    [inst : Field K] →
      [inst_1 : CharZero K] →
        [inst_2 : LieRing L] →
          [inst_3 : LieAlgebra K L] →
            [inst_4 : FiniteDimensional K L] →
              [inst_5 : LieAlgebra.IsKilling K L] →
                {H : LieSubalgebra K L} →
                  [inst_6 : H.IsCartanSubalgebra] →
                    [inst_7 : LieModule.IsTriangularizable K (↥H) L] →
                      (q : Submodule K (Module.Dual K ↥H)) →
                        (∀ (i : ↥LieSubalgebra.root),
                            q ∈ Module.End.invtSubmodule ↑((LieAlgebra.IsKilling.rootSystem H).reflection i)) →
                          LieIdeal K L

Constructs a Lie ideal from an invariant submodule of the dual space of a Cartan subalgebra. Given a submodule q of the dual space Dual K H that is invariant under all root reflections, this produces a Lie ideal by taking the sum of all sl₂ subalgebras corresponding to roots whose linear forms lie in q.

Defined in

Mathlib.Algebra.Lie.Weights.IsSimple

Cited by

7 results in Mathlib

Foundations

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

Assumes

FieldCharZeroLieRingLieAlgebraFiniteDimensionalLieAlgebra.IsKillingLieSubalgebra.IsCartanSubalgebraLieModule.IsTriangularizable