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.weightSpaceOfLieModule.weightSpaceLieModule.WeightLieModule.posFittingCompOfLieModule.posFittingCompLieModule.iSup_ucs_eq_weightSpace_zeroLieModule.iInf_lowerCentralSeries_eq_posFittingCompLieModule.isCompl_weightSpace_zero_posFittingCompLieModule.independent_weightSpaceLieModule.iSup_weightSpace_eq_top
References #
Tags #
lie character, eigenvalue, eigenspace, weight, weight vector, root, root vector
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)
(χ₂ : 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}
{χ₂ : R}
{x : L}
{y : L}
{m : M}
(hy : y ∈ ((LieModule.toEnd R L L) x).maxGenEigenspace χ₁)
(hm : m ∈ ((LieModule.toEnd R L M) x).maxGenEigenspace χ₂)
:
def
LieModule.weightSpaceOf
{R : Type u_2}
{L : Type u_3}
(M : Type u_4)
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[LieAlgebra.IsNilpotent R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
(χ : 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
weightSpaceOf 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.weightSpaceOf M χ x = let __src := ((LieModule.toEnd R L M) x).maxGenEigenspace χ; { toSubmodule := __src, lie_mem := ⋯ }
Instances For
theorem
LieModule.mem_weightSpaceOf
{R : Type u_2}
{L : Type u_3}
(M : Type u_4)
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[LieAlgebra.IsNilpotent R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
(χ : R)
(x : L)
(m : M)
:
m ∈ LieModule.weightSpaceOf M χ x ↔ ∃ (k : ℕ), (((LieModule.toEnd R L M) x - χ • 1) ^ k) m = 0
theorem
LieModule.coe_weightSpaceOf_zero
{R : Type u_2}
{L : Type u_3}
(M : Type u_4)
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[LieAlgebra.IsNilpotent R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
(x : L)
:
↑(LieModule.weightSpaceOf M 0 x) = ⨆ (k : ℕ), LinearMap.ker ((LieModule.toEnd R L M) x ^ k)
def
LieModule.weightSpace
{R : Type u_2}
{L : Type u_3}
(M : Type u_4)
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[LieAlgebra.IsNilpotent 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 nilpotent Lie algebra L and χ : L → R is a family of
scalars, then weightSpace 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.weightSpace M χ = ⨅ (x : L), LieModule.weightSpaceOf M (χ x) x
Instances For
theorem
LieModule.mem_weightSpace
{R : Type u_2}
{L : Type u_3}
(M : Type u_4)
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[LieAlgebra.IsNilpotent R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
(χ : L → R)
(m : M)
:
m ∈ LieModule.weightSpace M χ ↔ ∀ (x : L), ∃ (k : ℕ), (((LieModule.toEnd R L M) x - χ x • 1) ^ k) m = 0
theorem
LieModule.weightSpace_le_weightSpaceOf
{R : Type u_2}
{L : Type u_3}
(M : Type u_4)
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[LieAlgebra.IsNilpotent R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
(x : L)
(χ : L → R)
:
LieModule.weightSpace M χ ≤ LieModule.weightSpaceOf M (χ x) x
structure
LieModule.Weight
(R : Type u_2)
(L : Type u_3)
(M : Type u_4)
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[LieAlgebra.IsNilpotent R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
:
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.
- weightSpace_ne_bot' : LieModule.weightSpace M self.toFun ≠ ⊥
Instances For
theorem
LieModule.Weight.weightSpace_ne_bot'
{R : Type u_2}
{L : Type u_3}
{M : Type u_4}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[LieAlgebra.IsNilpotent R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
(self : LieModule.Weight R L M)
:
LieModule.weightSpace 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]
[LieAlgebra.IsNilpotent R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
:
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]
[LieAlgebra.IsNilpotent R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
(χ : L → R)
(h : LieModule.weightSpace M χ ≠ ⊥)
:
⇑{ toFun := χ, weightSpace_ne_bot' := h } = χ
theorem
LieModule.Weight.weightSpace_ne_bot
{R : Type u_2}
{L : Type u_3}
(M : Type u_4)
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[LieAlgebra.IsNilpotent R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
(χ : LieModule.Weight R L M)
:
LieModule.weightSpace M ⇑χ ≠ ⊥
theorem
LieModule.Weight.ext
{R : Type u_2}
{L : Type u_3}
{M : Type u_4}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[LieAlgebra.IsNilpotent R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
{χ₁ : LieModule.Weight R L M}
{χ₂ : 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]
[LieAlgebra.IsNilpotent R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
{χ₁ : LieModule.Weight R L M}
{χ₂ : 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]
[LieAlgebra.IsNilpotent R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
(χ : LieModule.Weight R L M)
:
∃ x ∈ LieModule.weightSpace 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]
[LieAlgebra.IsNilpotent R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[Subsingleton M]
:
IsEmpty (LieModule.Weight R L M)
Equations
- ⋯ = ⋯
instance
LieModule.Weight.instZeroOfNontrivialSubtypeMemSubmoduleWeightSpaceOfNatForall
{R : Type u_2}
{L : Type u_3}
{M : Type u_4}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[LieAlgebra.IsNilpotent R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[Nontrivial ↥↑(LieModule.weightSpace M 0)]
:
Zero (LieModule.Weight R L M)
Equations
- LieModule.Weight.instZeroOfNontrivialSubtypeMemSubmoduleWeightSpaceOfNatForall = { zero := { toFun := 0, weightSpace_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]
[LieAlgebra.IsNilpotent R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[Nontrivial ↥↑(LieModule.weightSpace 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]
[LieAlgebra.IsNilpotent R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[Nontrivial ↥↑(LieModule.weightSpace 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]
[LieAlgebra.IsNilpotent R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
(χ : 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.
Instances For
@[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]
[LieAlgebra.IsNilpotent R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
{χ : 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]
[LieAlgebra.IsNilpotent R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
(χ : 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]
[LieAlgebra.IsNilpotent R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[Nontrivial ↥↑(LieModule.weightSpace 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]
[LieAlgebra.IsNilpotent R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[Nontrivial ↥↑(LieModule.weightSpace 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]
[LieAlgebra.IsNilpotent R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
(χ : LieModule.Weight R L M)
:
The proposition that a weight of a Lie module is non-zero.
Instances For
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]
[LieAlgebra.IsNilpotent R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[Nontrivial ↥↑(LieModule.weightSpace M 0)]
{χ : LieModule.Weight R L M}
:
def
LieModule.Weight.equivSetOf
(R : Type u_2)
(L : Type u_3)
(M : Type u_4)
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[LieAlgebra.IsNilpotent R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
:
LieModule.Weight R L M ≃ ↑{χ : L → R | LieModule.weightSpace M χ ≠ ⊥}
The set of weights is equivalent to a subtype.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
LieModule.Weight.weightSpaceOf_ne_bot
{R : Type u_2}
{L : Type u_3}
{M : Type u_4}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[LieAlgebra.IsNilpotent R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
(χ : LieModule.Weight R L M)
(x : L)
:
LieModule.weightSpaceOf 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]
[LieAlgebra.IsNilpotent R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
(χ : 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]
[LieAlgebra.IsNilpotent R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[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_weightSpace_eq_top_of_nilpotent'
{R : Type u_2}
{L : Type u_3}
(M : Type u_4)
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[LieAlgebra.IsNilpotent R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[LieModule.IsNilpotent R L M]
:
LieModule.weightSpace M 0 = ⊤
See also the more useful form LieModule.zero_weightSpace_eq_top_of_nilpotent.
theorem
LieModule.coe_weightSpace_of_top
{R : Type u_2}
{L : Type u_3}
(M : Type u_4)
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[LieAlgebra.IsNilpotent R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
(χ : L → R)
:
↑(LieModule.weightSpace M (χ ∘ ⇑⊤.incl)) = ↑(LieModule.weightSpace M χ)
@[simp]
theorem
LieModule.zero_weightSpace_eq_top_of_nilpotent
{R : Type u_2}
{L : Type u_3}
(M : Type u_4)
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[LieAlgebra.IsNilpotent R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[LieModule.IsNilpotent R L M]
:
LieModule.weightSpace M 0 = ⊤
theorem
LieModule.exists_weightSpace_le_ker_of_isNoetherian
{R : Type u_2}
{L : Type u_3}
(M : Type u_4)
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[LieAlgebra.IsNilpotent R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[IsNoetherian R M]
(χ : L → R)
(x : L)
:
∃ (k : ℕ),
↑(LieModule.weightSpace M χ) ≤ LinearMap.ker (((LieModule.toEnd R L M) x - (algebraMap R (Module.End R M)) (χ x)) ^ k)
theorem
LieModule.exists_weightSpace_zero_le_ker_of_isNoetherian
(R : Type u_2)
{L : Type u_3}
(M : Type u_4)
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[LieAlgebra.IsNilpotent R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[IsNoetherian R M]
(x : L)
:
∃ (k : ℕ), ↑(LieModule.weightSpace 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]
[LieAlgebra.IsNilpotent R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[IsNoetherian R M]
(χ : L → R)
(x : L)
:
IsNilpotent
((LieModule.toEnd R L ↥↑(LieModule.weightSpace M χ)) x - (algebraMap R (Module.End R ↥↑(LieModule.weightSpace M χ))) (χ x))
theorem
LieModule.isNilpotent_toEnd_weightSpace_zero
{R : Type u_2}
{L : Type u_3}
(M : Type u_4)
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[LieAlgebra.IsNilpotent R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[IsNoetherian R M]
(x : L)
:
IsNilpotent ((LieModule.toEnd R L ↥↑(LieModule.weightSpace M 0)) x)
A (nilpotent) Lie algebra acts nilpotently on the zero weight space of a Noetherian Lie module.
instance
LieModule.instIsNilpotentSubtypeMemSubmoduleWeightSpaceOfNatForallOfIsNoetherian
{R : Type u_2}
{L : Type u_3}
(M : Type u_4)
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[LieAlgebra.IsNilpotent R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[IsNoetherian R M]
:
LieModule.IsNilpotent R L ↥↑(LieModule.weightSpace M 0)
By Engel's theorem, the zero weight space of a Noetherian Lie module is nilpotent.
Equations
- ⋯ = ⋯
@[simp]
theorem
LieModule.weightSpace_zero_normalizer_eq_self
(R : Type u_2)
(L : Type u_3)
(M : Type u_4)
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[LieAlgebra.IsNilpotent R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
:
(LieModule.weightSpace M 0).normalizer = LieModule.weightSpace M 0
theorem
LieModule.iSup_ucs_le_weightSpace_zero
(R : Type u_2)
(L : Type u_3)
(M : Type u_4)
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[LieAlgebra.IsNilpotent R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
:
⨆ (k : ℕ), LieSubmodule.ucs k ⊥ ≤ LieModule.weightSpace M 0
theorem
LieModule.iSup_ucs_eq_weightSpace_zero
(R : Type u_2)
(L : Type u_3)
(M : Type u_4)
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[LieAlgebra.IsNilpotent R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[IsNoetherian R M]
:
⨆ (k : ℕ), LieSubmodule.ucs k ⊥ = LieModule.weightSpace 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]
[LieAlgebra.IsNilpotent R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
(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₀ = weightSpaceOf 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
theorem
LieModule.mem_posFittingCompOf
(R : Type u_2)
{L : Type u_3}
{M : Type u_4}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[LieAlgebra.IsNilpotent R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
(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]
[LieAlgebra.IsNilpotent R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
(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]
[LieAlgebra.IsNilpotent R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[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]
[LieAlgebra.IsNilpotent R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
:
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
Instances For
theorem
LieModule.mem_posFittingComp
(R : Type u_2)
(L : Type u_3)
(M : Type u_4)
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[LieAlgebra.IsNilpotent R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
(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]
[LieAlgebra.IsNilpotent R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
(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]
[LieAlgebra.IsNilpotent R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
:
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]
[LieAlgebra.IsNilpotent R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[IsNoetherian R M]
[IsArtinian R M]
:
⨅ (k : ℕ), LieModule.lowerCentralSeries R L M k = LieModule.posFittingComp R L M
See also LieModule.iSup_ucs_eq_weightSpace_zero.
@[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]
[LieAlgebra.IsNilpotent R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[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]
[LieAlgebra.IsNilpotent R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
{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_weightSpace_le
{R : Type u_2}
{L : Type u_3}
{M : Type u_4}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[LieAlgebra.IsNilpotent R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
{M₂ : Type u_5}
[AddCommGroup M₂]
[Module R M₂]
[LieRingModule L M₂]
[LieModule R L M₂]
{χ : L → R}
(f : M →ₗ⁅R,L⁆ M₂)
:
LieSubmodule.map f (LieModule.weightSpace M χ) ≤ LieModule.weightSpace M₂ χ
theorem
LieModule.comap_weightSpace_eq_of_injective
{R : Type u_2}
{L : Type u_3}
{M : Type u_4}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[LieAlgebra.IsNilpotent R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
{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.comap f (LieModule.weightSpace M₂ χ) = LieModule.weightSpace M χ
theorem
LieModule.map_weightSpace_eq_of_injective
{R : Type u_2}
{L : Type u_3}
{M : Type u_4}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[LieAlgebra.IsNilpotent R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
{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.weightSpace M χ) = LieModule.weightSpace M₂ χ ⊓ f.range
theorem
LieModule.map_weightSpace_eq
{R : Type u_2}
{L : Type u_3}
{M : Type u_4}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[LieAlgebra.IsNilpotent R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
{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.weightSpace M χ) = LieModule.weightSpace 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]
[LieAlgebra.IsNilpotent R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
{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]
[LieAlgebra.IsNilpotent R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[IsNoetherian R M]
[IsArtinian R M]
{N₁ : LieSubmodule R L M}
{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.weightSpace_weightSpaceOf_map_incl
{R : Type u_2}
{L : Type u_3}
{M : Type u_4}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[LieAlgebra.IsNilpotent R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
(x : L)
(χ : L → R)
:
LieSubmodule.map (LieModule.weightSpaceOf M (χ x) x).incl
(LieModule.weightSpace (↥↑(LieModule.weightSpaceOf M (χ x) x)) χ) = LieModule.weightSpace M χ
theorem
LieModule.isCompl_weightSpaceOf_zero_posFittingCompOf
(R : Type u_2)
(L : Type u_3)
(M : Type u_4)
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[LieAlgebra.IsNilpotent R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[IsNoetherian R M]
[IsArtinian R M]
(x : L)
:
IsCompl (LieModule.weightSpaceOf M 0 x) (LieModule.posFittingCompOf R M x)
theorem
LieModule.isCompl_weightSpace_zero_posFittingComp
(R : Type u_2)
(L : Type u_3)
(M : Type u_4)
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[LieAlgebra.IsNilpotent R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[IsNoetherian R M]
[IsArtinian R M]
:
IsCompl (LieModule.weightSpace M 0) (LieModule.posFittingComp R L M)
This is the Fitting decomposition of the Lie module M.
theorem
LieModule.disjoint_weightSpaceOf
(R : Type u_2)
(L : Type u_3)
(M : Type u_4)
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[LieAlgebra.IsNilpotent R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[NoZeroSMulDivisors R M]
{x : L}
{φ₁ : R}
{φ₂ : R}
(h : φ₁ ≠ φ₂)
:
Disjoint (LieModule.weightSpaceOf M φ₁ x) (LieModule.weightSpaceOf M φ₂ x)
theorem
LieModule.disjoint_weightSpace
(R : Type u_2)
(L : Type u_3)
(M : Type u_4)
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[LieAlgebra.IsNilpotent R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[NoZeroSMulDivisors R M]
{χ₁ : L → R}
{χ₂ : L → R}
(h : χ₁ ≠ χ₂)
:
Disjoint (LieModule.weightSpace M χ₁) (LieModule.weightSpace M χ₂)
theorem
LieModule.injOn_weightSpace
(R : Type u_2)
(L : Type u_3)
(M : Type u_4)
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[LieAlgebra.IsNilpotent R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[NoZeroSMulDivisors R M]
:
Set.InjOn (fun (χ : L → R) => LieModule.weightSpace M χ) {χ : L → R | LieModule.weightSpace M χ ≠ ⊥}
theorem
LieModule.independent_weightSpace
(R : Type u_2)
(L : Type u_3)
(M : Type u_4)
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[LieAlgebra.IsNilpotent R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[NoZeroSMulDivisors R M]
:
CompleteLattice.Independent fun (χ : L → R) => LieModule.weightSpace M χ
Lie module weight spaces are independent.
See also LieModule.independent_weightSpace'.
theorem
LieModule.independent_weightSpace'
(R : Type u_2)
(L : Type u_3)
(M : Type u_4)
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[LieAlgebra.IsNilpotent R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[NoZeroSMulDivisors R M]
:
CompleteLattice.Independent fun (χ : LieModule.Weight R L M) => LieModule.weightSpace M ⇑χ
theorem
LieModule.independent_weightSpaceOf
(R : Type u_2)
(L : Type u_3)
(M : Type u_4)
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[LieAlgebra.IsNilpotent R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[NoZeroSMulDivisors R M]
(x : L)
:
CompleteLattice.Independent fun (χ : R) => LieModule.weightSpaceOf M χ x
theorem
LieModule.finite_weightSpaceOf_ne_bot
(R : Type u_2)
(L : Type u_3)
(M : Type u_4)
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[LieAlgebra.IsNilpotent R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[NoZeroSMulDivisors R M]
[IsNoetherian R M]
(x : L)
:
{χ : R | LieModule.weightSpaceOf M χ x ≠ ⊥}.Finite
theorem
LieModule.finite_weightSpace_ne_bot
(R : Type u_2)
(L : Type u_3)
(M : Type u_4)
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[LieAlgebra.IsNilpotent R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[NoZeroSMulDivisors R M]
[IsNoetherian R M]
:
{χ : L → R | LieModule.weightSpace 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]
[LieAlgebra.IsNilpotent R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[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]
[LieAlgebra.IsNilpotent R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[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.
- iSup_eq_top : ∀ (x : L), ⨆ (φ : R), ⨆ (k : ℕ), (((LieModule.toEnd R L M) x).genEigenspace φ) k = ⊤
Instances
theorem
LieModule.IsTriangularizable.iSup_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]
[self : LieModule.IsTriangularizable R L M]
(x : L)
:
⨆ (φ : R), ⨆ (k : ℕ), (((LieModule.toEnd R L M) x).genEigenspace φ) k = ⊤
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.instIsTriangularizableSubtypeMemSubmodule
(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_weightSpaceOf_eq_top
(R : Type u_2)
(L : Type u_3)
(M : Type u_4)
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[LieAlgebra.IsNilpotent R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[LieModule.IsTriangularizable R L M]
(x : L)
:
⨆ (φ : R), LieModule.weightSpaceOf M φ x = ⊤
@[simp]
theorem
LieModule.trace_toEnd_weightSpace
(R : Type u_2)
(L : Type u_3)
(M : Type u_4)
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[LieAlgebra.IsNilpotent R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[IsDomain R]
[IsPrincipalIdealRing R]
[Module.Free R M]
[Module.Finite R M]
(χ : L → R)
(x : L)
:
(LinearMap.trace R ↥↑(LieModule.weightSpace M χ)) ((LieModule.toEnd R L ↥↑(LieModule.weightSpace M χ)) x) = FiniteDimensional.finrank R ↥↑(LieModule.weightSpace 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.instIsTriangularizableSubtypeMemSubmodule_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_weightSpace_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.weightSpace M χ = ⊤
For a triangularizable Lie module in finite dimensions, the weight spaces span the entire space.
See also LieModule.iSup_weightSpace_eq_top'.
theorem
LieModule.iSup_weightSpace_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.weightSpace M ⇑χ = ⊤