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.
Main definitions #
LieIdeal.rootSet: the set of roots whose root space is contained in a given Lie ideal.LieIdeal.rootSpan: the submodule ofDual K Hspanned byLieIdeal.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.LieAlgebra.IsKilling.lieIdealOrderIso: the order isomorphism between Lie ideals and invariant root submodules.
Main results #
LieAlgebra.IsKilling.restr_inf_cartan_eq_iSup_corootSubmodule: the intersection of a Lie ideal and a Cartan subalgebra is the span of the coroots whose roots have root spaces in the ideal.LieAlgebra.IsKilling.isSimple_iff_isIrreducible: a Killing Lie algebra is simple if and only if its root system 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)
:
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)
:
The set of roots whose root space is contained in a given Lie ideal.
Instances For
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.
Instances For
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)
:
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)
:
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)
:
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.
Instances For
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)
:
theorem
LieIdeal.root_apply_eq_zero_of_notMem_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]
[CharZero K]
[LieAlgebra.IsKilling K L]
[LieModule.IsTriangularizable K (↥H) L]
(I : LieIdeal K L)
{h : ↥H}
(hI : ↑h ∈ I)
{β : ↥LieSubalgebra.root}
(hβ : β ∉ I.rootSet)
:
↑β h = 0
theorem
LieIdeal.rootSet_apply_coroot_eq_zero_of_notMem_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]
[CharZero K]
[LieAlgebra.IsKilling K L]
[LieModule.IsTriangularizable K (↥H) L]
(I : LieIdeal K L)
{α : ↥LieSubalgebra.root}
(hα : α ∈ I.rootSet)
{β : ↥LieSubalgebra.root}
(hβ : β ∉ I.rootSet)
:
↑α (LieAlgebra.IsKilling.coroot ↑β) = 0
theorem
LieIdeal.restr_inf_cartan_eq_biSup_corootSubmodule
{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)
:
LieSubmodule.restr I H ⊓ H.toLieSubmodule = ⨆ α ∈ I.rootSet, LieAlgebra.IsKilling.corootSubmodule ↑α
The intersection of a Lie ideal and a Cartan subalgebra is the span of the coroots whose roots have root spaces in the ideal.
theorem
LieIdeal.mem_rootSet_of_mem_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)
{α : ↥LieSubalgebra.root}
(hα_span : LieModule.Weight.toLinear K (↥H) L ↑α ∈ I.rootSpan)
:
α ∈ I.rootSet
theorem
LieIdeal.restr_eq_iSup_sl2SubmoduleOfRoot
{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)
:
LieSubmodule.restr I H = ⨆ α ∈ I.rootSet, LieAlgebra.IsKilling.sl2SubmoduleOfRoot ⋯
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.
Instances For
@[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.restr_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))
:
LieSubmodule.restr (invtSubmoduleToLieIdeal q hq) H = ⨆ (α : { α : LieModule.Weight K (↥H) L // LieModule.Weight.toLinear K (↥H) L α ∈ q ∧ α.IsNonZero }),
sl2SubmoduleOfRoot ⋯
theorem
LieAlgebra.IsKilling.mem_rootSet_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))
{α : ↥LieSubalgebra.root}
:
α ∈ (invtSubmoduleToLieIdeal q hq).rootSet ↔ (rootSystem H).root α ∈ q
theorem
LieAlgebra.IsKilling.invtSubmoduleToLieIdeal_mono
{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₁ q₂ : Submodule K (Module.Dual K ↥H)}
(hq₁ : ∀ (i : ↥LieSubalgebra.root), q₁ ∈ Module.End.invtSubmodule ↑((rootSystem H).reflection i))
(hq₂ : ∀ (i : ↥LieSubalgebra.root), q₂ ∈ Module.End.invtSubmodule ↑((rootSystem H).reflection i))
(h : q₁ ≤ q₂)
:
theorem
LieAlgebra.IsKilling.lieIdealOrderIso_left_inv
{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]
(I : LieIdeal K L)
(hI : ∀ (α : ↥LieSubalgebra.root), I.rootSpan ∈ Module.End.invtSubmodule ↑((rootSystem H).reflection α) := ⋯)
:
invtSubmoduleToLieIdeal I.rootSpan hI = I
theorem
LieAlgebra.IsKilling.lieIdealOrderIso_right_inv
{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 : ↥(rootSystem H).invtRootSubmodule)
(hq : ∀ (α : ↥LieSubalgebra.root), ↑q ∈ Module.End.invtSubmodule ↑((rootSystem H).reflection α) := ⋯)
:
(invtSubmoduleToLieIdeal (↑q) hq).toInvtRootSubmodule = q
noncomputable def
LieAlgebra.IsKilling.lieIdealOrderIso
{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]
:
The order isomorphism between Lie ideals and invariant root submodules.
Instances For
theorem
LieAlgebra.IsKilling.isSimple_iff_isIrreducible
{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]
:
(rootSystem H).IsIrreducible ↔ IsSimple K L
A Killing Lie algebra is simple if and only if its root system is irreducible.
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]
: