Theorems · Definition · nonassociative algebras

LieAlgebra.corootSpace

{R : Type u_1} →
  {L : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : LieRing L] →
        [inst_2 : LieAlgebra R L] →
          {H : LieSubalgebra R L} →
            [LieRing.IsNilpotent ↥H] → [H.IsCartanSubalgebra] → [IsNoetherian R L] → (↥H → R) → LieIdeal R ↥H

Given a root α relative to a Cartan subalgebra H, this is the span of all products of an element of the α root space and an element of the -α root space. Informally it is often denoted ⁅H(α), H(-α)⁆. If the Killing form is non-degenerate and the coefficients are a perfect field, this space is one-dimensional. See LieAlgebra.IsKilling.coe_corootSpace_eq_span_singleton and LieAlgebra.IsKilling.coe_corootSpace_eq_span_singleton'. Note that the name "coroot space" is not standard as this space does not seem to have a name in the informal literature.

Defined in

Mathlib.Algebra.Lie.Weights.Cartan

Cited by

23 results in Mathlib

Foundations

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

Assumes

CommRingLieRingLieAlgebraLieRing.IsNilpotentLieSubalgebra.IsCartanSubalgebraIsNoetherian