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.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 (Module.End.maximalGeneralizedEigenspace ((LieModule.toEndomorphism R L M₁) x) χ₁)
(Module.End.maximalGeneralizedEigenspace ((LieModule.toEndomorphism R L M₂) x) χ₂)) ≤ Module.End.maximalGeneralizedEigenspace ((LieModule.toEndomorphism R L M₃) x) (χ₁ + χ₂)
See also bourbaki1975b Chapter VII §1.1, Proposition 2 (ii).
theorem
LieModule.lie_mem_maxGenEigenspace_toEndomorphism
{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 ∈ Module.End.maximalGeneralizedEigenspace ((LieModule.toEndomorphism R L L) x) χ₁)
(hm : m ∈ Module.End.maximalGeneralizedEigenspace ((LieModule.toEndomorphism R L M) x) χ₂)
:
⁅y, m⁆ ∈ Module.End.maximalGeneralizedEigenspace ((LieModule.toEndomorphism R L M) x) (χ₁ + χ₂)
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 := Module.End.maximalGeneralizedEigenspace ((LieModule.toEndomorphism R L M) x) χ; { 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.toEndomorphism 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.toEndomorphism 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.toEndomorphism 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
@[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 (χ ∘ ⇑(LieSubalgebra.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.toEndomorphism 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.toEndomorphism R L M) x ^ k)
theorem
LieModule.isNilpotent_toEndomorphism_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.toEndomorphism R L ↥↑(LieModule.weightSpace M χ)) x - (algebraMap R (Module.End R ↥↑(LieModule.weightSpace M χ))) (χ x))
theorem
LieModule.isNilpotent_toEndomorphism_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.toEndomorphism 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.instIsNilpotentSubtypeMemSubmoduleToSemiringToCommSemiringToAddCommMonoidInstMembershipSetLikeToSubmoduleWeightSpaceOfNatForAllToOfNat0InstZeroToZeroToCommMonoidWithZeroAddCommGroupToRingInstModuleSubtypeMemSubmoduleToSemiringToCommSemiringToAddCommMonoidInstMembershipSetLikeToSubmoduleAddCommMonoidInstLieRingModuleSubtypeMemSubmoduleToSemiringToCommSemiringToAddCommMonoidInstMembershipSetLikeToSubmoduleAddCommGroupToRing
{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]
:
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 := toEndomorphism 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.toEndomorphism 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.toEndomorphism 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₂ χ ⊓ LieModuleHom.range f
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 (LieSubmodule.incl N₁) (LieModule.posFittingComp R L ↥↑N₁) ⊔ LieSubmodule.map (LieSubmodule.incl N₂) (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 (LieSubmodule.incl (LieModule.weightSpaceOf M (χ x) x))
(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 χ
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)
:
Set.Finite {χ : R | LieModule.weightSpaceOf M χ x ≠ ⊥}
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]
:
Set.Finite {χ : L → R | LieModule.weightSpace M χ ≠ ⊥}
@[inline, reducible]
noncomputable abbrev
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]
[NoZeroSMulDivisors R M]
[IsNoetherian R M]
:
Finset (L → R)
The collection of weights of a Noetherian Lie module, bundled as a Finset.
Equations
- LieModule.weight R L M = Set.Finite.toFinset ⋯
Instances For
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 : ℕ), (Module.End.generalizedEigenspace ((LieModule.toEndomorphism R L M) x) φ) k = ⊤
Instances
@[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_toEndomorphism_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.toEndomorphism 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.instIsTriangularizableSubtypeMemSubmoduleToSemiringToCommSemiringToCommRingToEuclideanDomainToAddCommMonoidInstMembershipSetLikeToSubmoduleAddCommGroupToRingToDivisionRingInstModuleSubtypeMemSubmoduleToSemiringToCommSemiringToAddCommMonoidInstMembershipSetLikeToSubmoduleAddCommMonoidInstLieRingModuleSubtypeMemSubmoduleToSemiringToCommSemiringToAddCommMonoidInstMembershipSetLikeToSubmoduleAddCommGroupToRingInstLieModule
(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 χ = ⊤