Weights and roots of Lie modules and Lie algebras with respect to Cartan subalgebras #
Given a Lie algebra L which is not necessarily nilpotent, it may be useful to study its
representations by restricting them to a nilpotent subalgebra (e.g., a Cartan subalgebra). In the
particular case when we view L as a module over itself via the adjoint action, the weight spaces
of L restricted to a nilpotent subalgebra are known as root spaces.
Basic definitions and properties of the above ideas are provided in this file.
Main definitions #
noncomputable def
LieModule.IsWeight
{R : Type u_1}
{L : Type u_2}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
(H : LieSubalgebra R L)
[LieAlgebra.IsNilpotent R ↥H]
(M : Type u_3)
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
(χ : LieAlgebra.LieCharacter R ↥H)
:
Given a Lie module M of a Lie algebra L, a weight of M with respect to a nilpotent
subalgebra H ⊆ L is a Lie character whose corresponding weight space is non-empty.
Equations
- LieModule.IsWeight H M χ = (LieModule.weightSpace M ⇑χ ≠ ⊥)
Instances For
theorem
LieModule.isWeight_zero_of_nilpotent
{R : Type u_1}
{L : Type u_2}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
(M : Type u_3)
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[Nontrivial M]
[LieAlgebra.IsNilpotent R L]
[LieModule.IsNilpotent R L M]
:
LieModule.IsWeight ⊤ M 0
For a non-trivial nilpotent Lie module over a nilpotent Lie algebra, the zero character is a
weight with respect to the ⊤ Lie subalgebra.
@[inline, reducible]
noncomputable abbrev
LieAlgebra.rootSpace
{R : Type u_1}
{L : Type u_2}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
(H : LieSubalgebra R L)
[LieAlgebra.IsNilpotent R ↥H]
(χ : ↥H → R)
:
LieSubmodule R (↥H) L
Given a nilpotent Lie subalgebra H ⊆ L, the root space of a map χ : H → R is the weight
space of L regarded as a module of H via the adjoint action.
Equations
Instances For
theorem
LieAlgebra.zero_rootSpace_eq_top_of_nilpotent
{R : Type u_1}
{L : Type u_2}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[LieAlgebra.IsNilpotent R L]
:
@[inline, reducible]
noncomputable abbrev
LieAlgebra.IsRoot
{R : Type u_1}
{L : Type u_2}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
(H : LieSubalgebra R L)
[LieAlgebra.IsNilpotent R ↥H]
(χ : LieAlgebra.LieCharacter R ↥H)
:
A root of a Lie algebra L with respect to a nilpotent subalgebra H ⊆ L is a weight of L,
regarded as a module of H via the adjoint action.
Equations
- LieAlgebra.IsRoot H χ = (χ ≠ 0 ∧ LieModule.IsWeight H L χ)
Instances For
@[simp]
theorem
LieAlgebra.rootSpace_comap_eq_weightSpace
{R : Type u_1}
{L : Type u_2}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
(H : LieSubalgebra R L)
[LieAlgebra.IsNilpotent R ↥H]
(χ : ↥H → R)
:
LieSubmodule.comap (LieSubalgebra.incl' H) (LieAlgebra.rootSpace H χ) = LieModule.weightSpace (↥H) χ
theorem
LieAlgebra.lie_mem_weightSpace_of_mem_weightSpace
{R : Type u_1}
{L : Type u_2}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
{H : LieSubalgebra R L}
[LieAlgebra.IsNilpotent R ↥H]
{M : Type u_3}
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
{χ₁ : ↥H → R}
{χ₂ : ↥H → R}
{x : L}
{m : M}
(hx : x ∈ LieAlgebra.rootSpace H χ₁)
(hm : m ∈ LieModule.weightSpace M χ₂)
:
noncomputable def
LieAlgebra.rootSpaceWeightSpaceProductAux
(R : Type u_1)
(L : Type u_2)
[CommRing R]
[LieRing L]
[LieAlgebra R L]
(H : LieSubalgebra R L)
[LieAlgebra.IsNilpotent R ↥H]
(M : Type u_3)
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
{χ₁ : ↥H → R}
{χ₂ : ↥H → R}
{χ₃ : ↥H → R}
(hχ : χ₁ + χ₂ = χ₃)
:
↥↑(LieAlgebra.rootSpace H χ₁) →ₗ[R] ↥↑(LieModule.weightSpace M χ₂) →ₗ[R] ↥↑(LieModule.weightSpace M χ₃)
Auxiliary definition for rootSpaceWeightSpaceProduct,
which is close to the deterministic timeout limit.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
LieAlgebra.rootSpaceWeightSpaceProduct
(R : Type u_1)
(L : Type u_2)
[CommRing R]
[LieRing L]
[LieAlgebra R L]
(H : LieSubalgebra R L)
[LieAlgebra.IsNilpotent R ↥H]
(M : Type u_3)
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
(χ₁ : ↥H → R)
(χ₂ : ↥H → R)
(χ₃ : ↥H → R)
(hχ : χ₁ + χ₂ = χ₃)
:
TensorProduct R ↥↑(LieAlgebra.rootSpace H χ₁) ↥↑(LieModule.weightSpace M χ₂) →ₗ⁅R,↥H⁆ ↥↑(LieModule.weightSpace M χ₃)
Given a nilpotent Lie subalgebra H ⊆ L together with χ₁ χ₂ : H → R, there is a natural
R-bilinear product of root vectors and weight vectors, compatible with the actions of H.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
LieAlgebra.coe_rootSpaceWeightSpaceProduct_tmul
(R : Type u_1)
(L : Type u_2)
[CommRing R]
[LieRing L]
[LieAlgebra R L]
(H : LieSubalgebra R L)
[LieAlgebra.IsNilpotent R ↥H]
(M : Type u_3)
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
(χ₁ : ↥H → R)
(χ₂ : ↥H → R)
(χ₃ : ↥H → R)
(hχ : χ₁ + χ₂ = χ₃)
(x : ↥(LieAlgebra.rootSpace H χ₁))
(m : ↥(LieModule.weightSpace M χ₂))
:
theorem
LieAlgebra.mapsTo_toEndomorphism_weightSpace_add_of_mem_rootSpace
(R : Type u_1)
(L : Type u_2)
[CommRing R]
[LieRing L]
[LieAlgebra R L]
(H : LieSubalgebra R L)
[LieAlgebra.IsNilpotent R ↥H]
(M : Type u_3)
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
(α : ↥H → R)
(χ : ↥H → R)
{x : L}
(hx : x ∈ LieAlgebra.rootSpace H α)
:
Set.MapsTo ⇑((LieModule.toEndomorphism R L M) x) ↑(LieModule.weightSpace M χ) ↑(LieModule.weightSpace M (α + χ))
noncomputable def
LieAlgebra.rootSpaceProduct
(R : Type u_1)
(L : Type u_2)
[CommRing R]
[LieRing L]
[LieAlgebra R L]
(H : LieSubalgebra R L)
[LieAlgebra.IsNilpotent R ↥H]
(χ₁ : ↥H → R)
(χ₂ : ↥H → R)
(χ₃ : ↥H → R)
(hχ : χ₁ + χ₂ = χ₃)
:
TensorProduct R ↥↑(LieAlgebra.rootSpace H χ₁) ↥↑(LieAlgebra.rootSpace H χ₂) →ₗ⁅R,↥H⁆ ↥↑(LieAlgebra.rootSpace H χ₃)
Given a nilpotent Lie subalgebra H ⊆ L together with χ₁ χ₂ : H → R, there is a natural
R-bilinear product of root vectors, compatible with the actions of H.
Equations
- LieAlgebra.rootSpaceProduct R L H χ₁ χ₂ χ₃ hχ = LieAlgebra.rootSpaceWeightSpaceProduct R L H L χ₁ χ₂ χ₃ hχ
Instances For
@[simp]
theorem
LieAlgebra.rootSpaceProduct_def
(R : Type u_1)
(L : Type u_2)
[CommRing R]
[LieRing L]
[LieAlgebra R L]
(H : LieSubalgebra R L)
[LieAlgebra.IsNilpotent R ↥H]
:
theorem
LieAlgebra.rootSpaceProduct_tmul
(R : Type u_1)
(L : Type u_2)
[CommRing R]
[LieRing L]
[LieAlgebra R L]
(H : LieSubalgebra R L)
[LieAlgebra.IsNilpotent R ↥H]
(χ₁ : ↥H → R)
(χ₂ : ↥H → R)
(χ₃ : ↥H → R)
(hχ : χ₁ + χ₂ = χ₃)
(x : ↥(LieAlgebra.rootSpace H χ₁))
(y : ↥(LieAlgebra.rootSpace H χ₂))
:
noncomputable def
LieAlgebra.zeroRootSubalgebra
(R : Type u_1)
(L : Type u_2)
[CommRing R]
[LieRing L]
[LieAlgebra R L]
(H : LieSubalgebra R L)
[LieAlgebra.IsNilpotent R ↥H]
:
LieSubalgebra R L
Given a nilpotent Lie subalgebra H ⊆ L, the root space of the zero map 0 : H → R is a Lie
subalgebra of L.
Equations
- LieAlgebra.zeroRootSubalgebra R L H = { toSubmodule := ↑(LieAlgebra.rootSpace H 0), lie_mem' := ⋯ }
Instances For
@[simp]
theorem
LieAlgebra.coe_zeroRootSubalgebra
(R : Type u_1)
(L : Type u_2)
[CommRing R]
[LieRing L]
[LieAlgebra R L]
(H : LieSubalgebra R L)
[LieAlgebra.IsNilpotent R ↥H]
:
(LieAlgebra.zeroRootSubalgebra R L H).toSubmodule = ↑(LieAlgebra.rootSpace H 0)
theorem
LieAlgebra.mem_zeroRootSubalgebra
(R : Type u_1)
(L : Type u_2)
[CommRing R]
[LieRing L]
[LieAlgebra R L]
(H : LieSubalgebra R L)
[LieAlgebra.IsNilpotent R ↥H]
(x : L)
:
x ∈ LieAlgebra.zeroRootSubalgebra R L H ↔ ∀ (y : ↥H), ∃ (k : ℕ), ((LieModule.toEndomorphism R (↥H) L) y ^ k) x = 0
theorem
LieAlgebra.toLieSubmodule_le_rootSpace_zero
(R : Type u_1)
(L : Type u_2)
[CommRing R]
[LieRing L]
[LieAlgebra R L]
(H : LieSubalgebra R L)
[LieAlgebra.IsNilpotent R ↥H]
:
theorem
LieAlgebra.le_zeroRootSubalgebra
(R : Type u_1)
(L : Type u_2)
[CommRing R]
[LieRing L]
[LieAlgebra R L]
(H : LieSubalgebra R L)
[LieAlgebra.IsNilpotent R ↥H]
:
H ≤ LieAlgebra.zeroRootSubalgebra R L H
@[simp]
theorem
LieAlgebra.zeroRootSubalgebra_normalizer_eq_self
(R : Type u_1)
(L : Type u_2)
[CommRing R]
[LieRing L]
[LieAlgebra R L]
(H : LieSubalgebra R L)
[LieAlgebra.IsNilpotent R ↥H]
:
theorem
LieAlgebra.is_cartan_of_zeroRootSubalgebra_eq
(R : Type u_1)
(L : Type u_2)
[CommRing R]
[LieRing L]
[LieAlgebra R L]
(H : LieSubalgebra R L)
[LieAlgebra.IsNilpotent R ↥H]
(h : LieAlgebra.zeroRootSubalgebra R L H = H)
:
If the zero root subalgebra of a nilpotent Lie subalgebra H is just H then H is a Cartan
subalgebra.
When L is Noetherian, it follows from Engel's theorem that the converse holds. See
LieAlgebra.zeroRootSubalgebra_eq_iff_is_cartan
@[simp]
theorem
LieAlgebra.zeroRootSubalgebra_eq_of_is_cartan
(R : Type u_1)
(L : Type u_2)
[CommRing R]
[LieRing L]
[LieAlgebra R L]
(H : LieSubalgebra R L)
[LieSubalgebra.IsCartanSubalgebra H]
[IsNoetherian R L]
:
LieAlgebra.zeroRootSubalgebra R L H = H
theorem
LieAlgebra.zeroRootSubalgebra_eq_iff_is_cartan
(R : Type u_1)
(L : Type u_2)
[CommRing R]
[LieRing L]
[LieAlgebra R L]
(H : LieSubalgebra R L)
[LieAlgebra.IsNilpotent R ↥H]
[IsNoetherian R L]
:
@[simp]
theorem
LieAlgebra.rootSpace_zero_eq
(R : Type u_1)
(L : Type u_2)
[CommRing R]
[LieRing L]
[LieAlgebra R L]
(H : LieSubalgebra R L)
[LieSubalgebra.IsCartanSubalgebra H]
[IsNoetherian R L]
:
noncomputable def
LieAlgebra.rootSpaceProductNegSelf
{R : Type u_1}
{L : Type u_2}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
{H : LieSubalgebra R L}
[LieAlgebra.IsNilpotent R ↥H]
[LieSubalgebra.IsCartanSubalgebra H]
[IsNoetherian R L]
(α : ↥H → R)
:
TensorProduct R ↥↑(LieAlgebra.rootSpace H α) ↥↑(LieAlgebra.rootSpace H (-α)) →ₗ⁅R,↥H⁆ ↥H
Given a root α, the Lie bracket restricted to the product of the root space of α and -α
takes value in the Cartan subalgebra.
When L is semisimple, the image of this map is one-dimensional and is spanned by the corresponding
coroot.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
LieAlgebra.coe_rootSpaceProductNegSelf_apply
{R : Type u_1}
{L : Type u_2}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
{H : LieSubalgebra R L}
[LieAlgebra.IsNilpotent R ↥H]
[LieSubalgebra.IsCartanSubalgebra H]
[IsNoetherian R L]
(α : ↥H → R)
(x : ↥(LieAlgebra.rootSpace H α))
(y : ↥(LieAlgebra.rootSpace H (-α)))
:
theorem
LieAlgebra.mem_range_rootSpaceProductNegSelf
{R : Type u_1}
{L : Type u_2}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
{H : LieSubalgebra R L}
[LieAlgebra.IsNilpotent R ↥H]
[LieSubalgebra.IsCartanSubalgebra H]
[IsNoetherian R L]
(α : ↥H → R)
{x : ↥H}
:
x ∈ LieModuleHom.range (LieAlgebra.rootSpaceProductNegSelf α) ↔ ↑x ∈ Submodule.span R {x : L | ∃ y ∈ LieAlgebra.rootSpace H α, ∃ z ∈ LieAlgebra.rootSpace H (-α), ⁅y, z⁆ = x}