Simple Lie algebras #
We show the irreducibility of root systems of simple Lie algebras.
Main definitions #
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
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 : { x : LieModule.Weight K (↥H) L // x ∈ 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.
Instances For
theorem
LieAlgebra.IsKilling.eq_top_of_invtSubmodule_ne_bot
{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]
(q : Submodule K (Module.Dual K ↥H))
(h₀ :
∀ (i : { x : LieModule.Weight K (↥H) L // x ∈ LieSubalgebra.root }),
q ∈ Module.End.invtSubmodule ↑((rootSystem H).reflection i))
(h₁ : q ≠ ⊥)
:
instance
LieAlgebra.IsKilling.instIsIrreducibleSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystem
{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]
: