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.genWeightSpaceOfLieModule.genWeightSpaceLieModule.WeightLieModule.posFittingCompOfLieModule.posFittingCompLieModule.iSup_ucs_eq_genWeightSpace_zeroLieModule.iInf_lowerCentralSeries_eq_posFittingCompLieModule.isCompl_genWeightSpace_zero_posFittingCompLieModule.independent_genWeightSpaceLieModule.iSup_genWeightSpace_eq_top
References #
Tags #
lie character, eigenvalue, eigenspace, weight, weight vector, root, root vector
def
LieModule.weightSpace
{R : Type u_2}
{L : Type u_3}
(M : Type u_4)
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
(χ : L → R)
:
LieSubmodule R L M
If M is a representation of a Lie algebra L and χ : L → R is a family of scalars,
then weightSpace M χ is the intersection of the χ x-eigenspaces
of the action of x on M as x ranges over L.
Equations
- LieModule.weightSpace M χ = { toSubmodule := ⨅ (x : L), ((LieModule.toEnd R L M) x).eigenspace (χ x), lie_mem := ⋯ }
theorem
LieModule.mem_weightSpace
{R : Type u_2}
{L : Type u_3}
{M : Type u_4}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
(χ : L → R)
(m : M)
:
theorem
LieModule.weight_vector_multiplication
{R : Type u_2}
{L : Type u_3}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
(M₁ : Type u_5)
(M₂ : Type u_6)
(M₃ : Type u_7)
[AddCommGroup M₁]
[Module R M₁]
[LieRingModule L M₁]
[LieModule R L M₁]
[AddCommGroup M₂]
[Module R M₂]
[LieRingModule L M₂]
[LieModule R L M₂]
[AddCommGroup M₃]
[Module R M₃]
[LieRingModule L M₃]
[LieModule R L M₃]
(g : TensorProduct R M₁ M₂ →ₗ⁅R,L⁆ M₃)
(χ₁ χ₂ : R)
(x : L)
:
LinearMap.range
(↑g ∘ₗ
TensorProduct.mapIncl (((LieModule.toEnd R L M₁) x).maxGenEigenspace χ₁)
(((LieModule.toEnd R L M₂) x).maxGenEigenspace χ₂)) ≤ ((LieModule.toEnd R L M₃) x).maxGenEigenspace (χ₁ + χ₂)
See also bourbaki1975b Chapter VII §1.1, Proposition 2 (ii).
theorem
LieModule.lie_mem_maxGenEigenspace_toEnd
{R : Type u_2}
{L : Type u_3}
{M : Type u_4}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
{χ₁ χ₂ : R}
{x y : L}
{m : M}
(hy : y ∈ ((LieModule.toEnd R L L) x).maxGenEigenspace χ₁)
(hm : m ∈ ((LieModule.toEnd R L M) x).maxGenEigenspace χ₂)
:
def
LieModule.genWeightSpaceOf
{R : Type u_2}
{L : Type u_3}
(M : Type u_4)
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[LieAlgebra.IsNilpotent R L]
(χ : R)
(x : L)
:
LieSubmodule R L M
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 := ⋯ }
theorem
LieModule.mem_genWeightSpaceOf
{R : Type u_2}
{L : Type u_3}
(M : Type u_4)
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[LieAlgebra.IsNilpotent R L]
(χ : R)
(x : L)
(m : M)
:
m ∈ LieModule.genWeightSpaceOf M χ x ↔ ∃ (k : ℕ), (((LieModule.toEnd R L M) x - χ • 1) ^ k) m = 0
theorem
LieModule.coe_genWeightSpaceOf_zero
{R : Type u_2}
{L : Type u_3}
(M : Type u_4)
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[LieAlgebra.IsNilpotent R L]
(x : L)
:
↑(LieModule.genWeightSpaceOf M 0 x) = ⨆ (k : ℕ), LinearMap.ker ((LieModule.toEnd R L M) x ^ k)
def
LieModule.genWeightSpace
{R : Type u_2}
{L : Type u_3}
(M : Type u_4)
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[LieAlgebra.IsNilpotent R L]
(χ : L → R)
:
LieSubmodule R L M
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
theorem
LieModule.mem_genWeightSpace
{R : Type u_2}
{L : Type u_3}
(M : Type u_4)
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[LieAlgebra.IsNilpotent R L]
(χ : L → R)
(m : M)
:
m ∈ LieModule.genWeightSpace M χ ↔ ∀ (x : L), ∃ (k : ℕ), (((LieModule.toEnd R L M) x - χ x • 1) ^ k) m = 0
theorem
LieModule.genWeightSpace_le_genWeightSpaceOf
{R : Type u_2}
{L : Type u_3}
(M : Type u_4)
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[LieAlgebra.IsNilpotent R L]
(x : L)
(χ : L → R)
:
LieModule.genWeightSpace M χ ≤ LieModule.genWeightSpaceOf M (χ x) x
theorem
LieModule.weightSpace_le_genWeightSpace
{R : Type u_2}
{L : Type u_3}
(M : Type u_4)
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[LieAlgebra.IsNilpotent R L]
(χ : L → R)
:
structure
LieModule.Weight
(R : Type u_2)
(L : Type u_3)
(M : Type u_4)
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[LieAlgebra.IsNilpotent R L]
:
Type (max u_2 u_3)
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 ≠ ⊥
instance
LieModule.Weight.instFunLike
{R : Type u_2}
{L : Type u_3}
(M : Type u_4)
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[LieAlgebra.IsNilpotent R L]
:
FunLike (LieModule.Weight R L M) L R
Equations
- LieModule.Weight.instFunLike M = { coe := fun (χ : LieModule.Weight R L M) => χ.toFun, coe_injective' := ⋯ }
@[simp]
theorem
LieModule.Weight.coe_weight_mk
{R : Type u_2}
{L : Type u_3}
(M : Type u_4)
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[LieAlgebra.IsNilpotent R L]
(χ : L → R)
(h : LieModule.genWeightSpace M χ ≠ ⊥)
:
⇑{ toFun := χ, genWeightSpace_ne_bot' := h } = χ
theorem
LieModule.Weight.genWeightSpace_ne_bot
{R : Type u_2}
{L : Type u_3}
(M : Type u_4)
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[LieAlgebra.IsNilpotent R L]
(χ : LieModule.Weight R L M)
:
LieModule.genWeightSpace M ⇑χ ≠ ⊥
theorem
LieModule.Weight.ext
{R : Type u_2}
{L : Type u_3}
{M : Type u_4}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[LieAlgebra.IsNilpotent R L]
{χ₁ χ₂ : LieModule.Weight R L M}
(h : ∀ (x : L), χ₁ x = χ₂ x)
:
χ₁ = χ₂
theorem
LieModule.Weight.ext_iff'
{R : Type u_2}
{L : Type u_3}
{M : Type u_4}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[LieAlgebra.IsNilpotent R L]
{χ₁ χ₂ : LieModule.Weight R L M}
:
theorem
LieModule.Weight.exists_ne_zero
{R : Type u_2}
{L : Type u_3}
{M : Type u_4}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[LieAlgebra.IsNilpotent R L]
(χ : LieModule.Weight R L M)
:
∃ x ∈ LieModule.genWeightSpace M ⇑χ, x ≠ 0
instance
LieModule.Weight.instIsEmptyOfSubsingleton
{R : Type u_2}
{L : Type u_3}
{M : Type u_4}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[LieAlgebra.IsNilpotent R L]
[Subsingleton M]
:
IsEmpty (LieModule.Weight R L M)
Equations
- ⋯ = ⋯
instance
LieModule.Weight.instZeroOfNontrivialSubtypeMemLieSubmoduleGenWeightSpaceOfNatForall
{R : Type u_2}
{L : Type u_3}
{M : Type u_4}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[LieAlgebra.IsNilpotent R L]
[Nontrivial ↥(LieModule.genWeightSpace M 0)]
:
Zero (LieModule.Weight R L M)
Equations
- LieModule.Weight.instZeroOfNontrivialSubtypeMemLieSubmoduleGenWeightSpaceOfNatForall = { zero := { toFun := 0, genWeightSpace_ne_bot' := ⋯ } }
@[simp]
theorem
LieModule.Weight.coe_zero
{R : Type u_2}
{L : Type u_3}
{M : Type u_4}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[LieAlgebra.IsNilpotent R L]
[Nontrivial ↥(LieModule.genWeightSpace M 0)]
:
⇑0 = 0
theorem
LieModule.Weight.zero_apply
{R : Type u_2}
{L : Type u_3}
{M : Type u_4}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[LieAlgebra.IsNilpotent R L]
[Nontrivial ↥(LieModule.genWeightSpace M 0)]
(x : L)
:
0 x = 0
def
LieModule.Weight.IsZero
{R : Type u_2}
{L : Type u_3}
{M : Type u_4}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[LieAlgebra.IsNilpotent R L]
(χ : LieModule.Weight R L M)
:
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.
@[simp]
theorem
LieModule.Weight.IsZero.eq
{R : Type u_2}
{L : Type u_3}
{M : Type u_4}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[LieAlgebra.IsNilpotent R L]
{χ : LieModule.Weight R L M}
(hχ : χ.IsZero)
:
⇑χ = 0
@[simp]
theorem
LieModule.Weight.coe_eq_zero_iff
{R : Type u_2}
{L : Type u_3}
{M : Type u_4}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[LieAlgebra.IsNilpotent R L]
(χ : LieModule.Weight R L M)
:
theorem
LieModule.Weight.isZero_iff_eq_zero
{R : Type u_2}
{L : Type u_3}
{M : Type u_4}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[LieAlgebra.IsNilpotent R L]
[Nontrivial ↥(LieModule.genWeightSpace M 0)]
{χ : LieModule.Weight R L M}
:
theorem
LieModule.Weight.isZero_zero
{R : Type u_2}
{L : Type u_3}
{M : Type u_4}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[LieAlgebra.IsNilpotent R L]
[Nontrivial ↥(LieModule.genWeightSpace M 0)]
:
@[reducible, inline]
abbrev
LieModule.Weight.IsNonZero
{R : Type u_2}
{L : Type u_3}
{M : Type u_4}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[LieAlgebra.IsNilpotent R L]
(χ : LieModule.Weight R L M)
:
The proposition that a weight of a Lie module is non-zero.
theorem
LieModule.Weight.isNonZero_iff_ne_zero
{R : Type u_2}
{L : Type u_3}
{M : Type u_4}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[LieAlgebra.IsNilpotent R L]
[Nontrivial ↥(LieModule.genWeightSpace M 0)]
{χ : LieModule.Weight R L M}
:
noncomputable instance
LieModule.Weight.instDecidablePredIsNonZero
{R : Type u_2}
{L : Type u_3}
{M : Type u_4}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[LieAlgebra.IsNilpotent R L]
:
DecidablePred LieModule.Weight.IsNonZero
Equations
- LieModule.Weight.instDecidablePredIsNonZero = Classical.decPred LieModule.Weight.IsNonZero
def
LieModule.Weight.equivSetOf
(R : Type u_2)
(L : Type u_3)
(M : Type u_4)
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[LieAlgebra.IsNilpotent R L]
:
LieModule.Weight R L M ≃ ↑{χ : L → R | LieModule.genWeightSpace M χ ≠ ⊥}
The set of weights is equivalent to a subtype.
Equations
- One or more equations did not get rendered due to their size.
theorem
LieModule.Weight.genWeightSpaceOf_ne_bot
{R : Type u_2}
{L : Type u_3}
{M : Type u_4}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[LieAlgebra.IsNilpotent R L]
(χ : LieModule.Weight R L M)
(x : L)
:
LieModule.genWeightSpaceOf M (χ x) x ≠ ⊥
theorem
LieModule.Weight.hasEigenvalueAt
{R : Type u_2}
{L : Type u_3}
{M : Type u_4}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[LieAlgebra.IsNilpotent R L]
(χ : LieModule.Weight R L M)
(x : L)
:
((LieModule.toEnd R L M) x).HasEigenvalue (χ x)
theorem
LieModule.Weight.apply_eq_zero_of_isNilpotent
{R : Type u_2}
{L : Type u_3}
{M : Type u_4}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[LieAlgebra.IsNilpotent R L]
[NoZeroSMulDivisors R M]
[IsReduced R]
(x : L)
(h : IsNilpotent ((LieModule.toEnd R L M) x))
(χ : LieModule.Weight R L M)
:
χ x = 0
@[simp]
theorem
LieModule.zero_genWeightSpace_eq_top_of_nilpotent'
{R : Type u_2}
{L : Type u_3}
(M : Type u_4)
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[LieAlgebra.IsNilpotent R L]
[LieModule.IsNilpotent R L M]
:
See also the more useful form LieModule.zero_genWeightSpace_eq_top_of_nilpotent.
theorem
LieModule.coe_genWeightSpace_of_top
{R : Type u_2}
{L : Type u_3}
(M : Type u_4)
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[LieAlgebra.IsNilpotent R L]
(χ : L → R)
:
↑(LieModule.genWeightSpace M (χ ∘ ⇑⊤.incl)) = ↑(LieModule.genWeightSpace M χ)
@[simp]
theorem
LieModule.zero_genWeightSpace_eq_top_of_nilpotent
{R : Type u_2}
{L : Type u_3}
(M : Type u_4)
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[LieAlgebra.IsNilpotent R L]
[LieModule.IsNilpotent R L M]
:
theorem
LieModule.exists_genWeightSpace_le_ker_of_isNoetherian
{R : Type u_2}
{L : Type u_3}
(M : Type u_4)
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[LieAlgebra.IsNilpotent R L]
[IsNoetherian R M]
(χ : L → R)
(x : L)
:
∃ (k : ℕ),
↑(LieModule.genWeightSpace M χ) ≤ LinearMap.ker (((LieModule.toEnd R L M) x - (algebraMap R (Module.End R M)) (χ x)) ^ k)
theorem
LieModule.exists_genWeightSpace_zero_le_ker_of_isNoetherian
(R : Type u_2)
{L : Type u_3}
(M : Type u_4)
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[LieAlgebra.IsNilpotent R L]
[IsNoetherian R M]
(x : L)
:
∃ (k : ℕ), ↑(LieModule.genWeightSpace M 0) ≤ LinearMap.ker ((LieModule.toEnd R L M) x ^ k)
theorem
LieModule.isNilpotent_toEnd_sub_algebraMap
{R : Type u_2}
{L : Type u_3}
(M : Type u_4)
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[LieAlgebra.IsNilpotent R L]
[IsNoetherian R M]
(χ : L → R)
(x : L)
:
IsNilpotent
((LieModule.toEnd R L ↥(LieModule.genWeightSpace M χ)) x - (algebraMap R (Module.End R ↥(LieModule.genWeightSpace M χ))) (χ x))
theorem
LieModule.isNilpotent_toEnd_genWeightSpace_zero
{R : Type u_2}
{L : Type u_3}
(M : Type u_4)
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[LieAlgebra.IsNilpotent R L]
[IsNoetherian R M]
(x : L)
:
IsNilpotent ((LieModule.toEnd R L ↥(LieModule.genWeightSpace M 0)) x)
A (nilpotent) Lie algebra acts nilpotently on the zero weight space of a Noetherian Lie module.
instance
LieModule.instIsNilpotentSubtypeMemLieSubmoduleGenWeightSpaceOfNatForallOfIsNoetherian
{R : Type u_2}
{L : Type u_3}
(M : Type u_4)
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[LieAlgebra.IsNilpotent R L]
[IsNoetherian R M]
:
LieModule.IsNilpotent R L ↥(LieModule.genWeightSpace M 0)
By Engel's theorem, the zero weight space of a Noetherian Lie module is nilpotent.
Equations
- ⋯ = ⋯
@[simp]
theorem
LieModule.genWeightSpace_zero_normalizer_eq_self
(R : Type u_2)
(L : Type u_3)
(M : Type u_4)
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[LieAlgebra.IsNilpotent R L]
:
(LieModule.genWeightSpace M 0).normalizer = LieModule.genWeightSpace M 0
theorem
LieModule.iSup_ucs_le_genWeightSpace_zero
(R : Type u_2)
(L : Type u_3)
(M : Type u_4)
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[LieAlgebra.IsNilpotent R L]
:
⨆ (k : ℕ), LieSubmodule.ucs k ⊥ ≤ LieModule.genWeightSpace M 0
theorem
LieModule.iSup_ucs_eq_genWeightSpace_zero
(R : Type u_2)
(L : Type u_3)
(M : Type u_4)
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[LieAlgebra.IsNilpotent R L]
[IsNoetherian R M]
:
⨆ (k : ℕ), LieSubmodule.ucs k ⊥ = LieModule.genWeightSpace M 0
See also LieModule.iInf_lowerCentralSeries_eq_posFittingComp.
def
LieModule.posFittingCompOf
(R : Type u_2)
{L : Type u_3}
(M : Type u_4)
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[LieAlgebra.IsNilpotent R L]
(x : L)
:
LieSubmodule R L M
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 := ⋯ }
theorem
LieModule.mem_posFittingCompOf
(R : Type u_2)
{L : Type u_3}
{M : Type u_4}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[LieAlgebra.IsNilpotent R L]
(x : L)
(m : M)
:
m ∈ LieModule.posFittingCompOf R M x ↔ ∀ (k : ℕ), ∃ (n : M), ((LieModule.toEnd R L M) x ^ k) n = m
@[simp]
theorem
LieModule.posFittingCompOf_le_lowerCentralSeries
(R : Type u_2)
{L : Type u_3}
(M : Type u_4)
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[LieAlgebra.IsNilpotent R L]
(x : L)
(k : ℕ)
:
LieModule.posFittingCompOf R M x ≤ LieModule.lowerCentralSeries R L M k
@[simp]
theorem
LieModule.posFittingCompOf_eq_bot_of_isNilpotent
(R : Type u_2)
{L : Type u_3}
(M : Type u_4)
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[LieAlgebra.IsNilpotent R L]
[LieModule.IsNilpotent R L M]
(x : L)
:
LieModule.posFittingCompOf R M x = ⊥
def
LieModule.posFittingComp
(R : Type u_2)
(L : Type u_3)
(M : Type u_4)
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[LieAlgebra.IsNilpotent R L]
:
LieSubmodule R L M
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
theorem
LieModule.mem_posFittingComp
(R : Type u_2)
(L : Type u_3)
(M : Type u_4)
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[LieAlgebra.IsNilpotent R L]
(m : M)
:
m ∈ LieModule.posFittingComp R L M ↔ m ∈ ⨆ (x : L), LieModule.posFittingCompOf R M x
theorem
LieModule.posFittingCompOf_le_posFittingComp
(R : Type u_2)
(L : Type u_3)
(M : Type u_4)
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[LieAlgebra.IsNilpotent R L]
(x : L)
:
LieModule.posFittingCompOf R M x ≤ LieModule.posFittingComp R L M
theorem
LieModule.posFittingComp_le_iInf_lowerCentralSeries
(R : Type u_2)
(L : Type u_3)
(M : Type u_4)
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[LieAlgebra.IsNilpotent R L]
:
LieModule.posFittingComp R L M ≤ ⨅ (k : ℕ), LieModule.lowerCentralSeries R L M k
@[simp]
theorem
LieModule.iInf_lowerCentralSeries_eq_posFittingComp
(R : Type u_2)
(L : Type u_3)
(M : Type u_4)
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[LieAlgebra.IsNilpotent R L]
[IsNoetherian R M]
[IsArtinian R M]
:
⨅ (k : ℕ), LieModule.lowerCentralSeries R L M k = LieModule.posFittingComp R L M
@[simp]
theorem
LieModule.posFittingComp_eq_bot_of_isNilpotent
(R : Type u_2)
(L : Type u_3)
(M : Type u_4)
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[LieAlgebra.IsNilpotent R L]
[LieModule.IsNilpotent R L M]
:
LieModule.posFittingComp R L M = ⊥
theorem
LieModule.map_posFittingComp_le
{R : Type u_2}
{L : Type u_3}
{M : Type u_4}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[LieAlgebra.IsNilpotent R L]
{M₂ : Type u_5}
[AddCommGroup M₂]
[Module R M₂]
[LieRingModule L M₂]
[LieModule R L M₂]
(f : M →ₗ⁅R,L⁆ M₂)
:
LieSubmodule.map f (LieModule.posFittingComp R L M) ≤ LieModule.posFittingComp R L M₂
theorem
LieModule.map_genWeightSpace_le
{R : Type u_2}
{L : Type u_3}
{M : Type u_4}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[LieAlgebra.IsNilpotent R L]
{M₂ : Type u_5}
[AddCommGroup M₂]
[Module R M₂]
[LieRingModule L M₂]
[LieModule R L M₂]
{χ : L → R}
(f : M →ₗ⁅R,L⁆ M₂)
:
theorem
LieModule.comap_genWeightSpace_eq_of_injective
{R : Type u_2}
{L : Type u_3}
{M : Type u_4}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[LieAlgebra.IsNilpotent R L]
{M₂ : Type u_5}
[AddCommGroup M₂]
[Module R M₂]
[LieRingModule L M₂]
[LieModule R L M₂]
{χ : L → R}
{f : M →ₗ⁅R,L⁆ M₂}
(hf : Function.Injective ⇑f)
:
theorem
LieModule.map_genWeightSpace_eq_of_injective
{R : Type u_2}
{L : Type u_3}
{M : Type u_4}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[LieAlgebra.IsNilpotent R L]
{M₂ : Type u_5}
[AddCommGroup M₂]
[Module R M₂]
[LieRingModule L M₂]
[LieModule R L M₂]
{χ : L → R}
{f : M →ₗ⁅R,L⁆ M₂}
(hf : Function.Injective ⇑f)
:
LieSubmodule.map f (LieModule.genWeightSpace M χ) = LieModule.genWeightSpace M₂ χ ⊓ f.range
theorem
LieModule.map_genWeightSpace_eq
{R : Type u_2}
{L : Type u_3}
{M : Type u_4}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[LieAlgebra.IsNilpotent R L]
{M₂ : Type u_5}
[AddCommGroup M₂]
[Module R M₂]
[LieRingModule L M₂]
[LieModule R L M₂]
{χ : L → R}
(e : M ≃ₗ⁅R,L⁆ M₂)
:
LieSubmodule.map e.toLieModuleHom (LieModule.genWeightSpace M χ) = LieModule.genWeightSpace M₂ χ
theorem
LieModule.map_posFittingComp_eq
{R : Type u_2}
{L : Type u_3}
{M : Type u_4}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[LieAlgebra.IsNilpotent R L]
{M₂ : Type u_5}
[AddCommGroup M₂]
[Module R M₂]
[LieRingModule L M₂]
[LieModule R L M₂]
(e : M ≃ₗ⁅R,L⁆ M₂)
:
LieSubmodule.map e.toLieModuleHom (LieModule.posFittingComp R L M) = LieModule.posFittingComp R L M₂
theorem
LieModule.posFittingComp_map_incl_sup_of_codisjoint
{R : Type u_2}
{L : Type u_3}
{M : Type u_4}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[LieAlgebra.IsNilpotent R L]
[IsNoetherian R M]
[IsArtinian R M]
{N₁ N₂ : LieSubmodule R L M}
(h : Codisjoint N₁ N₂)
:
LieSubmodule.map N₁.incl (LieModule.posFittingComp R L ↥N₁) ⊔ LieSubmodule.map N₂.incl (LieModule.posFittingComp R L ↥N₂) = LieModule.posFittingComp R L M
theorem
LieModule.genWeightSpace_genWeightSpaceOf_map_incl
{R : Type u_2}
{L : Type u_3}
{M : Type u_4}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[LieAlgebra.IsNilpotent R L]
(x : L)
(χ : L → R)
:
LieSubmodule.map (LieModule.genWeightSpaceOf M (χ x) x).incl
(LieModule.genWeightSpace (↥(LieModule.genWeightSpaceOf M (χ x) x)) χ) = LieModule.genWeightSpace M χ
theorem
LieModule.isCompl_genWeightSpaceOf_zero_posFittingCompOf
(R : Type u_2)
(L : Type u_3)
(M : Type u_4)
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[LieAlgebra.IsNilpotent R L]
[IsNoetherian R M]
[IsArtinian R M]
(x : L)
:
IsCompl (LieModule.genWeightSpaceOf M 0 x) (LieModule.posFittingCompOf R M x)
theorem
LieModule.isCompl_genWeightSpace_zero_posFittingComp
(R : Type u_2)
(L : Type u_3)
(M : Type u_4)
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[LieAlgebra.IsNilpotent R L]
[IsNoetherian R M]
[IsArtinian R M]
:
IsCompl (LieModule.genWeightSpace M 0) (LieModule.posFittingComp R L M)
This is the Fitting decomposition of the Lie module M.
theorem
LieModule.disjoint_genWeightSpaceOf
(R : Type u_2)
(L : Type u_3)
(M : Type u_4)
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[LieAlgebra.IsNilpotent R L]
[NoZeroSMulDivisors R M]
{x : L}
{φ₁ φ₂ : R}
(h : φ₁ ≠ φ₂)
:
Disjoint (LieModule.genWeightSpaceOf M φ₁ x) (LieModule.genWeightSpaceOf M φ₂ x)
theorem
LieModule.disjoint_genWeightSpace
(R : Type u_2)
(L : Type u_3)
(M : Type u_4)
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[LieAlgebra.IsNilpotent R L]
[NoZeroSMulDivisors R M]
{χ₁ χ₂ : L → R}
(h : χ₁ ≠ χ₂)
:
Disjoint (LieModule.genWeightSpace M χ₁) (LieModule.genWeightSpace M χ₂)
theorem
LieModule.injOn_genWeightSpace
(R : Type u_2)
(L : Type u_3)
(M : Type u_4)
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[LieAlgebra.IsNilpotent R L]
[NoZeroSMulDivisors R M]
:
Set.InjOn (fun (χ : L → R) => LieModule.genWeightSpace M χ) {χ : L → R | LieModule.genWeightSpace M χ ≠ ⊥}
theorem
LieModule.independent_genWeightSpace
(R : Type u_2)
(L : Type u_3)
(M : Type u_4)
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[LieAlgebra.IsNilpotent R L]
[NoZeroSMulDivisors R M]
:
CompleteLattice.Independent fun (χ : L → R) => LieModule.genWeightSpace M χ
Lie module weight spaces are independent.
See also LieModule.independent_genWeightSpace'.
theorem
LieModule.independent_genWeightSpace'
(R : Type u_2)
(L : Type u_3)
(M : Type u_4)
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[LieAlgebra.IsNilpotent R L]
[NoZeroSMulDivisors R M]
:
CompleteLattice.Independent fun (χ : LieModule.Weight R L M) => LieModule.genWeightSpace M ⇑χ
theorem
LieModule.independent_genWeightSpaceOf
(R : Type u_2)
(L : Type u_3)
(M : Type u_4)
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[LieAlgebra.IsNilpotent R L]
[NoZeroSMulDivisors R M]
(x : L)
:
CompleteLattice.Independent fun (χ : R) => LieModule.genWeightSpaceOf M χ x
theorem
LieModule.finite_genWeightSpaceOf_ne_bot
(R : Type u_2)
(L : Type u_3)
(M : Type u_4)
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[LieAlgebra.IsNilpotent R L]
[NoZeroSMulDivisors R M]
[IsNoetherian R M]
(x : L)
:
{χ : R | LieModule.genWeightSpaceOf M χ x ≠ ⊥}.Finite
theorem
LieModule.finite_genWeightSpace_ne_bot
(R : Type u_2)
(L : Type u_3)
(M : Type u_4)
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[LieAlgebra.IsNilpotent R L]
[NoZeroSMulDivisors R M]
[IsNoetherian R M]
:
{χ : L → R | LieModule.genWeightSpace M χ ≠ ⊥}.Finite
instance
LieModule.Weight.instFinite
(R : Type u_2)
(L : Type u_3)
(M : Type u_4)
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[LieAlgebra.IsNilpotent R L]
[NoZeroSMulDivisors R M]
[IsNoetherian R M]
:
Finite (LieModule.Weight R L M)
Equations
- ⋯ = ⋯
noncomputable instance
LieModule.Weight.instFintype
(R : Type u_2)
(L : Type u_3)
(M : Type u_4)
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[LieAlgebra.IsNilpotent R L]
[NoZeroSMulDivisors R M]
[IsNoetherian R M]
:
Fintype (LieModule.Weight R L M)
Equations
- LieModule.Weight.instFintype R L M = Fintype.ofFinite (LieModule.Weight R L M)
class
LieModule.IsTriangularizable
(R : Type u_2)
(L : Type u_3)
(M : Type u_4)
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule 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.
- maxGenEigenspace_eq_top : ∀ (x : L), ⨆ (φ : R), ((LieModule.toEnd R L M) x).maxGenEigenspace φ = ⊤
Instances
instance
LieModule.instIsTriangularizableSubtypeMemLieSubalgebra
(R : Type u_2)
(L : Type u_3)
(M : Type u_4)
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
(L' : LieSubalgebra R L)
[LieModule.IsTriangularizable R L M]
:
LieModule.IsTriangularizable R (↥L') M
Equations
- ⋯ = ⋯
instance
LieModule.instIsTriangularizableSubtypeMemLieSubmodule
(R : Type u_2)
(L : Type u_3)
(M : Type u_4)
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
(I : LieIdeal R L)
[LieModule.IsTriangularizable R L M]
:
LieModule.IsTriangularizable R (↥I) M
Equations
- ⋯ = ⋯
instance
LieModule.instIsTriangularizableSubtypeEndMemLieSubalgebraRangeToEnd
(R : Type u_2)
(L : Type u_3)
(M : Type u_4)
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[LieModule.IsTriangularizable R L M]
:
LieModule.IsTriangularizable R (↥(LieModule.toEnd R L M).range) M
Equations
- ⋯ = ⋯
@[simp]
theorem
LieModule.iSup_genWeightSpaceOf_eq_top
(R : Type u_2)
(L : Type u_3)
(M : Type u_4)
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[LieAlgebra.IsNilpotent R L]
[LieModule.IsTriangularizable R L M]
(x : L)
:
⨆ (φ : R), LieModule.genWeightSpaceOf M φ x = ⊤
@[simp]
theorem
LieModule.trace_toEnd_genWeightSpace
(R : Type u_2)
(L : Type u_3)
(M : Type u_4)
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[LieAlgebra.IsNilpotent R L]
[IsDomain R]
[IsPrincipalIdealRing R]
[Module.Free R M]
[Module.Finite R M]
(χ : L → R)
(x : L)
:
(LinearMap.trace R ↥(LieModule.genWeightSpace M χ)) ((LieModule.toEnd R L ↥(LieModule.genWeightSpace M χ)) x) = Module.finrank R ↥(LieModule.genWeightSpace M χ) • χ x
instance
LieModule.instIsTriangularizableOfIsAlgClosed
(K : Type u_1)
(L : Type u_3)
(M : Type u_4)
[LieRing L]
[AddCommGroup M]
[LieRingModule L M]
[Field K]
[LieAlgebra K L]
[Module K M]
[LieModule K L M]
[FiniteDimensional K M]
[IsAlgClosed K]
:
Equations
- ⋯ = ⋯
instance
LieModule.instIsTriangularizableSubtypeMemLieSubmodule_1
(K : Type u_1)
(L : Type u_3)
(M : Type u_4)
[LieRing L]
[AddCommGroup M]
[LieRingModule L M]
[Field K]
[LieAlgebra K L]
[Module K M]
[LieModule K L M]
[FiniteDimensional K M]
(N : LieSubmodule K L M)
[LieModule.IsTriangularizable K L M]
:
LieModule.IsTriangularizable K L ↥N
Equations
- ⋯ = ⋯
theorem
LieModule.iSup_genWeightSpace_eq_top
(K : Type u_1)
(L : Type u_3)
(M : Type u_4)
[LieRing L]
[AddCommGroup M]
[LieRingModule L M]
[Field K]
[LieAlgebra K L]
[Module K M]
[LieModule K L M]
[LieAlgebra.IsNilpotent K L]
[FiniteDimensional K M]
[LieModule.IsTriangularizable K L M]
:
⨆ (χ : L → K), LieModule.genWeightSpace M χ = ⊤
For a triangularizable Lie module in finite dimensions, the weight spaces span the entire space.
See also LieModule.iSup_genWeightSpace_eq_top'.
theorem
LieModule.iSup_genWeightSpace_eq_top'
(K : Type u_1)
(L : Type u_3)
(M : Type u_4)
[LieRing L]
[AddCommGroup M]
[LieRingModule L M]
[Field K]
[LieAlgebra K L]
[Module K M]
[LieModule K L M]
[LieAlgebra.IsNilpotent K L]
[FiniteDimensional K M]
[LieModule.IsTriangularizable K L M]
:
⨆ (χ : LieModule.Weight K L M), LieModule.genWeightSpace M ⇑χ = ⊤