Weight spaces of Lie modules of nilpotent Lie algebras #
Just as a key tool when studying the behaviour of a linear operator is to decompose the space on
which it acts into a sum of (generalised) eigenspaces, a key tool when studying a representation M
of Lie algebra L
is to decompose M
into a sum of simultaneous eigenspaces of x
as x
ranges
over L
. These simultaneous generalised eigenspaces are known as the weight spaces of M
.
When L
is nilpotent, it follows from the binomial theorem that weight spaces are Lie submodules.
Basic definitions and properties of the above ideas are provided in this file.
Main definitions #
LieModule.genWeightSpaceOf
LieModule.genWeightSpace
LieModule.Weight
LieModule.posFittingCompOf
LieModule.posFittingComp
LieModule.iSup_ucs_eq_genWeightSpace_zero
LieModule.iInf_lowerCentralSeries_eq_posFittingComp
LieModule.isCompl_genWeightSpace_zero_posFittingComp
LieModule.independent_genWeightSpace
LieModule.iSup_genWeightSpace_eq_top
References #
Tags #
lie character, eigenvalue, eigenspace, weight, weight vector, root, root vector
See also bourbaki1975b
Chapter VII §1.1, Proposition 2 (ii).
If M
is a representation of a nilpotent Lie algebra L
, χ
is a scalar, and x : L
, then
genWeightSpaceOf M χ x
is the maximal generalized χ
-eigenspace of the action of x
on M
.
It is a Lie submodule because L
is nilpotent.
Equations
- LieModule.genWeightSpaceOf M χ x = { toSubmodule := ((LieModule.toEnd R L M) x).maxGenEigenspace χ, lie_mem := ⋯ }
Instances For
If M
is a representation of a nilpotent Lie algebra L
and χ : L → R
is a family of scalars,
then genWeightSpace M χ
is the intersection of the maximal generalized χ x
-eigenspaces
of the action of x
on M
as x
ranges over L
.
It is a Lie submodule because L
is nilpotent.
Equations
- LieModule.genWeightSpace M χ = ⨅ (x : L), LieModule.genWeightSpaceOf M (χ x) x
Instances For
A weight of a Lie module is a map L → R
such that the corresponding weight space is
non-trivial.
- toFun : L → R
The family of eigenvalues corresponding to a weight.
- genWeightSpace_ne_bot' : LieModule.genWeightSpace M self.toFun ≠ ⊥
Instances For
Equations
- LieModule.Weight.instFunLike M = { coe := fun (χ : LieModule.Weight R L M) => χ.toFun, coe_injective' := ⋯ }
Equations
- ⋯ = ⋯
Equations
- LieModule.Weight.instZeroOfNontrivialSubtypeMemLieSubmoduleGenWeightSpaceOfNatForall = { zero := { toFun := 0, genWeightSpace_ne_bot' := ⋯ } }
The proposition that a weight of a Lie module is zero.
We make this definition because we cannot define a Zero (Weight R L M)
instance since the weight
space of the zero function can be trivial.
Instances For
The proposition that a weight of a Lie module is non-zero.
Instances For
Equations
- LieModule.Weight.instDecidablePredIsNonZero = Classical.decPred LieModule.Weight.IsNonZero
The set of weights is equivalent to a subtype.
Equations
- One or more equations did not get rendered due to their size.
Instances For
See also the more useful form LieModule.zero_genWeightSpace_eq_top_of_nilpotent
.
A (nilpotent) Lie algebra acts nilpotently on the zero weight space of a Noetherian Lie module.
By Engel's theorem, the zero weight space of a Noetherian Lie module is nilpotent.
Equations
- ⋯ = ⋯
See also LieModule.iInf_lowerCentralSeries_eq_posFittingComp
.
If M
is a representation of a nilpotent Lie algebra L
, and x : L
, then
posFittingCompOf R M x
is the infimum of the decreasing system
range φₓ ⊇ range φₓ² ⊇ range φₓ³ ⊇ ⋯
where φₓ : End R M := toEnd R L M x
. We call this
the "positive Fitting component" because with appropriate assumptions (e.g., R
is a field and
M
is finite-dimensional) φₓ
induces the so-called Fitting decomposition: M = M₀ ⊕ M₁
where
M₀ = genWeightSpaceOf M 0 x
and M₁ = posFittingCompOf R M x
.
It is a Lie submodule because L
is nilpotent.
Equations
- LieModule.posFittingCompOf R M x = { toSubmodule := ⨅ (k : ℕ), LinearMap.range ((LieModule.toEnd R L M) x ^ k), lie_mem := ⋯ }
Instances For
If M
is a representation of a nilpotent Lie algebra L
with coefficients in R
, then
posFittingComp R L M
is the span of the positive Fitting components of the action of x
on M
,
as x
ranges over L
.
It is a Lie submodule because L
is nilpotent.
Equations
- LieModule.posFittingComp R L M = ⨆ (x : L), LieModule.posFittingCompOf R M x
Instances For
This is the Fitting decomposition of the Lie module M
.
Lie module weight spaces are independent.
See also LieModule.independent_genWeightSpace'
.
Equations
- ⋯ = ⋯
Equations
- LieModule.Weight.instFintype R L M = Fintype.ofFinite (LieModule.Weight R L M)
A Lie module M
of a Lie algebra L
is triangularizable if the endomorhpism of M
defined by
any x : L
is triangularizable.
- iSup_eq_top : ∀ (x : L), ⨆ (φ : R), ⨆ (k : ℕ), (((LieModule.toEnd R L M) x).genEigenspace φ) k = ⊤
Instances
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
For a triangularizable Lie module in finite dimensions, the weight spaces span the entire space.
See also LieModule.iSup_genWeightSpace_eq_top'
.