Lie ideals, invariant root submodules, and simple Lie algebras

Given a semisimple Lie algebra, the lattice of ideals is order isomorphic to the lattice of Weyl-group-invariant submodules of the corresponding root system. In this file we provide LieIdeal.toInvtRootSubmodule, which constructs the invariant submodule associated to an ideal, and LieAlgebra.IsKilling.invtSubmoduleToLieIdeal, which constructs the ideal associated to an invariant submodule.

As of Mar 2026, the proofs that these maps are part of an order isomorphism is still pending.

Main definitions

• LieIdeal.rootSet: the set of roots whose root space is contained in a given Lie ideal.
• LieIdeal.rootSpan: the submodule of Dual K H spanned by LieIdeal.rootSet.
• LieIdeal.toInvtRootSubmodule: the invariant root submodule associated to an ideal.
• LieAlgebra.IsKilling.invtSubmoduleToLieIdeal: constructs a Lie ideal from an invariant submodule of the dual space

Main results

• LieAlgebra.IsKilling.instIsIrreducible: the root system of a simple Lie algebra is irreducible

theorem LieIdeal.corootSubmodule_le {K : Type u_1} {L : Type u_2} [Field K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] (I : LieIdeal K L) {α : LieModule.Weight K (↥H) L} (hα : LieAlgebra.rootSpace H ⇑α ≤ LieSubmodule.restr I H) : LieAlgebra.IsKilling.corootSubmodule α ≤ LieSubmodule.restr I H

def LieIdeal.rootSet {K : Type u_1} {L : Type u_2} [Field K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] (I : LieIdeal K L) : Set ↥LieSubalgebra.root

The set of roots whose root space is contained in a given Lie ideal.

Equations

• I.rootSet = {α : ↥LieSubalgebra.root | LieAlgebra.rootSpace H ⇑↑α ≤ LieSubmodule.restr I H}

@[simp]

theorem LieIdeal.mem_rootSet {K : Type u_1} {L : Type u_2} [Field K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] {I : LieIdeal K L} {α : ↥LieSubalgebra.root} : α ∈ I.rootSet ↔ LieAlgebra.rootSpace H ⇑↑α ≤ LieSubmodule.restr I H

noncomputable def LieIdeal.rootSpan {K : Type u_1} {L : Type u_2} [Field K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [CharZero K] [LieAlgebra.IsKilling K L] [LieModule.IsTriangularizable K (↥H) L] (I : LieIdeal K L) : Submodule K (Module.Dual K ↥H)

The submodule of Dual K H spanned by the roots associated to a Lie ideal.

Equations

• I.rootSpan = Submodule.span K (⇑(LieAlgebra.IsKilling.rootSystem H).root '' I.rootSet)

theorem LieIdeal.rootSpace_le_of_apply_coroot_ne_zero {K : Type u_1} {L : Type u_2} [Field K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [CharZero K] [LieAlgebra.IsKilling K L] [LieModule.IsTriangularizable K (↥H) L] (I : LieIdeal K L) {α : LieModule.Weight K (↥H) L} (hα : LieAlgebra.rootSpace H ⇑α ≤ LieSubmodule.restr I H) {γ : ↥H → K} (hγ_ne : γ (LieAlgebra.IsKilling.coroot α) ≠ 0) : LieAlgebra.rootSpace H γ ≤ LieSubmodule.restr I H

theorem LieIdeal.reflectionPerm_mem_rootSet_iff {K : Type u_1} {L : Type u_2} [Field K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [CharZero K] [LieAlgebra.IsKilling K L] [LieModule.IsTriangularizable K (↥H) L] (I : LieIdeal K L) (α β : ↥LieSubalgebra.root) : ((LieAlgebra.IsKilling.rootSystem H).reflectionPerm β) α ∈ I.rootSet ↔ α ∈ I.rootSet

theorem LieIdeal.rootSpan_mem_invtRootSubmodule {K : Type u_1} {L : Type u_2} [Field K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [CharZero K] [LieAlgebra.IsKilling K L] [LieModule.IsTriangularizable K (↥H) L] (I : LieIdeal K L) : I.rootSpan ∈ (LieAlgebra.IsKilling.rootSystem H).invtRootSubmodule

The submodule spanned by roots of a Lie ideal is invariant under all root reflections.

noncomputable def LieIdeal.toInvtRootSubmodule {K : Type u_1} {L : Type u_2} [Field K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [CharZero K] [LieAlgebra.IsKilling K L] [LieModule.IsTriangularizable K (↥H) L] (I : LieIdeal K L) : ↥(LieAlgebra.IsKilling.rootSystem H).invtRootSubmodule

The invariant root submodule corresponding to a Lie ideal.

Given a Lie ideal I, this produces an invariant root submodule by taking the span of all roots whose root spaces are contained in I.

Equations

• I.toInvtRootSubmodule = ⟨I.rootSpan, ⋯⟩

theorem LieIdeal.toInvtRootSubmodule_mono {K : Type u_1} {L : Type u_2} [Field K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [CharZero K] [LieAlgebra.IsKilling K L] [LieModule.IsTriangularizable K (↥H) L] {I J : LieIdeal K L} (h : I ≤ J) : I.toInvtRootSubmodule ≤ J.toInvtRootSubmodule

noncomputable def LieAlgebra.IsKilling.invtSubmoduleToLieIdeal {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [IsKilling K L] [LieModule.IsTriangularizable K (↥H) L] (q : Submodule K (Module.Dual K ↥H)) (hq : ∀ (i : ↥LieSubalgebra.root), q ∈ Module.End.invtSubmodule ↑((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.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem LieAlgebra.IsKilling.coe_invtSubmoduleToLieIdeal_eq_iSup {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [IsKilling K L] [LieModule.IsTriangularizable K (↥H) L] (q : Submodule K (Module.Dual K ↥H)) (hq : ∀ (i : ↥LieSubalgebra.root), q ∈ Module.End.invtSubmodule ↑((rootSystem H).reflection i)) : ↑(invtSubmoduleToLieIdeal q hq) = ↑(⨆ (α : { α : LieModule.Weight K (↥H) L // LieModule.Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }), sl2SubmoduleOfRoot ⋯)

@[simp]

theorem LieAlgebra.IsKilling.invtSubmoduleToLieIdeal_top {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [IsKilling K L] [LieModule.IsTriangularizable K (↥H) L] : invtSubmoduleToLieIdeal ⊤ ⋯ = ⊤

@[simp]

theorem LieAlgebra.IsKilling.invtSubmoduleToLieIdeal_apply_eq_top_iff {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [IsKilling K L] [LieModule.IsTriangularizable K (↥H) L] (q : Submodule K (Module.Dual K ↥H)) (hq : ∀ (i : ↥LieSubalgebra.root), q ∈ Module.End.invtSubmodule ↑((rootSystem H).reflection i)) : invtSubmoduleToLieIdeal q hq = ⊤ ↔ q = ⊤

@[simp]

theorem LieAlgebra.IsKilling.invtSubmoduleToLieIdeal_apply_eq_bot_iff {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [IsKilling K L] [LieModule.IsTriangularizable K (↥H) L] (q : Submodule K (Module.Dual K ↥H)) (hq : ∀ (i : ↥LieSubalgebra.root), q ∈ Module.End.invtSubmodule ↑((rootSystem H).reflection i)) : invtSubmoduleToLieIdeal q hq = ⊥ ↔ q = ⊥

instance LieAlgebra.IsKilling.instIsIrreducibleSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystemOfIsSimple {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [IsKilling K L] [LieModule.IsTriangularizable K (↥H) L] [IsSimple K L] : (rootSystem H).IsIrreducible