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 #
@[reducible, inline]
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_genWeightSpace
{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 H.incl' (LieAlgebra.rootSpace H χ) = LieModule.genWeightSpace (↥H) χ
theorem
LieAlgebra.lie_mem_genWeightSpace_of_mem_genWeightSpace
{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}
{x : L}
{m : M}
(hx : x ∈ LieAlgebra.rootSpace H χ₁)
(hm : m ∈ LieModule.genWeightSpace M χ₂)
:
theorem
LieAlgebra.toEnd_pow_apply_mem
{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}
{x : L}
{m : M}
(hx : x ∈ LieAlgebra.rootSpace H χ₁)
(hm : m ∈ LieModule.genWeightSpace M χ₂)
(n : ℕ)
:
((LieModule.toEnd R L M) x ^ n) m ∈ LieModule.genWeightSpace M (n • χ₁ + χ₂)
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χ : χ₁ + χ₂ = χ₃)
:
↥(LieAlgebra.rootSpace H χ₁) →ₗ[R] ↥(LieModule.genWeightSpace M χ₂) →ₗ[R] ↥(LieModule.genWeightSpace 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χ : χ₁ + χ₂ = χ₃)
:
TensorProduct R ↥(LieAlgebra.rootSpace H χ₁) ↥(LieModule.genWeightSpace M χ₂) →ₗ⁅R,↥H⁆ ↥(LieModule.genWeightSpace 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χ : χ₁ + χ₂ = χ₃)
(x : ↥(LieAlgebra.rootSpace H χ₁))
(m : ↥(LieModule.genWeightSpace M χ₂))
:
theorem
LieAlgebra.mapsTo_toEnd_genWeightSpace_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)
{x : L}
(hx : x ∈ LieAlgebra.rootSpace H α)
:
Set.MapsTo ⇑((LieModule.toEnd R L M) x) ↑(LieModule.genWeightSpace M χ) ↑(LieModule.genWeightSpace 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χ : χ₁ + χ₂ = χ₃)
:
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χ : χ₁ + χ₂ = χ₃)
(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.toEnd 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]
:
H.toLieSubmodule ≤ LieAlgebra.rootSpace H 0
noncomputable instance
LieAlgebra.instNontrivialSubtypeMemLieSubmoduleLieSubalgebraGenWeightSpaceOfNatForall
(R : Type u_1)
(L : Type u_2)
[CommRing R]
[LieRing L]
[LieAlgebra R L]
(H : LieSubalgebra R L)
[LieAlgebra.IsNilpotent R ↥H]
[Nontrivial ↥H]
:
This enables the instance Zero (Weight R H L).
Equations
- ⋯ = ⋯
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]
:
(LieAlgebra.zeroRootSubalgebra R L H).normalizer = LieAlgebra.zeroRootSubalgebra R L 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)
:
H.IsCartanSubalgebra
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)
[H.IsCartanSubalgebra]
[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]
:
LieAlgebra.zeroRootSubalgebra R L H = H ↔ H.IsCartanSubalgebra
@[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)
[H.IsCartanSubalgebra]
[IsNoetherian R L]
:
LieAlgebra.rootSpace H 0 = H.toLieSubmodule
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]
[H.IsCartanSubalgebra]
[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(-α)⁆.
If the Killing form is non-degenerate and the coefficients are a perfect field, this space is
one-dimensional. See LieAlgebra.IsKilling.coe_corootSpace_eq_span_singleton and
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
- LieAlgebra.corootSpace α = (LieModuleHom.codRestrict H.toLieSubmodule ((LieAlgebra.rootSpace H 0).incl.comp (LieAlgebra.rootSpaceProduct R L H α (-α) 0 ⋯)) ⋯).range
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]
[H.IsCartanSubalgebra]
[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]
[H.IsCartanSubalgebra]
[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}