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 #
@[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]
:
@[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.corootSpace
{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)
:
LieIdeal R ↥H
Given a root α relative to a Cartan subalgebra H, this is the span of all products of
an element of the α root space and an element of the -α root space. Informally it is often
denoted ⁅H(α), H(-α)⁆.
When L is semisimple over a field of characteristic zero, it is spanned by the coroot
corresponding to α, see LieAlgebra.IsKilling.coe_corootSpace_eq_span_singleton.
Note that the name "coroot space" is not standard as this space does not seem to have a name in the informal literature.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
LieAlgebra.mem_corootSpace
{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 ∈ LieAlgebra.corootSpace α ↔ ↑x ∈ Submodule.span R {x : L | ∃ y ∈ LieAlgebra.rootSpace H α, ∃ z ∈ LieAlgebra.rootSpace H (-α), ⁅y, z⁆ = x}
theorem
LieAlgebra.mem_corootSpace'
{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 ∈ LieAlgebra.corootSpace α ↔ x ∈ Submodule.span R {x : ↥H | ∃ y ∈ LieAlgebra.rootSpace H α, ∃ z ∈ LieAlgebra.rootSpace H (-α), ⁅y, z⁆ = ↑x}