The nilradicals and the Borel subalgebra of a positive system #
Let L be a finite-dimensional Lie algebra with non-degenerate Killing form over a field of
characteristic zero, and let H be a splitting Cartan subalgebra, so that
LieAlgebra.IsKilling.rootSystem H is the root system of L relative to H. A base b of that
root system singles out the positive roots, and this file builds the three subalgebras the base
determines: the positive nilradical n⁺ = ⨁_{α > 0} Lα, the negative nilradical
n⁻ = ⨁_{α < 0} Lα, and the Borel subalgebra 𝔟 = H + n⁺.
Everything rests on one observation, isolated as Ado.rootSpaceSubalgebra: a special closed
set S of roots spans a Lie subalgebra, because ⁅Lα, Lβ⁆ ≤ L(α + β). Being closed under sums is
what puts the bracket back in the span when α + β is a root, and containing no opposite pair is
what rules out α + β = 0, whose weight space is the Cartan subalgebra rather than a root space.
The positive roots and the negative roots are two such sets, by the additivity of the height
function.
Main definitions #
Ado.rootSpaceSpan H S: theH-submodule ofLspanned by the root spaces indexed by a setSof roots, the instance ofAdo.genWeightSpaceSpanatM = L.Ado.IsSpecialClosedRootSet H S:Sis stable under those sums of its members that are again roots, and contains no root together with its negative.Ado.rootSpaceSubalgebra H S hS: the span of a special closed set of roots, as a Lie subalgebra.Ado.positiveNilradical H b,Ado.negativeNilradical H b: the nilradicalsn⁺andn⁻of the positive system determined by a baseb.Ado.borelSubalgebra H b: the Borel subalgebra𝔟 = H + n⁺.
Main results #
Ado.rootSpaceSpan_le_iffandAdo.rootSpaceSubalgebra_le_iffare the universal property of the span: it is contained in a given submodule, resp. Lie subalgebra, exactly when each of the root spaces it is spanned by is.Ado.positiveNilradical_le_iffandAdo.negativeNilradical_le_iffare its two specialisations to the nilradicals.Ado.mem_positiveNilradical_of_mem_rootSpaceandAdo.mem_negativeNilradical_of_mem_rootSpacesay the nilradicals contain the root spaces they are built from.Ado.neg_mem_posRoots_of_mem_negRootsandAdo.neg_mem_negRoots_of_mem_posRootssay that negation exchanges negative and positive roots.Ado.borelSubalgebra_eq_sup: the Borel subalgebra is the joinH ⊔ n⁺.Ado.le_borelSubalgebraandAdo.positiveNilradical_le_borelSubalgebraare the two inclusionsH ≤ 𝔟andn⁺ ≤ 𝔟.Ado.lie_mem_positiveNilradical_of_mem_borelSubalgebra:⁅𝔟, n⁺⁆ ≤ n⁺, son⁺is a Lie ideal of𝔟.Ado.negativeNilradical_sup_borelSubalgebra_eq_top: the triangular decompositionL = n⁻ + (H + n⁺), as an equality of submodules.Ado.exists_mem_negativeNilradical_add_mem_borelSubalgebra: the corresponding elementwise decomposition.
Implementation notes #
The nilradicals are built through Ado.rootSpaceSpan, which is valued in LieSubmodule K H L
rather than in Submodule K L: the root spaces are H-submodules by construction, so this records
for free that ⁅H, n⁺⁆ ≤ n⁺, which is exactly what makes H + n⁺ a subalgebra. Only the carrier
of a Lie subalgebra is a plain submodule, so the passage to Submodule K L happens at the last
moment, in Ado.rootSpaceSubalgebra and Ado.borelSubalgebra.
The root space product ⁅Lα, Lβ⁆ ≤ L(α + β) enters the file only through
Ado.lie_mem_rootSpaceSpan; everything else about the bracket is derived from that lemma.
The two nilradicals are not obtained from one another by a symmetry of the base, Mathlib's
RootPairing.Base having no negation; instead both are instances of Ado.rootSpaceSubalgebra,
the negative case running the positive one through root negation, in the form of the self
reflection P.reflectionPerm i i.
References #
This file supplies the "Borel and the nilradicals" item of Layer 3 of
TauCetiRoadmap/RepresentationTheory/LieHighestWeight/README.md, whose target signatures
positiveNilradical, negativeNilradical and borelSubalgebra are pinned in the accompanying
Suggested.lean. They are the subalgebras the Verma module U(L) ⊗_{U(𝔟)} Kλ of that layer is
induced from.
- J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, GTM 9, §10.1.
Spans of root spaces #
The H-submodule of L spanned by the root spaces indexed by a set S of roots: the weight
spaces of L itself at the weights the members of S name.
Equations
- Ado.rootSpaceSpan H S = Ado.genWeightSpaceSpan (↥H) L ((fun (α : ↥LieSubalgebra.root) => ⇑(LieModule.Weight.toLinear K (↥H) L ↑α)) '' S)
Instances For
A root space indexed by a member of S lies in the span of S.
The span of the root spaces indexed by S, written as the supremum of those root spaces.
Spans of root spaces are monotone in the indexing set.
The span of the root spaces indexed by S is contained in an H-submodule exactly when each
of the root spaces it is spanned by is.
The span of the root spaces indexed by S is closed under the bracket as soon as the root
space of the sum of any two members of S lies back inside it.
Special closed sets of roots #
A set S of roots is special closed when it is closed, that is stable under those sums
of its members that are again roots, and moreover contains no root together with its negative.
The second condition is what the first one alone does not give: without it the sum α + (-α) = 0
would contribute the zero weight space, which is the Cartan subalgebra and not a root space, and
the span of S would not be closed under the bracket.
- add_mem (α : ↥LieSubalgebra.root) : α ∈ S → ∀ β ∈ S, ∀ (k : ↥LieSubalgebra.root), (LieAlgebra.IsKilling.rootSystem H).root k = (LieAlgebra.IsKilling.rootSystem H).root α + (LieAlgebra.IsKilling.rootSystem H).root β → k ∈ S
- reflectionPerm_self_notMem (α : ↥LieSubalgebra.root) : α ∈ S → ((LieAlgebra.IsKilling.rootSystem H).reflectionPerm α) α ∉ S
Instances For
The root space of the sum of two members of a special closed set of roots lies in the span of that set.
Negating a negative root gives a positive root.
Negating a positive root gives a negative root.
The positive roots are a special closed set of roots: heights add, and a positive root never has a positive negative.
The negative roots are a special closed set of roots.
The span of the root spaces indexed by a special closed set S of roots, as a Lie subalgebra
of L.
Equations
- Ado.rootSpaceSubalgebra H S hS = { toSubmodule := ↑(Ado.rootSpaceSpan H S), lie_mem' := ⋯ }
Instances For
The carrier of the Lie subalgebra spanned by a special closed set S of roots is the span of
the root spaces indexed by S; the bracket-closure the definition supplies costs the carrier
nothing.
The Lie subalgebra spanned by a special closed set S of roots is contained in a Lie
subalgebra K' exactly when each of the root spaces indexed by S is.
The nilradicals and the Borel subalgebra #
The positive nilradical n⁺ = ⨁_{α > 0} Lα of the positive system determined by b.
Equations
Instances For
The negative nilradical n⁻ = ⨁_{α < 0} Lα of the positive system determined by b.
Equations
Instances For
The positive nilradical contains the root space of every positive root.
The negative nilradical contains the root space of every negative root.
The positive nilradical is contained in a Lie subalgebra K' exactly when the root space of
every positive root is.
The negative nilradical is contained in a Lie subalgebra K' exactly when the root space of
every negative root is.
The Borel subalgebra 𝔟 = H + n⁺ of the positive system determined by b.
It is a subalgebra because H is one, because ⁅H, n⁺⁆ ≤ n⁺ — the root spaces being
H-submodules — and because n⁺ is one.
Equations
- Ado.borelSubalgebra H b = { toSubmodule := H.toSubmodule ⊔ (Ado.positiveNilradical H b).toSubmodule, lie_mem' := ⋯ }
Instances For
The carrier of the Borel subalgebra is the submodule sum H + n⁺; no closure is needed. This
is the concrete description the construction supplies, Ado.mem_borelSubalgebra being the
canonical membership criterion.
The Cartan subalgebra is contained in the Borel subalgebra.
The positive nilradical is contained in the Borel subalgebra.
The Borel subalgebra is the join H ⊔ n⁺ of the Cartan subalgebra and the positive nilradical
in the lattice of Lie subalgebras: no closure is needed, the submodule sum H + n⁺ being already
a Lie subalgebra.
The positive nilradical is a Lie ideal of the Borel subalgebra: ⁅𝔟, n⁺⁆ ≤ n⁺.
The triangular decomposition #
The triangular decomposition L = n⁻ + (H + n⁺): the negative nilradical and the Borel
subalgebra together span L. This is the spanning half of L = n⁻ ⊕ H ⊕ n⁺, and it is exactly
what the root space decomposition of L supplies.
The triangular decomposition, as a splitting of an element of L: every x : L is the sum
of an element of the negative nilradical and an element of the Borel subalgebra.